Corecrypto proofs against FIPS 203 and FIPS 204
Apple’s corecrypto work on ML-KEM and ML-DSA draws a hard line around correctness. The aim is not just that the code runs, but that the portable C implementation matches the FIPS 203 and FIPS 204 specifications closely enough to prove it. That is a sensible target when the same cryptography feeds iMessage, VPN, TLS networking, and CryptoKit APIs.
Why Apple bothered proving the ML-KEM and ML-DSA paths
Post-quantum cryptography arrived in corecrypto in 2024, and that brings a new kind of failure risk. ML-KEM and ML-DSA are newer than the classical primitives already embedded in Apple’s stack, so there is less field experience to lean on and fewer years of bug reports to steal confidence from.
Formal verification gives Apple a way to say more than “it passed tests”. It lets the implementation be checked against the maths in the standard, which matters when a flaw sits in a library used by a very large device base. If a corecrypto bug lands in the wrong place, the blast radius is awkwardly large.
The other reason is practical rather than glamorous. Quantum-secure cryptography sits in places where failure is boringly expensive: transport security, device messaging, and API surfaces that other code assumes are correct. Proving the path gives a stronger bound on what the code can and cannot do.
How the portable C code is tied back to the FIPS text
The implementation starts in portable C, which is the sensible place to prove equivalence before the code is specialised for Apple silicon. The proof work links the formulas in the code back to the formulas in FIPS 203 and FIPS 204, so the argument is mathematical rather than observational.
That matters because production crypto is rarely a neat translation of a standard document. The portable layer has to survive compiler choices, platform differences, and all the ordinary ways code gets made less elegant in the name of speed. Hand-optimised routines then sit on top of that base, with separate checking to show they still match the verified behaviour.
Apple also pairs formal verification with testing, simulation, and independent review. That is not window dressing. Each method catches different failure modes, and proof alone does not tell you whether the implementation remains faithful once the optimised paths and hardware-specific tricks arrive.
Where the proof obligations get awkward in optimised code
Optimised crypto code is where proofs start collecting sharp edges. A hand-tuned routine may depend on exact processor behaviour, timing properties, or low-level data flow that looks ugly in the source and even uglier in the proof. The more a function is shaped around the machine, the more awkward it becomes to express the same behaviour in a clean model.
Apple leans on Data Independent Timing and Pointer Authentication to reduce two common risks: timing leakage and memory corruption. Those controls help, but they also add proof obligations of their own. A compiler can interfere with timing guarantees, and a micro-architectural quirk can still expose more than the developer wanted. The proof has to sit close enough to the real code to matter, which is where the work becomes tedious in the proper sense of the word.
What the proofs do not cover, and what still needs checking
A proof of equivalence is not a proof that the whole system is safe. It says the code matches the stated algorithms under the model being checked. It does not make every deployment choice harmless, and it does not erase the usual risks around integration, compiler behaviour, or surrounding code that misuses the primitives.
The remaining checks still matter. Testing catches regressions. Simulation exposes behaviour that proof models may flatten away. Independent review helps spot places where a neat argument hides a messy implementation detail. None of that is exotic, just the unglamorous part of shipping cryptography that other code depends on.
There is also a limit on what formal verification can buy when the algorithms themselves are new in production use. ML-KEM and ML-DSA have a standards body behind them, but not decades of field scar tissue. A verified implementation narrows the correctness boundary; it does not remove the need to keep checking the edges where the verified code meets the rest of the platform.
