ML-KEM formal verification

Research, not an audit

These pages are research and development and may not match the live app. Do not treat this as an audit. Shared for testing and demo only. Please use responsibly.

Closed-source library (no source tree): a thin wrapper over portable libcrux-ml-kem 0.0.10 (the same crate pin as libsignal) plus hybrid HKDF-SHA256 and AES-256-GCM. Gallery: positive-intentions.github.io/ml-kem. This page reports tests and proofs with the same claim words as Signal Protocol (tested / modeled / type-checked / assumed / open). It is not an audit of the messenger and not a re-proof of Kyber.

Start from the verification report. This page has extract, lemma, and libcrux-pin detail.

Interface under test

ML-KEM-1024 only (Signal PQXDH production sizes). Secret keys are the expanded FIPS form, not a 64-byte seed.

$$\lvert \mathit{pk} \rvert = 1568,\quad \lvert \mathit{sk} \rvert = 3168,\quad \lvert \mathit{ct} \rvert = 1568,\quad \lvert \mathit{ss} \rvert = 32,\quad \lvert \mathit{seed} \rvert = 64.$$

Callers use generate_key_pair, encapsulate, decapsulate, and hybrid encrypt / decrypt. WASM and the gallery are tested (WASM) or demos — not extracted.

Production enables libcrux-backend. Extraction builds without it. Stubs use AbstractKem axioms.

Hybrid info string (19 bytes): $\texttt{ML-KEM-1024-AES-GCM}$.

$$\begin{aligned} (\mathit{ct}, \mathit{ss}) &= \mathrm{Encaps}(\mathit{pk}), \\ k &= \mathrm{HKDF}(\mathit{ss},\; \mathit{salt},\; \texttt{ML-KEM-1024-AES-GCM}), \\ c &= \mathrm{Enc}_{k,\mathit{iv}}(m). \end{aligned}$$

Executable tests

Suite	What it covers	Gate
Rust tests (backend on)	Keygen, encap/decap round-trip, hybrid round-trip, empty plaintext, tamper, wrong key, bad IV/salt, unreduced public key, invalid private key bytes	Must pass (CI)
Rust tests (backend off)	Length and field-rejection paths on the extractable stubs	Exist locally; CI runs the default libcrux-backend feature only
Line coverage	ml-kem-core (no coverage(off) sites)	100% lines
Clippy / rustfmt	Core crate	Must pass
WASM	wasm-pack test --node	Must pass

Coverage includes backend try_from error paths (wrong-size public/private key and ciphertext).

Wrapper lemmas

Hand-written AbstractKem (F*, Rocq, Lean) states assumptions and the glue properties.

Assumed

Assumption	Formal content
KEM correctness	$\mathrm{Decaps}(\mathit{sk}, \mathrm{Encaps}(\mathit{pk})) = \mathit{ss}$ for a generated pair $(\mathit{pk}, \mathit{sk})$
Public-key validation	FIPS 203 §7.2-style check before encapsulate (libcrux in production)
HKDF	Deterministic expand; info as above
AES-256-GCM	$\mathrm{Dec}_{k,n}(\mathrm{Enc}_{k,n}(m)) = m$
fill_random	The CSPRNG fills the buffer

KEM correctness is not proved in this library. Portable lattice math is cited from the libcrux pin below — not linked as a lemma. ind_cpa is 0/21 at that pin, so there is no in-tree ML-KEM IND-CPA story. Decaps(Encaps)=ss is correctness, not secrecy.

Length guards (backend split)

These lemmas live on the spec, not on the production libcrux-backend functions. F* proves them (precondition includes ValidatePK). Rocq proves a length-only variant (no ValidatePK in those lemmas). Lean states them as axioms.

The encapsulate precondition is

$$\mathrm{pre}_{\mathrm{encap}}(\mathit{pk}) \iff \lvert \mathit{pk} \rvert = 1568 \;\wedge\; \mathrm{ValidatePK}(\mathit{pk}).$$

Then:

$$\lvert \mathit{pk} \rvert \neq 1568 \implies \mathrm{pre}_{\mathrm{encap}}(\mathit{pk}) = \mathsf{false}.$$

Same shape for decapsulation: a wrong-length $\mathit{sk}$ or $\mathit{ct}$ fails before the KEM is invoked.

$$\lvert \mathit{salt} \rvert = 16 \;\wedge\; \lvert \mathit{iv} \rvert = 12 \implies \text{hybrid salt/IV sizes match the implementation}.$$

Assumed hybrid round-trip

