Apple shipped formal proofs for its post-quantum crypto. 2.5 billion devices now run verified code.

Apple’s Security Engineering and Architecture team published formal verification proofs for the post-quantum cryptographic algorithms in corecrypto on May 22. The release covers Apple’s implementation of ML-KEM and ML-DSA, the two algorithms NIST standardised under FIPS 203 and 204 in 2024.

corecrypto is the cryptographic core that ships on every iPhone, iPad, Mac, Watch and TV. Apple cites 2.5 billion active devices running it, which makes it one of the most widely deployed cryptographic codebases in the world. The new release is the first time Apple has paired the source code with machine-checked mathematical proofs that the implementation matches the standard.

What “formally verified” actually means here

Apple’s framing is the right one to quote: “if we can prove that the mathematical formula of our implementation is equivalent to that of its specification, then we know that our implementation will produce the correct output.” A formal proof translates the C or assembly code into a logical model and shows, step by step, that the model behaves identically to the standard’s reference. The output is a mathematical certificate, not a test pass rate.

The toolchain Apple used is worth tracking, because it’s mostly off-the-shelf and could be borrowed by any other cryptographic project willing to do the work.

• Cryptol, the cryptography-focused functional language Galois maintains, holds the formal specification.
• SAW, the Software Analysis Workbench, checks that the compiled implementation matches that specification.
• Isabelle, the proof assistant that’s been doing this kind of work in academic settings for decades, carries the high-level theorems.
• cryptol-to-isabelle, a new translator Apple wrote and is releasing alongside the post, lets Cryptol models feed Isabelle directly.

That last piece is the interesting one. Cryptol-to-Isabelle is the tool that closes the loop between “this is the standard” and “this is the code we shipped,” and it’s the part of the work other vendors don’t have today. Apple is publishing the translator, which suggests an intent to make the broader ecosystem catch up rather than keep the moat.

What the proofs caught that testing didn’t

The post documents one finding: formal verification “identified a missing step in an early ML-DSA implementation, which in rare cases could cause inputs to exceed the expected range and produce incorrect output.” Apple is explicit that the bug would have been hard to surface through conventional testing, because the failing inputs were too rare to land in a fuzz corpus and too valid-looking to fail a unit test.

That’s the case for formal verification compressed into one example. Cryptographic code is the worst possible target for empirical testing, because the gap between “works on every input I tried” and “works on every input that exists” is exactly the gap an adversary will hunt. NIST-standardised algorithms have huge input spaces, and the wrong-output cases that matter cluster at the edges of those spaces. A proof closes that gap by construction.

The work isn’t free. Apple cites 50,000 proof steps to cover the implementation, which is the kind of number that translates to many engineer-years. The “blueprint” framing in the post title suggests Apple wants other projects to adopt the same toolchain rather than reinvent it, but anyone doing so should plan for a multi-quarter effort on a single primitive.

This release also lands in a market that has been slowly catching up on post-quantum deployment. GnuPG mainlined ML-KEM in April; Ubuntu 26.04 LTS shipped with post-quantum SSH by default the same month. The 2.5-billion-device installed base Apple ships against now becomes the largest formally verified ML-KEM and ML-DSA deployment in production.

What this means for you

If you’re building cryptographic code that will ever be a regulatory or audit target, this is the bar you’ll eventually be measured against. The proof artifacts and the cryptol-to-isabelle translator are public, which means the next post-quantum migration review at a regulated firm can credibly ask “is your implementation formally verified the way Apple’s is?” The right answer in 2027 won’t be “we ran fuzzers for six months.”

If you’re a developer relying on Apple’s platform primitives, this is the rare instance where vertical integration is the customer’s win. The TLS connections, file encryption, and key-exchange operations your app delegates to corecrypto are now backed by a proof that the underlying algorithm produces the correct ciphertext on every input. You still have to handle keys correctly. But the layer below your code now has a mathematical certificate behind it, and that is genuinely new.