CVE-2026-72711 — Lean 4 Kernel Soundness Bug: Inference Cache Poisoning

Proving 0 = 1 axiom-free via opaque declaration FVar cache poisoning.

Field	Value
Bug report	leanprover/lean4#14484
Fix	leanprover/lean4#14498
Affected	Lean 4 ≤ v4.31.0 / all prior versions
Fixed in	nightly 2026-07-23+, backported to v4.32.1 and v4.33.0
CVSS 3.1	AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1
CWE	CWE-488 (Exposure of Data Element to Wrong Session), CWE-20 (Improper Input Validation)
CVE	CVE-2026-72711

Vulnerability Summary

The Lean 4 kernel's environment::add_opaque path does not call check_no_metavar_no_fvar on the declaration body — unlike definitions and theorems, which perform this closure check before type-checking the value.

An adversarial metaprogram exploits this omission through inference cache poisoning:

1. Priming — A crafted type expression (cachePrimingType) is a closed beta-redex definitionally equal to False. While type-checking it, the kernel creates a temporary local declaration _kernel_fresh.2 : False and caches its inferred type in the type_checker instance's inference cache.

2. Context invalidation — The local context is restored (the temporary variable is removed), but the inference cache persists on the same type_checker instance. The cache entry is now stale — it maps an identifier that no longer refers to anything in scope.

3. Exploitation — The opaque declaration's value is an Expr.fvar pointing at the stale identifier. The cache lookup fires before the FVar branch checks local-context membership, returning False as the type without ever detecting the unbound variable.

The result is a kernel-accepted opaque constant of type False, from which 0 = 1 follows trivially.

The exploit:

• Uses only the checked addDecl kernel path
• Runs with --trust=0 (maximum checking)
• Reports no axioms via #print axioms
• Uses no sorry, unsafeCast, debug.skipKernelTC, FFI, or .olean tampering
• Passes leanchecker --fresh replay

Usage

docker build -t lean-cve-poc-14484 .
docker run --rm lean-cve-poc-14484

Expected output on a vulnerable Lean version:

[*] Running CachePoisonFalse.lean with --trust=0 ...
kernel accepted bad : False
'bad' does not depend on any axioms
'assumptionFreeFalse' does not depend on any axioms
'zero_eq_one' does not depend on any axioms

[!] VULNERABILITY CONFIRMED

    zero_eq_one : 0 = 1
    Depends on: no axioms

    Bug class:  Inference cache poisoning (CWE-488)
    Root cause: missing check_no_metavar_no_fvar in add_opaque
    Bug report: https://github.com/leanprover/lean4/issues/14484
    Fix:        https://github.com/leanprover/lean4/pull/14498

On a patched Lean version, the kernel rejects the ill-typed opaque declaration and the script reports the version is not vulnerable.

Impact

Any system that trusts Lean's kernel-checked proofs as ground truth is affected. This includes:

• Formally verified software: compilers, cryptographic libraries, smart contracts, avionics, automotive — any safety case built on a Lean proof is invalid if built with an affected version.
• Proof-carrying code: a malicious dependency in a Lake package can silently introduce unsound declarations that downstream code uses.
• Independent checkers: the reporter confirmed leanchecker --fresh replay also accepts the exploit. The comparator export format cannot express an FVar, so that validation path is unaffected.
• AI-generated proofs: systems like AlphaProof, DeepSeek-Prover, and Kimina-Prover that use Lean as a trusted backend could produce proofs that exploit kernel bugs rather than prove theorems.

Technical Details

Root Cause

In src/kernel/environment.cpp, the add_opaque function checks the opaque value's type but does not perform the closure check:

environment environment::add_opaque(declaration const & d, bool check) const {
    scoped_diagnostics diag(*this, check);
    opaque_val const & v = d.to_opaque_val();
    if (check) {
        type_checker checker(*this, diag.get());
        check_constant_val(*this, v.to_constant_val(), checker);
        // ← MISSING: check_no_metavar_no_fvar(*this, v.get_name(), v.get_value());
        expr val_type = checker.check(v.get_value(), v.get_lparams());
        // ...
    }
}

Both add_definition and add_theorem call check_no_metavar_no_fvar on their values before type-checking them. The omission in add_opaque is the entry point.

Cache Poisoning Mechanism

The inference cache in type_checker maps expressions to their inferred types. In infer_type_core, the cache lookup:

auto it = m_infer_type_cache[binfo_idx(bi)].find(e);
if (it != m_infer_type_cache[binfo_idx(bi)].end())
    return it->second;

fires before the FVar branch validates local-context membership:

case expr_kind::FVar: {
    optional<local_decl> d = m_lctx.find_local_decl(e);
    if (!d) throw_kernel_exception(...);
    return d->get_type();
}

The attacker controls cache population through the type expression, making the stale entry's name (_kernel_fresh.2) predictable and targetable.

Comparison with #14576

Aspect	#14484 (this bug)	#14576
Bug class	Cache poisoning	Type confusion via projection validation
Entry point	add_opaque missing closure check	Nested inductive phantom parameters
Cache involved	Yes — inference cache	Yes — expr hash comparison
Affects leanchecker	Yes	Yes
Affects comparator	No (FVar not expressible)	Yes

Related Work

• endrazine/lean-cve-poc — PoC for the #14576 nested inductive projection bug (same repo structure)
• lean4lean soundness fix — lean4lean was independently affected by the same cache poisoning bug

Credits

• Bug discovery: Patrick Hulin (@phulin), with assistance from GPT-5.6 Sol
• Kernel fix: Joachim Breitner (@nomeata), PR #14498
• PoC packaging: Jonathan Brossard (@endrazine)