Apple published formal verification methods for its quantum-secure cryptography implementations in corecrypto, the cryptographic library running on over 2.5 billion devices. The company released mathematical proofs confirming its ML-KEM and ML-DSA implementations faithfully follow FIPS 203 and FIPS 204 specifications, along with the verification libraries and tools used to achieve the strongest correctness guarantees for any widely deployed production implementation.

In 2024, Apple began adding post-quantum encryption to corecrypto after identifying ML-KEM and ML-DSA as the algorithms best matching its four-part criteria for inclusion: security improvement, strong theoretical design, high performance, and compact parameters. These matched the same two algorithms NIST later standardized, and Apple applied mathematical optimizations plus hand-tuned code paths to take full advantage of Apple silicon.

Implementations were hardened using Data Independent Timing and Pointer Authentication to prevent timing side channels and memory exploits. Apple released the code and verification tools this week for independent expert evaluation, marking one of the most comprehensive formal verification efforts ever applied to production cryptographic code.