Leanprover Lean 4 up to 4.32.1/4.33.0-rc1 Kernel Type Checking src/kernel/inductive.cpp add_inductive type confusion

Summaryinfo

A vulnerability was found in Leanprover Lean 4 up to 4.32.1/4.33.0-rc1. It has been classified as problematic. This affects the function environment::add_inductive of the file src/kernel/inductive.cpp of the component Kernel Type Checking. The manipulation leads to type confusion. This vulnerability is uniquely identified as CVE-2026-72844. Local access is required to approach this attack. No exploit exists.

Detailsinfo

A vulnerability, which was classified as problematic, has been found in Leanprover Lean 4 up to 4.32.1/4.33.0-rc1. This issue affects the function environment::add_inductive of the file src/kernel/inductive.cpp of the component Kernel Type Checking. The manipulation with an unknown input leads to a type confusion vulnerability. Using CWE to declare the problem leads to CWE-843. The product allocates or initializes a resource such as a pointer, object, or variable using one type, but it later accesses that resource using a type that is incompatible with the original type. Impacted is confidentiality, integrity, and availability. The summary by CVE is:

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, 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.

The advisory is shared at github.com. The identification of this vulnerability is CVE-2026-72844 since 08/10/2026. The exploitation is known to be easy. An attack has to be approached locally. Additional levels of successful authentication are required for exploitation. It demands that the victim is doing some kind of user interaction. Technical details are known, but no exploit is available.

Upgrading to version 4.32.2 eliminates this vulnerability.

If you want to get the best quality for vulnerability data then you always have to consider VulDB.

Productinfo

Vendor

• Leanprover

Name

• Lean 4

Version

• 4.32.0
• 4.32.1
• 4.33.0-rc1

CPE 2.3info

• 🔒
• 🔒
• 🔒

CPE 2.2info

• 🔒
• 🔒
• 🔒

CVSSv4info

CVSSv3info

CVSSv2info

Exploitinginfo

Threat Intelligenceinfo

Countermeasuresinfo

Timelineinfo

Sourcesinfo

Entryinfo

If you want to get the best quality for vulnerability data then you always have to consider VulDB.

Discussion