CVE-2026-72844: Lean 4 Kernel Soundness Bug

Proving 0 = 1 axiom-free via nested inductive projection validation bypass.

Vulnerability Summary

The Lean 4 kernel does not verify that the structure named in a projection expression matches the type of the value being projected, and environment::add_inductive in src/kernel/inductive.cpp did not type check the nested inductive applications that are replaced by auxiliary types, so their parametric arguments escaped checking.

A metaprogram running in the Lean process can register an ill-typed nested inductive whose constructor applies a .proj C 0 projection to a value of the unrelated type W, and the kernel admits the declaration through the ordinary checked addDecl path at maximum kernel checking. The result is a type confusion yielding a proof of False that carries no axioms, from which any proposition — including 0 = 1 — can be derived.

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

Usage

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

Expected output on a vulnerable Lean version:

[*] Running ZeroEqOne.lean with --trust=0 ...
'bad' does not depend on any axioms
'boom' does not depend on any axioms
'zero_eq_one' does not depend on any axioms
zero_eq_one : 0 = 1

[!] VULNERABILITY CONFIRMED — CVE-2026-72844

    zero_eq_one : 0 = 1
    Depends on: no axioms

On a patched Lean version, the kernel rejects the ill-typed inductive 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 same class of bug was shown to also bypass the Nanoda independent type checker.

Technical Details

The root cause is in the kernel's handling of nested inductive types. When eliminating a nested occurrence I Ds is, the kernel must verify that the parametric arguments Ds match the inductive's declared parameters. The vulnerable code fails to check that projection expressions (.proj) in Ds reference the correct structure name — a .proj C 0 w is accepted even when w : W and W ≠ C.

Combined with a hash collision (the kernel uses Expr.hash comparisons in its definitional equality check), this allows an attacker to register declarations where the kernel's internal type assignment disagrees with the actual term semantics, leading to type confusion and a proof of False.

References

• NVD: CVE-2026-72844
• VulnCheck Advisory
• oss-security disclosure
• Lean 4 issue #14576
• Fix PR #14577
• Fix commit

Credits

• Bug discovery and minimal PoC: @kiranandcode
• Original CollatzLean exploit: @xrchz (Ramana Kumar)
• Kernel fix: Leonardo de Moura (PR #14577)
• CVE filing and PoC packaging: Jonathan Brossard (@endrazine)