Formal Verification Blueprint for Apple’s CoreCrypto

Apple’s recent corecrypto release marks a watershed moment for post‑quantum cryptography in consumer devices. By making the implementations of ML‑KEM and ML‑DSA—the algorithms standardized in FIPS 203 and FIPS 204—public, together with the mathematical proofs that certify their fidelity, Apple invites the broader security community to scrutinise the most widely deployed production‑grade post‑quantum code. The effort is not merely an open‑source gesture; it is the culmination of a multi‑year engineering programme that blends high‑performance hand‑optimised code with a rigorously engineered formal‑verification stack.

---

Why Formal Verification Matters for CoreCrypto

Corecrypto underpins encryption, hashing, random‑number generation, and digital signatures on over 2.5 billion active Apple devices. A single flaw could cascade through iMessage, VPN, TLS, and any third‑party app that relies on the library. Conventional testing—unit tests, fuzzing, simulation—can expose many bugs, yet it cannot guarantee that every possible input yields the mathematically correct output. Formal verification supplies that guarantee by constructing a mathematical proof that the implementation is equivalent to the specification.

If we can prove that the mathematical formula of our implementation is equivalent to that of its specification, then we know that the implementation will produce the correct output for every input.

Apple’s verification effort therefore targets three pillars:

1. Functional correctness – the algorithm’s output matches the FIPS spec.
2. Security hardening – no secret‑dependent timing or memory‑access patterns leak information.
3. Performance preservation – hand‑optimised ARM64 assembly remains provably faithful to the verified C reference.

---

The Verification Stack: From C to Isabelle

The verification pipeline weaves together three open‑source tools, each handling a distinct translation layer:

Layer	Tool	Role
Source code (C)	Cryptol (via manual translation)	Provides a functional model of the portable implementation that can be reasoned about symbolically.
Intermediate model	SAW (Software Analysis Workbench)	Checks that the Cryptol model faithfully implements the C code, generating proof obligations for each subroutine.
Formal proof assistant	Isabelle/HOL	Hosts the final proofs that the Cryptol model equals the formal specification derived from the FIPS documents.

The process begins with a manual translation of each corecrypto routine into Cryptol. SAW then verifies that the Cryptol model behaves identically to the original C, catching mismatches such as off‑by‑one errors or incorrect handling of carries in polynomial arithmetic. Because SAW lacks the expressive power to encode the full FIPS mathematics, the Cryptol model is fed into a custom translator—the cryptol‑to‑isabelle bridge built by Galois—that emits Isabelle definitions.

In parallel, Apple engineers painstakingly encode the FIPS specifications themselves into Isabelle. This step is deliberately manual to avoid any hidden translation bugs. With both sides expressed in the same proof language, the team writes incremental lemmas that relate each subroutine’s Isabelle model to the specification. Over 50 000 proof steps later, the full algorithm—key generation, encapsulation/decapsulation for ML‑KEM, and signing/verification for ML‑DSA—is shown to be mathematically equivalent to the standard.

---

Verifying Hand‑Optimised Assembly

The most performance‑critical kernels are rewritten in ARM64 assembly to exploit Data‑Independent Timing (DIT) and Pointer Authentication (PAC). Directly proving assembly against the high‑level spec would be infeasible. Instead, Apple adopts a refinement strategy:

1. Translate the verified C subroutine into Isabelle.
2. Translate the corresponding ARM64 routine into Isabelle as well.
3. Prove that the assembly implementation is refined by the C model.

Because the C model is already proven correct, the assembly inherits that assurance without the need for a separate, massive proof effort. This approach dramatically reduces the verification burden while preserving the performance benefits of hand‑tuned code.

---

Concrete Findings and Their Impact

The formal‑verification campaign uncovered subtle defects that would have escaped conventional testing:

• Missing range‑check step in an early ML‑DSA prototype could, under rare input patterns, produce out‑of‑range values and silently corrupt signatures.
• Third‑party proof discrepancy: a published proof for a particular parameter set contained an error; Apple’s translation exposed it, allowing the team to patch the proof for their own parameter choices.

Both issues were fixed before any code reached shipping devices, illustrating how formal methods act as a safety net for the most intricate arithmetic pathways—carry chains, polynomial reductions, and modular inverses.

---

Trade‑offs and Limitations

Formal verification is not a silver bullet. Apple’s methodology makes several explicit assumptions:

• Compiler correctness – the proof guarantees that the source C matches the spec; it trusts the compiler to emit faithful machine code for the verified C paths.
• Message‑size coverage – SAW cannot exhaustively verify all possible ML‑DSA message lengths; those cases remain covered by traditional testing.
• Proof effort – constructing and maintaining the Isabelle libraries required a dedicated team and a substantial engineering investment.

Nevertheless, the combination of formal proofs with exhaustive conventional testing yields a level of confidence that far exceeds what either technique could achieve alone.

---

Implications for the Wider Ecosystem

By publishing the corecrypto source, the Isabelle theories, the Cryptol models, and the cryptol‑to‑isabelle translator, Apple provides a reference verification framework that other vendors can adopt. The open‑source nature of the tools—Isabelle, SAW, Cryptol—means that the community can reproduce Apple’s results, extend the libraries to new algorithms, or adapt the pipeline for different architectures.

If more platform providers expose similar verification artefacts, the industry could converge on a shared assurance baseline for post‑quantum cryptography, accelerating adoption while reducing the risk of subtle implementation bugs that have historically plagued new primitives (e.g., early elliptic‑curve deployments).

---

Looking Ahead

Apple’s blueprint demonstrates that rigorous formal verification can be integrated into a fast‑moving product development cycle without sacrificing performance. The key take‑aways for any organisation aiming to follow this path are:

1. Invest early in a formal model of the specification; manual transcription errors are costly later.
2. Leverage existing proof assistants (Isabelle) and verification workbenches (SAW) rather than building tools from scratch.
3. Design for refinement, allowing hand‑optimised assembly to be proved against a verified high‑level model.
4. Combine proofs with conventional testing to cover aspects outside the formal model’s scope (e.g., compiler behaviour, side‑channel resistance).

As quantum‑resistant cryptography becomes a mandatory part of secure communications, the methodology outlined by Apple may become the de‑facto standard for ensuring that the mathematics of security translates flawlessly into the silicon that protects billions of users.

---

Further reading

• Apple’s Formal verification for Apple corecrypto paper (PDF) – deep dive into the Isabelle theories and proof structure.
• Galois’ SAW documentation – tutorial on verifying C code against Cryptol specifications.
• The Isabelle/HOL website – resources for learning the proof assistant used in the verification.
• NIST’s post‑quantum standardisation process – background on ML‑KEM and ML‑DSA.

---

Image credit: Apple Security Research