Apple Open-Sources Its Post-Quantum Crypto Code
Apple put its corecrypto library on GitHub, including formally verified ML-KEM and ML-DSA implementations. Here's why that matters.
On May 22, Apple published the corecrypto source code on GitHub. The repository includes implementations of the NIST post-quantum algorithms ML-KEM (FIPS 203) and ML-DSA (FIPS 204), along with the formal verification tooling Apple built to prove those implementations are correct.
The formal verification piece is the interesting part.
What’s in the repo
Corecrypto is the cryptographic library underneath Apple’s Security framework, CryptoKit, and CommonCrypto. It handles encryption, hashing, signatures, and random number generation on every Apple device. Until now, the source was not publicly available.
The repo includes Apple’s ML-KEM implementation (the lattice-based key encapsulation mechanism for establishing shared secrets) and ML-DSA (lattice-based digital signatures). Both algorithms were standardized by NIST in August 2024.
But the more interesting part is the formal verification folder. Apple didn’t just write PQC code and push it out. They built proof libraries that mathematically verify the ML-KEM and ML-DSA code matches the FIPS 203 and FIPS 204 specs. Apple says these are the strongest correctness results for any widely deployed production implementation of either algorithm. The proofs and tooling are all public now, so anyone can check that claim.
Why the proofs matter more than the code
Most crypto libraries rely on test vectors and code review. You run a known input, check you get the known output, and hope nothing weird happens with the inputs you didn’t test. Formal verification is different. It proves the code behaves correctly for all possible inputs, mathematically.
For algorithms that have been around for decades, like RSA or ECDSA, this is less urgent. Thousands of people have stared at those implementations. PQC algorithms are newer. Fewer eyes, less field time. A subtle bug in a key encapsulation mechanism could weaken security in ways that don’t show up in testing but matter enormously when the data you encrypted today gets decrypted by a quantum computer in 2035.
By publishing both code and proofs, Apple is letting the community verify these results rather than asking anyone to take their word for it. That’s worth something, and it puts pressure on other vendors to show similar rigor.
Everyone else is shipping too
Apple wasn’t the only one making moves last week. Google published a blog post urging the industry to get moving on PQC, confirming its own 2029 migration target. Google is already defaulting to quantum-safe TLS connections this year, and Android 17 uses ML-DSA for signature protection.
Earlier in May, AT&T launched the first commercially available post-quantum SD-WAN service in North America, built on the Cisco 8000 Series router. It uses NIST-aligned PQC for encryption and authentication, with global availability planned for later this year.
The policy side is tightening too. The White House made PQC a top federal priority in its March cyber strategy. EU member states need to publish national PQC strategies by the end of 2026. And Project Eleven released a report arguing that over $3 trillion in assets secured by elliptic curve cryptography could be exposed to quantum attack within four to seven years. Their estimate for Q-Day? Possibly as early as 2030.
Where this leaves you
If you’re a security engineer evaluating PQC implementations, you now have a reference codebase with formal correctness proofs you can study and compare against. That’s more than most vendors offer. The verification approach Apple used will probably become the bar other implementations get measured against, at least for ML-KEM and ML-DSA.
More broadly, the excuse that PQC is “still too early” is getting thin. The standards exist. Verified implementations are public. You can buy quantum-safe network services from AT&T today. Cloudflare is targeting full PQC by 2029.
If you haven’t started your cryptographic inventory yet, you’re behind. Not in a sky-is-falling way, but the window where migration felt optional has closed.