$$\mathrm{Dec}_{k,\mathit{iv}}(\mathrm{Enc}_{k,\mathit{iv}}(m)) = m \;\wedge\; \mathrm{Decaps}(\mathit{sk}, \mathit{ct}) = \mathit{ss}$$

under the KEM, HKDF, and AEAD axioms, for $\lvert \mathrm{salt} \rvert = 16$ and $\lvert \mathrm{iv} \rvert = 12$. That is an axiom on the spec, not a derived F* proof of the extracted encrypt / decrypt functions.

Symbolic models (ProVerif)

Two processes. $\mathrm{HKDF}(\mathrm{salt}, \mathrm{ikm}, \mathrm{info})$ matches Hkdf::new(Some(salt), ikm).expand(info, 32).

Model	Queries
Hybrid security	Attacker does not obtain the secret plaintext; does not obtain KEM shared-secret / AES-key material; $\mathrm{event}(\mathsf{decrypted}(m)) \implies \mathrm{event}(\mathsf{encrypted}(m))$
Hybrid round-trip	Honest Alice and Bob recover the same $m$

These assume KEM and AEAD equations. They do not prove libcrux or AES-GCM. The models are not machine-linked to the Rust. The KEM process treats the shared-secret argument as encapsulation coins (kem_enc(pk, ss)), not “encapsulate draws 32 random bytes after validation.” The AEAD equation is idealized: it is not IND-CCA, nonce-misuse resistance, or key commitment. Production hybrid uses a random salt/IV; the symbolic model does not stress reuse.

Extracted Rust (hax → F*, Rocq, Lean)

Backend	Automated job	Depth
F*	Full extract	Type-checks extracted ml-kem-core (types, error, crypto stubs, KEM, hybrid, lib) plus AbstractKem
Rocq	Full extract	Type-checks the same modules after a standalone prelude; functions that use Rust ? become axioms (generate_key_pair, encapsulate, decapsulate, derive_aes_key, encrypt, decrypt) because hax emits ill-typed ControlFlow nesting
Lean	Extract + spec	Extraction must succeed; Lean type-checks AbstractKem. The extracted Lean file depends on Hax/Aeneas/Mathlib and is not built in this job

F* uses replace_body so stub parameter names must match hax binders (unused _x would become e_x and break the body).

Pinned libcrux proofs

Lattice math is not re-proved here. The wrapper pins crates.io libcrux-ml-kem 0.0.10.

Field	Value
crates.io checksum	1d8160f7d64fd2716b4fd05cc886a042f8dcda18d9206c0d506e2c67bdf97daa
Tag	libcrux-ml-kem-v0.0.10
Commit	c5fb80f37530ee9b2df9501ae5ff8cb4a973a4bd
F* at that revision	v2026.03.24
hax-lib at that revision	0.3.7

CI checks out that commit. It does not follow libcrux main. Only portable mlkem1024 is enabled (no AVX2 / Neon). The job does not check that the crates.io 0.0.10 tarball equals commit c5fb80f…. Wrapper Cargo.toml uses hax-lib = "0.3"; the pin’s libcrux revision uses hax-lib 0.3.7.

verify:host:full is ProVerif + F* + Rocq + Lean. It does not run this libcrux job.

Upstream portable status at that commit (verification_status.md):

File	Panic-free	Correct
arithmetic	13/13	13/13
ntt	10/10	10/10
serialize	22/22	22/22
compress	6/6	6/6
sampling (portable)	1/1	1/1

Generic modules still open at that commit include ind_cpa (0/21 panic-free and correct), generic sampling (0/5 — a different libcrux module than the portable row above), and parts of serialize / matrix / ntt. Neon is unverified; this wrapper does not build Neon.

Upstream’s own workflow at that revision extracts and runs ./hax.py prove --admit (lax). The full ./hax.py prove job is commented out upstream. This library’s libcrux job runs extract and ./hax.py prove on the pin; admitted functions stay upstream facts.

Automated jobs

Job	What it runs
Format, Clippy, cargo test	Production ml-kem-core
Coverage	100% lines on ml-kem-core
WASM	Node wasm-pack
ProVerif	Both hybrid models
F*	Full extract and check
Rocq	Extract, patch, type-check
Lean	Extract + AbstractKem
libcrux	Pin → checkout → extract / prove in libcrux-ml-kem

What this does not prove

• WASM bindings or the gallery
• AES-GCM or HKDF internals
• ML-KEM lattice math inside this library (that is the libcrux pin)
• AVX2 or Neon libcrux paths
• Generic ind_cpa at the pin
• PQXDH, the recipient cascade, or the Glitr messenger
• Refinement from the libcrux-backend production build to AbstractKem

Next: Cryptography — how these libraries sit in the product cascade.