Apple open-sources quantum-resistant encryption code and formal verification tools
Apple released its quantum-resistant cryptographic implementations and the formal verification tools used to prove their correctness, making them publicly available for industry-wide review.
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 use across the industry. 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.
The quantum-secure algorithms are integrated into corecrypto, Apple's cryptographic library used across its operating systems. The library handles encryption, decryption, hashing, and digital signatures on over 2.5 billion active devices. Apple began deploying quantum-resistant encryption in iMessage in 2024 and has expanded the technology to VPN services and TLS networking protocols. This open-source release allows the broader security community to inspect and validate the same code that protects hundreds of millions of users today.
One of the tools released is the company's Cryptol-to-Isabelle translator, which converts cryptographic models between formal languages, along with supporting libraries needed to reproduce the results. Formal verification uses mathematical proofs to show that code works correctly for all possible inputs. Apple translated its code into Cryptol, a formal language developed by Galois, then into Isabelle, a proof assistant from the University of Cambridge and The Technical University of Munich, to prove both matched the official standards. Apple has used Isabelle previously to verify hardware cryptographic components.
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. If this bug had reached production, messages in iMessage may have appeared authenticated when they actually weren't, leaving users unaware their communications lacked proper security. The discovery underscores the value of formal verification for catching subtle flaws in complex cryptographic implementations.
Even with these tools, Apple acknowledged that it still depends on conventional cryptographic testing and evaluation for assurance. Formal verification can catch errors that traditional testing simply cannot find. Testing works by trying many scenarios, but with complex cryptographic code, there are too many possible inputs to test exhaustively. Subtle bugs can hide in the gaps between test cases and never trigger a warning. Formal verification, by contrast, uses mathematics to prove correctness across all possible inputs at once.
However, Apple's team writes that it couldn't formally verify every single aspect of their code with the tools available, so they combined approaches: formal verification for core mathematical correctness, conventional testing for aspects formal methods couldn't cover, and careful evaluation of how all the pieces work together. Apple argues this hybrid approach provides the most robust security for critical cryptographic software. "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.
The open-source release marks a significant contribution to the cryptography community as organizations race to prepare for the threat of quantum computers, which could eventually break the encryption methods currently protecting digital communications. Apple selected ML-KEM and ML-DSA from among several standardized quantum-resistant algorithms because they best matched the company's requirements for security, performance, and compact parameters. The tools and code are now available for inspection on Apple's corecrypto GitHub page, enabling other vendors and researchers to adopt similar formal verification practices for their own cryptographic implementations.