Apple Publishes Formal Verification Blueprint for Quantum-Secure corecrypto

Apple has released its implementations of post-quantum ML-KEM and ML-DSA algorithms in corecrypto alongside the mathematical proofs used to formally verify their correctness against FIPS 203 and FIPS 204. The company also published its custom formal verification libraries and tools, which it used to achieve the strongest known correctness guarantees for a widely deployed production cryptographic library. The work aims to prevent subtle bugs in quantum-secure cryptography across over 2.5 billion active devices, building on techniques previously used for Apple silicon hardware verification.