Apple has released quantum-resistant cryptographic code and the mathematical verification tools it developed to prove the code’s correctness, making them publicly available for independent review and broader industry use.
The release includes implementations of two quantum-secure algorithms — ML-KEM and ML-DSA — along with the formal verification libraries and tools Apple created to validate their accuracy. The company also published detailed documentation of its verification methodology, which it describes as achieving the strongest known correctness results for any widely deployed production implementation of these algorithms.
Formal Verification Caught What Testing Missed
The verification process uncovered errors that conventional testing would have missed. Researchers found a missing computational step in the ML-DSA code that would have silently broken digital signatures in production. If this bug had shipped, messages in iMessage may have appeared authenticated when they actually weren’t — leaving users unaware their communications lacked proper security.
Testing works by trying many scenarios, but with complex cryptographic code there are too many possible inputs to test exhaustively. Formal verification uses mathematical proofs to show that code works correctly for all possible inputs at once — catching subtle bugs that hide in the gaps between test cases.
The Broader Deployment
The quantum-secure algorithms are integrated into corecrypto, Apple’s cryptographic library used across its operating systems — handling encryption, decryption, hashing, and digital signatures on over 2.5 billion active devices. Apple began deploying quantum-resistant encryption in iMessage in 2024 (PQ3) and has expanded the technology to VPN services and TLS networking protocols.
The algorithms address the threat posed by future quantum computers, which could potentially break the encryption methods currently protecting digital communications. The full code is available on Apple’s corecrypto GitHub page.
