What a Formally Verified ML-KEM Actually Proves: Specifications, Models and the Gaps Between Them

A building inspection certificate is worth exactly what it says: which floors were inspected, against which edition of the code, by whom, and with which items excluded. Nobody reads 'inspected' as 'safe in every respect'. Cryptographic verification deserves the same reading, and ML-KEM is now the clearest place to practise it, because several independent teams have verified it in very different ways and published what they proved. Those efforts are a genuine advance; some of the subtle bugs they rule out have broken real implementations. But the word 'verified' compresses a long sentence, and the parts it leaves out are where deployments still go wrong.

A verification claim is a sentence with five parts

Formal verification proves, with a machine-checked argument, that a program or a design has a stated property for every input the theorem covers, rather than for the inputs someone happened to test. That much is familiar. What is easy to forget is how many choices sit inside a single verified claim. Each one names a property, the code or design it is about, the specification that defines correct behaviour, the model of the machine or language the reasoning assumes, and the proof tool whose checker accepted the argument. Change any of the five and the claim changes.

The mlkem-native project, a C and assembly implementation of ML-KEM maintained in the open-source Post-Quantum Code Package project, publishes a soundness document that makes this structure explicit and names three gaps. Gap A asks whether the formal specification captures what users actually want from the real system. Gap B asks whether the formal model of the code and its execution faithfully reflects the compiled program on real hardware. Gap C asks whether the proof infrastructure, the kernel and solvers that accepted the argument, is itself sound. The document is unusual in candour, and its framework applies to every verified implementation, not only its own.

For ML-KEM the five parts vary widely across efforts. Some proofs are about the specification and say nothing about code; some are about code and assume the specification is right; some cover one processor family's assembly and none of the C that calls it. Reading a claim well means filling in all five parts before deciding what it buys.

Four kinds of statement, three verified ML-KEMs

Verified ML-KEM work makes four distinct kinds of statement. A specification-security proof shows that the algorithm as specified meets IND-CCA, indistinguishability under chosen-ciphertext attack, and a correctness bound on decapsulation failure, from a hardness assumption. A functional-correctness proof shows that an implementation computes exactly what a formal specification says. A safety proof shows that code has no memory errors, integer overflows, panics or other undefined behaviour. A timing proof shows that execution time does not depend on secret values, within some model of the processor.

The EasyCrypt development of Almeida and colleagues, published at CRYPTO 2024, is the most complete on the first axis. It machine-checks the correctness and passive security of the underlying public-key scheme, a formalization of the relevant Fujisaki-Okamoto transform in the random-oracle model, and the resulting IND-CCA security of the ML-KEM specification, with concrete bounds down to a variant of the Module-LWE problem. It also presents two Jasmin implementations proved functionally equivalent to that specification and constant-time, so the security theorem carries over to them. The libcrux library verifies its Rust code by translating it with the hax toolchain into F*, a proof-oriented language; its documentation states that the portable and AVX2 code for field arithmetic, NTT polynomial arithmetic, serialization and the generic high-level algorithms is verified, and it uses Rust types to reject operations on secret values that are known to take data-dependent time, describing the resulting constant-time behaviour as best effort. mlkem-native proves all of its core C code memory-safe and free of integer overflow with CBMC, a bounded model checker, and proves its AArch64 and x86_64 assembly functionally correct, memory-safe and secret-independent in timing with the HOL Light theorem prover and the s2n-bignum processor models.

Composition is the reason the first two axes matter together. A security theorem about a specification protects deployed code only if the code provably computes that specification; a correctness proof protects security only if the specification it targets is secure. The EasyCrypt work closes that loop for its own Jasmin implementations. The other efforts rely, for security, on the published pen-and-paper analysis of the standard, and prove that their code matches a specification of it. Both are legitimate positions, but they are different positions, and a reader comparing libraries should know which one each takes.

The table that follows places each effort on the four axes, using its authors' own descriptions. The striking feature is how little the columns overlap. No single effort is the most complete on every axis, and a library that ships one effort's code inherits that effort's column, not the union of all three.

Gap A: is the specification the standard?

A functional-correctness proof shows that code equals a specification, and the specification is written by people. It is, in effect, a second implementation of the standard, in a proof language rather than a production language, and it can be wrong in the same ways. The libcrux repository shows this concretely. Its F* specification of ML-KEM was first committed on 12 August 2024. On 4 March 2026 a commit titled 'Fix three bugs in ML-KEM F* spec' corrected the zeta index used in one layer of the number-theoretic transform, the rounding constant in decompression, which had been copied from the compression function, and a missing final scaling step in the inverse transform. All three made the specification compute something other than FIPS 203.

