Apple has made public quantum-resistant cryptographic code and the verification tools used to check it, including implementations of ML-KEM and ML-DSA for its corecrypto library, which secures software on more than 2.5 billion active devices.
KEY FACTS
- Algorithms The release covers ML-KEM and ML-DSA, two standardized quantum-secure algorithms.
- Library The code is part of corecrypto, used across Apple operating systems.
- Verification Apple also published the formal verification libraries, tools and methodology it used.
- Bug found The verification process uncovered a missing step in ML-DSA that could have broken digital signatures.
In a technical analysis from Apple, the company said it translated the code into Cryptol and then into Isabelle, a proof assistant, to show the implementation matched the standards. Apple said the process produced the strongest known correctness results for any widely deployed production implementation of these algorithms.
The disclosure says the company began deploying quantum-resistant encryption in iMessage in 2024 and later expanded it to VPN services and TLS networking protocols. Apple said it selected ML-KEM and ML-DSA because they best fit its requirements for security, performance and compact parameters.
Apple said conventional testing still plays a role because formal methods cannot cover every aspect of the code. The company used a hybrid approach that combined mathematical proof, testing and end-to-end evaluation.
The published tools include a Cryptol-to-Isabelle translator and supporting libraries needed to reproduce the results. Apple said the work is intended for independent review and broader industry use.
WHY IT MATTERS
The release gives security researchers and developers code, proof tools and documentation they can examine and reuse as the industry prepares for quantum computers that could weaken current encryption. It also shows how formal verification can find flaws that normal testing may miss.