CVE-2026-72844
Received Received - Intake

Type Confusion in Lean 4 Kernel via Inductive Projection

Publication date: 2026-08-20

Last updated on: 2026-08-20

Assigner: VulnCheck

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

CVSS Scores

EPSS Scores

Probability:
Percentile:

Meta Information

Published
2026-08-20
Last Modified
2026-08-20
Generated
2026-08-20
AI Q&A
2026-08-20
EPSS Evaluated
N/A
NVD
CVE-2026-72844
EUVD
EUVD-2026-63487

Affected Vendors & Products

Showing 7 associated CPEs
Vendor Product Version / Range
lean lean *-*
leanprover lean 4.31.0
leanprover lean 4.32.1
leanprover lean to 4.32.2 (exc)
leanprover lean to 4.33.0-rc1 (inc)
leanprover lean 4.34.0-nightly-2026-07-27
leanprover lean 4.34.0-nightly-2026-07-29

Helpful Resources

Exploitability

CWE
CWE Icon
KEV
KEV Icon
CWE ID Description
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.

Attack-Flow Graph

AI Quick Actions

Instant insights powered by AI
Executive Summary

This vulnerability in the Lean 4 kernel allows a metaprogram to register an ill-typed nested inductive declaration that the kernel incorrectly accepts. The kernel fails to verify that projection expressions match the expected structure types, leading to type confusion. This results in a proof of False without axioms, enabling derivation of any proposition.

Detection Guidance

Detection requires checking Lean 4 kernel versions and verifying proof artifacts. Inspect Lean version with `lean --version` and check project dependencies for malicious Lake packages. Review `.olean` files for unexpected declarations using `lean --make` to rebuild and check for errors. Compare hashes of critical proofs against known-good versions.

Impact Analysis

If you use Lean 4 for formal verification, this flaw could allow attackers to forge proofs, including false statements like 0=1, compromising the integrity of verified software. Exploitation requires running a malicious metaprogram in-process, such as importing a compromised dependency.

Compliance Impact

This vulnerability could undermine compliance by allowing forged proofs in formally verified systems. For example, it might invalidate cryptographic proofs in HIPAA-regulated systems or compromise data integrity claims in GDPR contexts where Lean is used for verification.

Mitigation Strategies

Upgrade Lean 4 to nightly builds from 2026-07-29 or later. Rebuild all proof artifacts with the patched kernel. Avoid untrusted metaprograms or Lake dependencies. Re-verify all proofs using independent tools like Nanoda. Audit existing projects for suspicious inductive declarations.

Chat Assistant

Ask questions about this CVE
Hi! I’m here to help you understand CVE-2026-72844. Ask me anything about the vulnerability, its impact, or mitigation strategies.
0/70

EPSS Chart