VRIL-KEM v1.2-rc2: A Complete EasyCrypt Formal-Verification Architecture

A cryptographic library can be tested, benchmarked, and audited by experts, and still rest on an argument that turns out, under formal scrutiny, to have a gap. The purpose of machine-checked verification is to remove the gap between “we believe this is secure” and “a proof assistant has confirmed the security argument holds, line by line, against a precisely stated assumption.” EasyCrypt is the tool the cryptographic research community uses to close that gap, and it is the tool behind the central change in this release.

When VRIL-KEM v1.2-rc1 shipped, the team was explicit about what was missing. The first item under the README's “Honest Disclosures” section read: no formal EasyCrypt security proofs have been completed yet; the IND-CCA2 argument is mechanically sound via the Fujisaki-Okamoto structure, but the full CVKDF chain has not been formally verified; proofs are planned for v2.0. v1.2-rc2 brings that work forward by more than a full version.

What Ships in v1.2-rc2

The cryptographic core is unchanged from rc1. The same three stable parameter sets — VRIL-KEM-1024-3, VRIL-KEM-2048-5, and the default VRIL-KEM-4096-7 — ship across the same four build backends (ref/, avx2/, ct/, mem/) over the same ring algebra, R_q = Z_q[X]/(X^N + 1) with q = 12,289. The three novel constructions are intact: the seven-layer Fibonacci-weighted HI-Gaussian sampler, the Outer Harmonic Commitment, and the Centripetal Vortex KDF.

What is new is the proof/ tree. The release validation report records that every stable parameter set passes the full functional test suite across all in-scope backends — 100 KEM iterations per category, zero failures — and, for the first time, that the EasyCrypt formal proof tree compiles end-to-end: zero errors, with a single documented global-axiom warning and nothing else outstanding. That last clause is the heart of this release, and it deserves to be unpacked honestly.

What Is Actually Formalized

The architecture is modular, mirroring the structure of the implementation rather than collapsing it into a single monolithic claim. It is organized into theories, a specification, security proofs, and an implementation boundary:

• Ring algebra and NTT (theories/VRILRing.eca) — the polynomial ring R_q = Z_q[X]/(X^N+1), number-theoretic transform correctness, and module-vector operations, formalized as the algebraic substrate everything else stands on.
• M-LWE hardness (theories/MLWE.eca) — the decisional Module-LWE game with a quantitative advantage bound, the assumption to which all security ultimately reduces.
• The HI-Gaussian noise model (theories/HIGaussian.eca) — sub-Gaussianity of the seven-layer Fibonacci sampler, a smudging bound, and a concrete decryption-failure probability δ derived by Chernoff and union bounds. This is what turns the noise distribution from a heuristic into a quantity that appears, with a number attached, in the final security statement.
• The CVKDF (theories/CVKDF.eca) — the centripetal spiral key derivation function modeled in the lazy random-oracle model, with a quantitative one-wayness bound. rc1 could only argue the CVKDF's 2^-128 inversion estimate informally; rc2 states it as a bound inside the proof system.
• The Outer Harmonic Commitment (theories/OHC.eca) — binding and hiding games for the post-decapsulation integrity token that closes the ciphertext component-substitution surface.
• The KEM specification (spec/VRIL_KEM_Spec.eca) — a full KEM module realizing the upstream KeyEncapsulationMechanisms.Scheme interface, so the proofs are stated against the same abstract scheme type the wider EasyCrypt ecosystem uses rather than a bespoke one.
• The security proofs (security/) — IND-CPA structure, the IND-CCA2 concrete-bound lemma, and the binding hierarchy.
• The Jasmin boundary (impl/VRIL_Jasmin_Equiv.eca) — the source-level specification-to-implementation equivalence boundary, the seam where a verified specification is tied to verified machine code.

The tree is verified against the genuine upstream EasyCrypt standard library and a quantum Fujisaki-Okamoto transform clone, with external dependencies — the EasyCrypt stdlib, the EasyCrypt-KEMs library, and formosa-mlkem — vendored as git submodules under proof/upstream/. This matters: a proof that only typechecks against a hand-rolled, weakened standard library proves very little. Building on the same foundations the formally verified ML-KEM work uses is what makes the result meaningful. To the team's knowledge this is the first formalization of its kind for a novel post-quantum KEM outside the NIST finalist ecosystem.

The Bounds, Stated Concretely

Formal verification is only as useful as the statement it proves. The value of this architecture is that the security claims are no longer prose — they are bound expressions a machine has checked for consistency. The four headline statements are:

