One common misconception about quantum computing threats is that they only matter once a sufficiently powerful quantum computer actually exists. The encryption protecting most of today’s digital communications — RSA, elliptic curve cryptography, Diffie-Hellman — is vulnerable in principle to a quantum algorithm called Shor’s algorithm. But without a fault-tolerant quantum computer capable of running it at scale, the math remains practically unbreakable.
The mistake in this reasoning is the phrase “once a sufficiently powerful quantum computer actually exists.” Any adversary with the patience and storage capacity to collect encrypted communications today can simply hold them — waiting for quantum computing to mature before decrypting. Intelligence agencies almost certainly already do this. The data they’re collecting right now, protected by algorithms we consider strong, may be in their archives for a decade or more before it becomes readable.
This is the harvest now, decrypt later problem is a major reason why Apple started working on post-quantum encryption for iMessage years ago, not after a quantum threat materialized.
The company released a detailed technical blog post that serves as an introduction to quantum-secure cryptography in iMessage, which marks the start of a significant security transition to protect Apple users now from quantum computers that are deployed in the future.
In early 2024, Apple deployed what it calls PQ3 — its third-generation iMessage cryptographic protocol. The “3” refers not to a version number but to Apple’s own classification of security levels for messaging protocols. Level 1 protects initial key establishment with post-quantum algorithms. Level 2 adds ongoing rekeying, so that even if a key is later compromised, past messages remain protected. PQ3 reaches Level 3, whic means post-quantum security that applies both to initial key establishment and to ongoing message encryption, with the ability to re-establish cryptographic security automatically even if a session key is somehow compromised mid-conversation.
The core upgrade was integrating ML-KEM (also known as CRYSTALS-Kyber, now standardized by NIST as FIPS 203) for key encapsulation alongside the existing elliptic curve Diffie-Hellman (ECDH) mechanism. ML-KEM’s security is based on the hardness of solving problems involving high-dimensional mathematical lattices — a class of problems for which no efficient quantum algorithm is currently known.
Apple didn’t replace ECDH entirely, at least not immediately. Instead, it combined classical and post-quantum key exchange in a hybrid design. The session key is derived from both mechanisms, meaning that breaking the encryption requires defeating both simultaneously. This matters: if ML-KEM were later found to have a flaw, the classical ECDH layer would still hold. If ECDH succumbs to quantum attack, ML-KEM covers it. The hybrid approach is the right call for a transition period where confidence in post-quantum algorithms is still accumulating.
ML-DSA and Digital Signatures
Key exchange isn’t the only piece. Messaging systems also need to verify that the person you’re talking to is actually who they say they are — that requires digital signatures. Apple also deployed ML-DSA (CRYSTALS-Dilithium, FIPS 204), a post-quantum signature scheme based on the same lattice mathematics as ML-KEM, for authentication in its cryptographic infrastructure.
Both ML-KEM and ML-DSA were selected by Apple before NIST finalized its standardization process — and the two algorithms Apple converged on independently were precisely what NIST ultimately standardized. That alignment wasn’t luck; it reflects that the global cryptographic research community had reached broad consensus on which approaches combined security and performance most convincingly.
Apple’s effort is ahead of most enterprise security migrations and offers a glimpse of the company’s technical ambition.
Post-quantum algorithms are mathematically newer than RSA or ECC. There’s less collective implementation experience, fewer battle-tested libraries, and a higher risk that a subtle bug in implementation could undermine the security guarantee of a theoretically sound algorithm. Early ECC implementations, before the cryptographic community developed robust shared tooling, were riddled with exploitable bugs. Apple clearly studied that history carefully.
Rather than relying on conventional testing — which, however thorough, cannot prove the absence of bugs, only their presence — Apple applied formal verification, namely, mathematical proofs that the implementation is equivalent to the algorithm’s specification. This is the gold standard for safety-critical code, yet enormously difficult to pull off.
Apple’s approach works in several layered steps:
- The portable C implementation of each algorithm (ML-KEM and ML-DSA) is translated into Cryptol, a formal language designed for cryptographic specifications.
- The SAW (Software Analysis Workbench) tool, developed by Galois, verifies that the Cryptol model matches the actual C code.
- A new translator — specified by Apple and built by Galois — converts the Cryptol model into Isabelle, a powerful proof assistant that can verify complex mathematical theorems.
- Apple’s engineers also manually translate the NIST FIPS specifications for ML-KEM and ML-DSA into Isabelle. Now both the implementation and the standard live in the same formal mathematical language.
- Proofs are written in Isabelle demonstrating that the implementation is equivalent to the specification — not just for the algorithm as a whole, but for every subroutine in the sequence, and for the correctness of how they compose together. This required more than 50,000 proof steps.
- For the hand-optimized ARM64 assembly code that runs on Apple silicon, the process takes a further step: proving each assembly subroutine equivalent to its C counterpart, which is already proven correct.
The result is a chain of verified correctness from the FIPS specification all the way down to the machine-level assembly instructions executing on iPhones and Macs.
This is not hypothetical rigor. During the process, Apple’s formal verification caught a real bug in an early ML-DSA implementation. It found a missing step that in rare cases would cause inputs to exceed their expected range and produce incorrect output. This is exactly the kind of subtle, low-frequency defect that conventional test suites miss — it might only manifest in unusual edge cases, with no observable error. The formal proof found it.
The team also discovered an error in a third-party proof and repaired it independently for the specific parameter values used in Apple’s implementation.
The Scale Consideration
Apple’s corecrypto library — the foundational cryptographic layer for all Apple operating systems — runs continuously on more than 2.5 billion active devices. A bug in corecrypto doesn’t affect one app or one service; it potentially affects every app and feature on every Apple device. That’s the context for understanding why the formal verification effort was proportionate, not excessive.
The implementations also had to be engineered for performance across the full range of Apple hardware: from M-series MacBook Pros with enormous compute resources to constrained embedded chips in older devices and IoT hardware. This meant writing in portable C first, then hand-optimizing critical subroutines in ARM64 assembly to take full advantage of Apple silicon’s specific microarchitecture — including hardware features like Data Independent Timing (DIT), which guards against timing side-channel attacks that could otherwise leak secret values by measuring how long operations take.
ML-KEM public keys run to about 1,184 bytes, compared to 32 bytes for an ECC key — nearly 37 times larger. For devices with constrained memory or bandwidth, that’s a real cost. Apple’s performance optimizations are specifically designed to make the trade-off manageable across all its hardware.
What It Means for iMessage Users
In practical terms, iMessage users don’t configure anything. The post-quantum protections activate automatically for conversations between devices running iOS 17.4 or later. The protocol is designed to re-establish cryptographic security periodically during long conversations — not just at the initial key exchange — so that even in adversarial scenarios where keys might somehow be exposed, the window of vulnerability is bounded.
Messages sent before the PQ3 update aren’t retroactively protected, of course. Nothing can undo communications that already exist. But any messages sent since the deployment are substantially better protected against future quantum decryption than they would have been under the previous protocol.
Apple’s deployment came alongside other major industry moves in post-quantum security. NIST published its first three finalized post-quantum standards in August 2024. Cloudflare reported in April 2026 that more than 65% of human traffic through its network is protected using post-quantum methods, targeting full migration by 2029. Google has set the same internal deadline.
What separates Apple’s approach isn’t simply the deployment of ML-KEM, which is becoming standard practice, but the depth of assurance behind it. Publishing the corecrypto source code, the formal verification tools, the Isabelle theories, and the Cryptol-to-Isabelle translator for independent evaluation is a meaningful transparency commitment. It invites external cryptographers to check the proofs themselves.
Formal verification at this level is rare outside of aerospace, defense, and payments infrastructure. Applying it to a consumer messaging platform’s cryptographic library, across the full chain from specification to silicon, represents a significant investment — one that reflects how seriously Apple is treating the transition rather than treating post-quantum encryption as a checkbox.
Safety is The Destination
It’s worth taking some time to process exactly what the PQ3 upgrade protects — and what it doesn’t.
The upgrade addresses the confidentiality of message content going forward. It does not address metadata — who is communicating with whom, and when — which remains visible to Apple’s infrastructure regardless of how the message content is encrypted. It also operates within iMessage’s existing trust model for device verification, which relies on Apple’s identity servers. Post-quantum key exchange doesn’t eliminate reliance on that trust hierarchy.
Additionally, while formal verification proves the implementation matches the specification, it assumes the compiler and underlying hardware behave correctly — a reasonable assumption, but not one that disappears from the security model entirely.
None of these caveats undermine the significance of the cryptographic migration. They’re relevant context for understanding what the upgrade does and doesn’t change.
The harvest now, decrypt later threat is not speculative. Encrypted data collected today can be held for years, waiting for quantum hardware to mature. Organizations that treat post-quantum migration as a future problem are, in effect, making a bet that adversaries won’t be patient — a bet that intelligence history suggests is unwise.
Apple’s PQ3 deployment demonstrates that production-scale post-quantum encryption is achievable now, across billions of devices, with rigorously verified implementations. The open-sourcing of the formal verification methodology advances the state of the art for the broader security community.
