Apple Publishes iPhone Post-Quantum Code on GitHub, Proofs Included

Apple uploaded its post-quantum cryptography source code to GitHub on May 22, 2026, packaged with the formal mathematical proofs that verify the implementations match NIST’s FIPS 203 and FIPS 204 standards, the algorithms designed to protect iPhone, Mac, and iMessage encryption against future quantum computers. The release covers the cryptographic code already running on more than 2.5 billion active Apple devices, protecting iMessage, Transport Layer Security (TLS, the protocol securing HTTPS) networking, virtual private network (VPN) connections, and the iPhone-to-Apple Watch link.

Inside the corecrypto_verify subdirectory of the new repository sits a toolchain Apple built with Galois that translates cryptographic specifications into formal mathematics, then proves the production implementation matches the spec line for line. It already caught a real bug in Apple’s own ML-DSA code that conventional testing missed.

What Landed on May 22

The new corecrypto repository on GitHub ships the low-level cryptographic library that powers Apple’s Security framework, CryptoKit, and CommonCrypto. These are the building blocks the operating system reaches for whenever it needs encryption, hashing, random number generation, or a digital signature.

Per Apple’s Security Research blog, the repository contains:

• Production implementations of ML-KEM (Module-Lattice-Based Key-Encapsulation Mechanism) and ML-DSA (Module-Lattice-Based Digital Signature Algorithm), the two post-quantum algorithms Apple chose for corecrypto
• Tests, performance tools, and build targets developers use to evaluate the code
• A dedicated formal verification folder containing the proof work and supporting tools
• Apple’s Isabelle theories used to mathematically check correctness
• The Cryptol-to-Isabelle translator built to Apple’s specification

NIST (the National Institute of Standards and Technology) finalized ML-KEM as FIPS 203 and ML-DSA as FIPS 204 on August 13, 2024, closing an eight-year selection process. ML-KEM handles key encapsulation, the step in a secure conversation where two parties agree on a shared secret. ML-DSA handles digital signatures, which prove a message came from who it claims to have come from.

Why the Verification Toolchain Matters More Than the Algorithms

Multiple major vendors shipped post-quantum cryptography in production before this release. Cloudflare has been rolling out X25519MLKEM768, a hybrid mode pairing ML-KEM-768 with classical elliptic curve cryptography, since before NIST finalized the standard. Signal moved its initial key handshake to PQXDH (Post-Quantum Extended Diffie-Hellman) in 2023. Chrome, Firefox, OpenSSL, Java 27, and Cloudflare all support post-quantum key agreement by default in current versions.

The unusual move at Apple is shipping production code with machine-checkable proofs that it does what the spec says. The company claims the corecrypto release achieves the strongest known correctness results for any widely-deployed production implementation of ML-KEM and ML-DSA. That is a deliberately narrow claim. It does not assert strongest cryptographic security. It asserts strongest assurance the code faithfully implements the published algorithm.

Apple’s verification stack rests on three open-source tools.

Isabelle, the Proof Assistant

Isabelle is a formal language and proof checker that handles complex mathematical proofs. Apple already uses it to verify the hardware Public Key Accelerator on its silicon, so the company had institutional experience with the tool before the post-quantum work began.

Cryptol and SAW

Cryptol is a domain-specific language for cryptographic algorithms, developed by Galois Inc. for the NSA’s Laboratory for Advanced Cybersecurity Research. SAW, the Software Analysis Workbench, verifies that a software implementation matches a Cryptol specification. Apple manually translates its portable C implementation of each algorithm into Cryptol, then uses SAW to confirm the two match.

The Cryptol-to-Isabelle Translator

Galois built this new tool to Apple’s specification. It converts Cryptol algorithm models into Isabelle formulas so they can be checked against the official NIST standards, which Apple also encoded in Isabelle. The translator and the supporting Isabelle theories ship in the new repository under licenses more permissive than the rest of corecrypto, so other researchers and library maintainers can reuse them on their own implementations.

The Bug That Conventional Testing Could Not Find

Formal verification caught at least two real problems before the code shipped to customers. The company described both in its Security Research blog post.

For example, we 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. We also discovered an error in a third-party proof, which we were able to independently repair for the specific parameter values used in our implementation.

That third-party proof matters. The cryptographic research community has been building proofs around ML-KEM and ML-DSA since the algorithms were Kyber and Dilithium drafts. If a published proof contains an error subtle enough that one of the world’s most resourced security teams had to repair it, the same error is sitting in other people’s verification work.

The missing-step bug is the more visceral example. Apple says in the worst case the issue could have silently corrupted cryptographic computations without any warning from existing test suites. That is the textbook failure mode for cryptographic code: a small mathematical mistake that does not crash anything, does not look obviously wrong in any test vector, and quietly weakens the protection of every conversation it touches.

How Apple’s Rollout Stacks Up Against Signal and Cloudflare

Several vendors deployed post-quantum cryptography in production before this release. The table below shows where Apple’s work fits in that landscape.