• IND-CPA: the adversary's distinguishing advantage is at most 2 · mlwe_eps.
• IND-CCA2: the advantage is at most 2 · mlwe_eps + δ + q_RO / 2²⁵⁶, where δ is the formalized decryption-failure probability and q_RO counts random-oracle queries.
• Leakage binding (LEAK-BIND-K-CT): at most ohc_bind_eps + cvkdf_ow_eps — the shared-secret-to-ciphertext binding reduces jointly to OHC binding and CVKDF one-wayness.
• Malleability binding (MAL-BIND-CT-PK): at most mlwe_eps + ohc_bind_eps.

The IND-CCA2 bound and the full binding hierarchy — honest binding, leakage binding, and malleability binding — are checked EasyCrypt lemma bodies. There are no admit tactics and no sorry placeholders anywhere in the VRIL proof sources. In a proof assistant, an admit is the way a developer tells the checker “assume this step without justification”; a proof littered with them is a proof in name only. The validation report confirms their absence, and lists each checked lemma by name, including the non-negativity of the failure bound that the IND-CCA2 statement depends on.

Honest Status: The One Global Axiom

The release does not claim a finished end-to-end machine proof, and saying otherwise would betray the standard rc1 set. There is exactly one global-axiom warning in the tree, and it sits in security/VRIL_PKE_INDCPA.eca: the IND-CPA game-hop reduction body, vril_pke_indcpa.

What this means precisely: the IND-CPA bound expression is stated, and every downstream theorem that consumes it — including the checked IND-CCA2 and binding lemmas — is verified relative to it. What remains is the proof body of the game hop itself: the byequiv and smt argument that ties the scheme's IND-CPA game to the MLWE_Real / MLWE_Ideal distinguisher. In other words, the scaffolding and the consequences are checked; the single reduction at the base of the IND-CPA layer is asserted as an axiom pending its proof body. It is the difference between a fully closed proof and a proof with one clearly marked, well-understood hole at a known location — not a hole hiding in the conclusions.

The rest of the honest disclosures from rc1 still stand and are worth repeating, because none of them are fixed by a proof tree:

• Constant-time behavior is compiler-dependent on some targets; for side-channel-sensitive deployments, use the ct/ backend explicitly.
• Key and ciphertext sizes remain large relative to ML-KEM (FIPS 203) — VRIL-KEM-4096-7 still carries a 50 KB public key and a 42 KB ciphertext. That is the cost of the security margin.
• The library has not been independently peer-reviewed. It remains a research prototype and is not recommended for production use without independent audit. A machine-checked proof of a security reduction is a strong signal; it is not a substitute for review of the implementation, the parameter choices, or the threat model.

Why the Acceleration Matters

rc1's roadmap placed formal verification at v2.0 — a deliberately conservative target, because formalizing novel constructions like the CVKDF and the HI-Gaussian sampler is genuinely hard work with no off-the-shelf templates. Delivering the architecture at rc2 changes the character of the project's remaining roadmap. The hardest structural decisions — how to model the spiral KDF in the lazy ROM, how to express the seven-layer noise distribution's failure probability as a checkable bound, how to attach the whole thing to the upstream Scheme interface — are now made and checked. What is left at the IND-CPA layer is a single, well-scoped reduction body, not an open research question.

Integration Is Unchanged

Nothing about the verification work alters the public surface. The API remains NIST PQC competition-compatible: any library using the standard triple — crypto_kem_keypair, crypto_kem_enc, crypto_kem_dec — adapts to VRIL-KEM with no protocol changes, and the shared secret is 32 bytes in every parameter set. The Go hybrid package still exposes VRIL-KEM + X25519 combined key exchange for defense-in-depth against an adversary who breaks either primitive alone.

The source, the release artifacts, the pre-built libraries, the NIST KAT response files, and now the complete EasyCrypt proof tree are all at github.com/VRIL-LABS/vril-kem. The validation report sits under dist/ for anyone who wants the per-backend, per-parameter-set results without rebuilding from source.

What Comes Next

The immediate work item is closing the one global axiom: completing the IND-CPA game-hop proof body against MLWE_Real / MLWE_Ideal, which would make the tree a fully closed end-to-end machine proof. Beyond that, the roadmap is the one rc1 named — independent security review, and the VRIL-MESH integration that uses VRIL-KEM as its key-exchange primitive at every connection layer. The same CVKDF cascade formalized here also governs the entropy pipeline in VRIL-ZIP, which is the point of doing this work once and carefully: one cascade, two applications, a single body of formal verification that both can draw on.