Apple has released the source code for its corecrypto library along with formal mathematical proofs verifying the correctness of its ML-KEM and ML-DSA (post-quantum cryptography) implementations against FIPS 203 and FIPS 204 specifications. The approach combines Cryptol, SAW, and Isabelle proof assistants with a custom Cryptol-to-Isabelle translator built by Galois. The verification covers both portable C code and hand-optimized ARM64 assembly, requiring over 50,000 proof steps. Formal verification caught real bugs — including a missing step in an early ML-DSA implementation that could silently corrupt cryptographic computations — that conventional testing would have missed. Apple is open-sourcing the verification libraries, Isabelle theories, and tooling to advance the state of the art in critical software assurance.