The Rust implementation had been correct throughout; the disagreement was between the specification and the standard, and it survived because, in the project's own build files as of late 2025, the module whose proof would have connected the implementation's encryption routine to that part of the specification was listed among the admitted modules, those whose proofs are assumed rather than checked. That combination, a specification error plus an admitted proof, is exactly what a 'verified' badge cannot reveal on its own. An independent review in early 2026 drew public attention to these gaps, and the fix commit, in a detail worth noticing for anyone using AI tooling in proof work, credits an AI coding assistant as co-author in its metadata.

The standard itself also moved. FIPS 203's appendix records that the initial public draft had inadvertently swapped the indices of the public matrix in key generation and encryption, and the final version changed them back to match the original Kyber submission. A specification faithfully formalized from the draft would have certified implementations of a function the final standard does not compute. Two disciplines follow. Formal specifications should be executable and run against NIST's published test vectors, which catches transcription errors before they become the foundation of a theorem; and every claim of verification should list its admitted modules and the edition of the standard its specification follows.

Gap B: is the model the machine?

Every proof reasons about a model: of the C language, of Rust's operators and core library, or of a processor's instruction set. mlkem-native's assembly proofs are notable because they are done at the object-code level against formal models of the Arm and x86 architectures, which removes the compiler from the trusted path for those routines. Even so, its soundness document lists the remaining risks plainly: the fidelity of the instruction-set models, the reassembly of verified object code into the shipped library, instructions the models omit, and hardware that does not implement its own architecture specification correctly.

Timing claims are the most model-sensitive. The s2n-bignum notion of constant time, which mlkem-native uses, flags instructions known to vary in timing, such as branches, memory accesses and divisions, and proves that the sequence of those events depends only on public values. The document states that this cannot guarantee constant-time execution in hardware: speculative execution and frequency-scaling effects of the Hertzbleed kind are outside the model, and power and electromagnetic channels are out of scope entirely. The methods for verifying constant-time behaviour, statistical, static and dynamic, form a field of their own; the point here is narrower. A timing theorem is a theorem about a model, and the model is a deliberate simplification.

C code adds another layer. CBMC reasons about a model of C semantics, and the compiled binary is produced by a compiler the proof does not cover. mlkem-native mitigates this with value barriers and with constant-time tests across many compilers and optimization levels, run, as the project notes, on x86_64 and AArch64 in default configurations. Those are tests, valuable and repeatable, but a different kind of evidence from proofs.

Gap C: who checks the checker?

A machine-checked proof is trustworthy to the extent that the machine that checked it is. Proof assistants are designed so that only a small kernel needs to be trusted: HOL Light accepts a theorem only if its compact logical core does, and the same design underlies other assistants. That is a strong position, but the trusted base is never only the kernel. mlkem-native's soundness document lists the HOL Light kernel and the OCaml runtime it runs on for the assembly proofs, and CBMC with its satisfiability and SMT solvers for the C proofs, where a solver bug could in principle make an unprovable property appear proved.

Translation tools add their own entries. A Rust-to-F* pipeline such as hax must model Rust's arithmetic and core library in the target language, and those models are hand-written and trusted; a mismatch between the model of an operator and its real behaviour would make a correct-looking proof describe the wrong program. EasyCrypt and Jasmin have a similar structure, with a certified compiler path for Jasmin. None of these components is known to be unsound, and each has been scrutinised far more than ordinary software. But the list belongs in the claim.

Proofs also have to keep up with code. A verified library changes with every optimization, platform port and dependency upgrade, and a proof that ran once establishes nothing about the next release unless it runs again. mlkem-native's soundness document is frank that it has no automatic check, at present, that every function is covered by a specification, so a new routine could slip through unproved. Proofs that run in continuous integration on every change, with coverage reported, are the difference between a verified release and a verified project.

The practical consequence is diversity rather than doubt. An ML-KEM implementation whose functional correctness is proved in one tool chain and whose test vectors are checked by an independent implementation, written in a different language by different people, is protected against a class of errors, including toolchain and specification errors, that neither form of evidence covers alone.

What no ML-KEM proof states

Every verified claim above is a statement about the algorithm or about code that computes it. None of them, as their authors describe them, is a statement about the properties that decide whether a deployment is safe once the algorithm is correct. The EasyCrypt theorem establishes IND-CCA for honestly generated keys; it does not address binding, the question of whether a shared secret identifies the public key and ciphertext that produced it, and known binding results show that ML-KEM's strongest form of binding fails for attacker-built keys. A functional-correctness proof of decapsulation says nothing about whether the caller ran the FIPS 203 input checks, whether a private key was imported from an untrusted expanded encoding, or whether the random bit generator met the parameter set's security strength.

