Apple’s Corecrypto Proof And A Next Phase Of Quantum Migration

In the late 1990s, a new kind of encryption called elliptic curve cryptography started showing up in phones, websites, and game consoles. The math behind it was solid. The code that ran the math was not. Engineers made small mistakes deep inside the software, and attackers found them. In 2010, Sony lost the master signing key for the PlayStation 3 because the code reused a random number it was supposed to generate fresh every time. Once that key leaked, anyone could load any software they wanted onto the console. The math worked. The code did not.

I wrote in April about the two paths to post-quantum cryptography, software and hardware, and how moving everything over will take more than a decade. Post-quantum cryptography, or PQC, is the new family of encryption designed to survive future quantum computers. Today’s encryption depends on math problems that classical computers cannot solve in any reasonable time. A large enough quantum computer running Shor’s algorithm makes those problems easy.

On May 22, Apple released a major update to corecrypto, the encryption software running on more than 2.5 billion Apple devices. The update includes the new post-quantum algorithms standardized by NIST, called ML-KEM (for key exchange) and ML-DSA (for digital signatures). What makes this release different is that Apple also published a mathematical proof that the code does exactly what the standard says it should do. No surprises. No hidden mistakes. The technique is called formal verification, and it has been used for decades in chip design and aerospace software. Seeing it applied to cryptography on consumer devices is new.

It often takes years of work and very specialized math skills. Apple’s proof runs more than 50,000 steps and already caught a bug that normal testing would have missed. Apple open-sourced the tools, including software built by Galois Inc., so other companies can do the same thing. iMessage, Signal, Chrome, and Cloudflare are already shipping post-quantum protections, and more are coming.

For decades the pattern was ship first, fix later. The quantum migration is too important and too complicated for that. Apple just showed what doing it right looks like. The next step for us academics - colleges and training programs must prepare engineers who will do it.