Executive brief
Lean 4 is a theorem prover and programming language used to write formally verified software and machine-checked proofs. A soundness bug in the kernel allows a malicious program or dependency to create a false proof (such as proving 0 = 1) that appears axiom-free, invalidating any formal verification claims. This affects all safety-critical systems relying on Lean proofs, including compilers, cryptographic libraries, and autonomous vehicle software.
Technical details
The vulnerability is a type confusion (CWE-843) in the kernel's handling of nested inductive types. The kernel fails to verify that projection expressions (.proj) reference the correct structure name, allowing ill-typed nested inductives to be registered via the checked addDecl path even at maximum trust level (--trust=0). An attacker can craft a nested inductive whose constructor applies an incorrect projection, and combined with expression hash collisions, bypass definitional equality checks and the kernel's type system. The result is a derivable proof of False with no axioms. Exploitation requires running a malicious metaprogram in-process, such as through a Lake dependency or project build. The vulnerability was fixed in Lean 4 nightly 2026-07-29 and v4.32.2.
Affected products
- Lean Lean 4 ≤ v4.31.0
Timeline
- 2026-08-20: disclosed: CVE-2026-72844 published
- 2026-07-29: patched: Fixed in Lean 4 nightly; v4.32.2 includes the fix