endrazine/lean-cve-poc: open-source project for self-hosters

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

Vulnerability Summary

The Lean 4 kernel fails to validate that projection expressions in nested inductive type declarations reference the correct structure. An adversarial metaprogram can register an inductive whose constructor type applies a .proj C 0 projection to a value of type W (which is not C). Because the kernel uses expression-hash comparison for certain definitional equality checks, a crafted hash collision between Bool.false and Bool.true allows type confusion, ultimately producing a checked proof of False — and from it, 0 = 1.

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

    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.