“Based on our work to date, we believe that the strongest assurance possible comes from combining formal verification with conventional methods and critically evaluating the end-to-end results,” the blog post reads.
Apple's ML-KEM and ML-DSA implementations
Apple has publicly released implementations of two quantum-resistant algorithms — ML-KEM and ML-DSA — and folded them into corecrypto, the company’s cryptographic library used across its operating systems. Corecrypto handles encryption, decryption, hashing and digital signatures on over 2.5 billion active devices, according to Apple. The company began deploying quantum-resistant encryption in iMessage in 2024 and has since extended the technology to VPN services and TLS networking protocols.
Cryptol-to-Isabelle translator and supporting tools
Alongside the algorithm implementations, Apple published the formal verification libraries and tools it used to prove the code’s correctness, including a Cryptol-to-Isabelle translator. Apple translated its code into Cryptol — a formal language developed by Galois — and then into Isabelle, the proof assistant developed at the University of Cambridge and The Technical University of Munich, to demonstrate that the implementations matched the official standards. The company also released the supporting libraries required to reproduce the results.
Formal verification: what Apple proved and what it could not
Apple describes its verification methodology as achieving “the strongest known correctness results for any widely deployed production implementation of these algorithms.” Formal verification, the company explains, uses mathematical proofs to show that code works correctly for all possible inputs, a capability conventional testing cannot provide. Apple notes that formal methods uncovered errors conventional testing would have missed, but it also acknowledged constraints: the team could not formally verify every single aspect of their code with the available tools. As a result, Apple combined formal verification for core mathematical correctness with conventional testing for areas the formal tools could not cover, and a careful evaluation of how all pieces work together.
The bug found in ML-DSA and its practical implications
During the verification work, researchers discovered a missing computational step in the ML-DSA code that would have silently broken digital signatures. Apple warned that, had this bug reached production, messages in iMessage “may have appeared authenticated when they actually weren’t,” leaving users unaware that their communications lacked proper security. The finding illustrates a concrete case where formal proofs detected a flaw that could evade traditional test-case-based validation.
What this means for technologists, procurement leaders, and end users
- Technologists and security teams: The release gives cryptographers and implementers access to Apple’s implementations and the formal-verification toolchain — including the Cryptol-to-Isabelle translator — so independent review and reuse are possible. Teams will likely examine the verification artifacts and reproduce Apple’s proofs where applicable.
- Procurement leaders and affected enterprises: Organizations evaluating quantum-resistant options gain a production-grade reference implementation integrated into a widely deployed library. The availability of verification artifacts may inform acquisition and assurance conversations, especially where mathematical proof of core properties is a procurement requirement.
- End users and the general public: Apple’s work aims to address the threat posed by future quantum computers that could break current encryption methods. The company’s hybrid approach — formal verification plus conventional testing — is presented as a risk-reduction strategy to keep services such as iMessage, VPNs and TLS-based networking more robust against future cryptographic threats.
Apple selected ML-KEM and ML-DSA from among several standardized quantum-resistant algorithms because, the company said, they best matched its requirements for security, performance and compact parameters. While Apple stresses the added assurance from formal methods, it also underscores that conventional cryptographic testing and evaluation remain necessary for comprehensive assurance.
The company has made additional information available on its corecrypto GitHub page and published a blog post describing the verification methodology and the released tools. For readers who want to review the original reporting and links to Apple’s materials, see the CyberScoop story linked below.
https://cyberscoop.com/apple-open-source-quantum-resistant-encryption/
