CVE-2026-72844: Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections
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::addinductive 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, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI, or a modified .olean file. The result is a type confusion yielding a proof of False that carries no axioms, from which any proposition can be derived. The published proof of concept additionally pads two expressions until their hashes and approximate depths collide, which defeats kernel caching; that is the technique used to reach the flaw, not its cause. Exploitation requires running a metaprogram in-process, for example by building a project or importing a malicious Lake dependency.
Affected Software
Event History
Frequently Asked Questions
Who is exposed to exploitation?
Users who build a Lean project or import a malicious Lake dependency are exposed if that action runs an attacker-controlled metaprogram in the Lean process. The issue is not described as remotely exploitable; the stated attack vector requires local code execution through an in-process metaprogram.
What does an attacker need to exploit this?
The attacker needs the ability to run a metaprogram in the Lean process. The proof of concept reaches the flaw through the ordinary checked addDecl path at maximum kernel checking and does not require sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI, modified .olean files, or a modified kernel.
What is the security impact if exploitation succeeds?
An attacker can cause a type confusion that produces a proof of False with no axioms. From that proof, any proposition can be derived, defeating the kernel's soundness guarantees for the affected process or build.
Does kernel checking or restricting common bypass mechanisms prevent this attack?
No. The described declaration is accepted through the ordinary checked addDecl path even at maximum kernel checking, and the proof of concept does not rely on the listed bypass mechanisms. The hash and approximate-depth collision padding is used to defeat kernel caching in the proof of concept, rather than being the underlying cause.