Cloudflare reports that over 35% of non-bot HTTPS traffic touching its network is now post-quantum secure, with hybrid X25519MLKEM768 covering most major browsers and major TLS libraries. Signal’s SPQR (Sparse Post-Quantum Ratchet) extends PQ protection to ongoing message exchanges, not just session setup. What Apple’s release adds to that landscape is the mathematical proof work that other implementers can study, audit, and reuse.

The Licensing Catch Nobody Highlighted

Calling the new corecrypto repository open source overstates what Apple actually published. The default license remains the corecrypto Internal Use License Agreement, a non-redistributable 90-day evaluation license intended only for inspecting the code’s security characteristics. This is the same restrictive license Apple has attached to corecrypto since it first published the source in 2015.

The verification folder is the meaningful exception. Files in corecrypto_verify/isabelle/Apple_Isabelle_Libraries and the translator directory ship under more permissive per-subdirectory licenses. Security researchers, academic groups, and other library maintainers can take those proof tools, study them, and apply them to their own implementations of ML-KEM and ML-DSA.

What Apple has open-sourced, in the meaningful sense of the term, is the methodology. The cryptographic implementation itself remains source-available under restrictions. For practical purposes, the most reusable artifact in the repository is the proof toolchain, which is precisely the piece Apple says it built to raise the bar for cryptographic assurance.

What This Means for Developers Building on iOS and Mac

• ML-KEM-768 and ML-KEM-1024 for key encapsulation, exposed through CryptoKit on iOS 26, iPadOS 26, macOS 26, tvOS 26, and watchOS 26
• ML-DSA-65 and ML-DSA-87 for digital signatures, same platforms, same release window
• Quantum-secure TLS on by default in URLSession and the Network framework for any app that uses those APIs (the standard ones)
• IKEv2 API exposes post-quantum key exchange to third-party VPN clients without reimplementing the math from scratch

The default-on behaviour is the policy choice that matters. Security upgrades that require developers to opt in tend to propagate slowly through any large app ecosystem. By wiring quantum-secure key agreement into the system APIs that handle most networking traffic on iOS and macOS, Apple converts the migration from a per-app decision into a server-side one. If the server supports post-quantum key agreement, the connection is post-quantum secure.

That still leaves the harder problem, which is post-quantum digital signatures for TLS certificates. ML-DSA signatures are significantly larger and slower than the elliptic-curve signatures they will eventually replace, and the certificate ecosystem is built around signatures from public Certificate Authorities. That part of the transition is being prototyped (Cloudflare is evaluating ML-DSA-44) but is not ready for default rollout anywhere. The next read on Apple’s progress will come in the next OS cycle, when authentication signatures, not just key agreement, start showing up in shipping code.

Frequently Asked Questions

What Is Post-Quantum Cryptography?

Post-quantum cryptography (PQC) refers to encryption and digital signature algorithms designed to remain secure against future quantum computers. These machines could break current public-key methods like RSA and elliptic curve cryptography by efficiently solving the math problems those methods rely on. NIST finalized the first three PQC standards (FIPS 203, 204, and 205) in August 2024, ending an eight-year competition.

Are My iMessage Conversations Already Protected Against Quantum Attacks?

Yes, if your devices are running iOS 17.4 or later, iPadOS 17.4 or later, macOS 14.4 or later, or watchOS 10.4 or later. Apple deployed its PQ3 protocol across those releases in 2024, adding post-quantum protection both at the start of a conversation and as encryption keys are refreshed over time.

Do I Need to Do Anything to Get Post-Quantum TLS and VPN Protection?

On Apple’s current OS 26 generation, quantum-secure TLS is on by default in URLSession and the Network framework, the standard APIs most apps already use. For VPN, the native client and the IKEv2 developer APIs include post-quantum key exchange. The catch is that the server you connect to must also support post-quantum key agreement, otherwise the connection falls back to classical cryptography.

Did Apple Really Find a Cryptographic Bug Nobody Else Found?

Apple’s blog reports that formal verification caught a missing step in an early ML-DSA implementation that could, in rare cases, cause inputs to exceed the expected range and produce incorrect output. The company also says it identified an error in a third-party proof of ML-DSA and repaired it for the parameter values used in corecrypto. Both findings were caught before the code reached customers.

When Will Quantum Computers Actually Break Current Encryption?

There is no consensus date. Industry estimates range from around 2030 to beyond 2035. The more immediate concern is the harvest-now-decrypt-later threat model (HNDL), in which adversaries store encrypted traffic today and decrypt it once a sufficiently powerful quantum computer becomes available. That model is the reason post-quantum migration is happening now, before fault-tolerant quantum hardware exists.

Is the Corecrypto Code Now Genuinely Open Source?

No, not in the full sense. The default corecrypto license remains the Internal Use License Agreement, a non-redistributable 90-day evaluation license intended only for inspecting the code’s security characteristics. The exception is the formal verification work: files in the Apple_Isabelle_Libraries directory and the Cryptol-to-Isabelle translator are available under more permissive per-subdirectory licenses, making the proof tooling genuinely reusable by other implementers.