The interaction with key formats is instructive. A decapsulation routine proved functionally correct computes exactly what the FIPS 203 decapsulation algorithm says for the key it is given, and that algorithm uses the public-key copy, its hash and the rejection secret stored in the key without recomputing them. A forged hash is therefore processed perfectly correctly, and the proof is no less valid for it. Correctness proofs faithfully reproduce the standard's own assumptions; they cannot add protections the standard places outside the algorithm itself, such as the input checks it requires but allows to be performed elsewhere, including the hash check on an imported key.

Even the security theorem has its own scope. The EasyCrypt development formalizes the Fujisaki-Okamoto transform in the random-oracle model, in which hash functions are treated as ideal and are queried classically. An adversary with a quantum computer could query a hash function on a superposition of inputs, and arguments against that adversary are made in the quantum random-oracle model, which is a different and harder theorem. The paper's claim is precise about this; summaries of it are not always.

There is also the interface. A verified core is wrapped by an API, error handling, key serialization and, often, language bindings. The libcrux documentation marks some features, such as its pre-standard Kyber implementation, as unverified, and mlkem-native lists backends for platforms other than AArch64 and x86_64 as outside its proofs. Build configuration decides which code path is compiled in. A verified library built with a different backend, or called through an unverified binding, is no longer the artifact the proof describes.

None of this diminishes the work. Verified ML-KEM removes whole classes of defects, including the rare arithmetic overflows that mlkem-native's documentation identifies as the most subtle bugs in optimized implementations, and the timing leaks that have repeatedly appeared in unverified code. It does mean that 'formally verified' should be the beginning of a dependency review, not its conclusion.

Reading verification evidence for an agent platform

AI agent platforms raise the stakes of reading these claims correctly. Agents run across heterogeneous fleets, so the same library may execute verified x86_64 assembly on one host, verified AArch64 assembly on another, and an unverified backend on a third. Agent runtimes often reach cryptography through bindings from Python, JavaScript or other languages, which are rarely part of any proof. And dependency decisions are increasingly made, or drafted, by AI coding agents that read a project's badge and summary. Each of those paths converts a scoped claim into an unscoped one unless someone restores the five parts.

The same agents are now part of proof engineering itself. The specification fix described earlier was committed with an AI assistant credited as co-author, and AI tools are increasingly used to draft proofs and specifications. The trust model survives this, because a proof kernel rejects an invalid argument whoever wrote it. What it does not check is whether the specification an AI drafted, or repaired, is the standard. That judgement remains a human review against FIPS 203 and NIST's test vectors, and an agent platform that adopts AI-assisted verification should require it explicitly.

A workable discipline is to record, for each cryptographic dependency an agent platform ships, the verification claim in its five parts, the admitted or excluded modules, the backend actually compiled and executed on each host type, the independent test-vector evidence, and the deployment properties, binding, input checks and key provenance, that the platform must supply itself. That record is short, it survives library upgrades, and it turns a badge into evidence.

Practitioner Toolkit

Copy-paste, strictly defensive artifacts you can use today. Nothing here attacks a real system.

Glossary

Formal verification

Proving with a machine-checked argument that a design or program has a stated property for every input the theorem covers.

Specification-security proof

A proof that an algorithm, as specified, meets a security definition such as IND-CCA from a hardness assumption.

Functional correctness

The property that an implementation computes exactly what its formal specification defines.

Admitted module

A part of a verification development whose proof is assumed rather than checked.

EasyCrypt

A proof assistant for game-based cryptographic security proofs.

Jasmin

A low-level programming language for high-assurance cryptographic code with a verified compilation path.

hax and F*

A toolchain that translates Rust into F*, a proof-oriented language in which correctness and safety are proved.

CBMC

The C Bounded Model Checker, used to prove absence of undefined behaviour such as out-of-bounds access and integer overflow.

HOL Light

A theorem prover with a very small trusted kernel, used with processor models to verify assembly code.

Trusted computing base (of a proof)

The kernels, solvers, runtimes and models that must be correct for a machine-checked proof to mean what it says.

Random-oracle model

A proof setting that treats hash functions as ideal random functions; quantum attackers querying them in superposition need a stronger model.

References

1. NIST FIPS 203, Module-Lattice-Based Key-Encapsulation Mechanism Standard (2024), including Appendix C
2. Almeida et al., Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt (CRYPTO 2024, IACR ePrint 2024/843)
3. Barbosa et al., SoK: Computer-Aided Cryptography (IEEE S&P 2021, IACR ePrint 2019/1393)
4. Schmieg, Unbindable Kemmy Schmidt: ML-KEM is neither MAL-BIND-K-CT nor MAL-BIND-K-PK (IACR ePrint 2024/523)
5. Cremers, Dax and Medinger, Keeping Up with the KEMs (ACM CCS 2024, IACR ePrint 2023/1933)
6. mlkem-native, Formal Verification: Scope, Assumptions, Risks (SOUNDNESS.md)
7. libcrux repository, commit 2928456: Fix three bugs in ML-KEM F* spec (2026)