Type Checking Bypass in Lean 4 Kernel by Lean Prover

CVE-2026-72844

What is CVE-2026-72844?

The Lean 4 kernel fails to verify the structure within a projection expression aligns with the projected value's type. Consequently, the function environment::add_inductive does not properly type check nested inductive applications. This oversight permits a metaprogram to construct an ill-typed nested inductive type, allowing a projection to a value of an unrelated type. The weakness enables the kernel to accept declarations through a standard method without sufficient type verification. As a result, attackers can achieve type confusion leading to an unstructured proof that can derive any proposition from a proof of False. Exploiting this vulnerability necessitates the execution of a metaprogram within the Lean process, achieved via project construction or reliance on a compromised Lake dependency.

References