U.S. flag   An official website of the United States government
Dot gov

Official websites use .gov
A .gov website belongs to an official government organization in the United States.

Https

Secure .gov websites use HTTPS
A lock (Dot gov) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.

National Vulnerability Database

National Vulnerability Database

NVD

National Vulnerability Database
  1. Vulnerabilities

CVE-2026-72844 Detail

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.


Metrics

 
NVD enrichment efforts reference publicly available information to associate vector strings. CVSS information contributed by other sources is also displayed.
CVSS 4.0 Severity and Vector Strings:

NIST CVSS score
NIST: NVD
N/A
NVD assessment not yet provided.

Nist CVSS score does not match with CNA score
CNA:  VulnCheck
CVSS-B 6.8 MEDIUM
Vector:  CVSS:4.0/AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N

References to Advisories, Solutions, and Tools

By selecting these links, you will be leaving NIST webspace. We have provided these links to other web sites because they may have information that would be of interest to you. No inferences should be drawn on account of other sites being referenced, or not, from this page. There may be other web sites that are more appropriate for your purpose. NIST does not necessarily endorse the views expressed, or concur with the facts presented on these sites. Further, NIST does not endorse any commercial products that may be mentioned on these sites. Please address comments about this page to [email protected].

URL Source(s) Tag(s)
https://github.com/endrazine/lean-cve-poc VulnCheck
https://github.com/leanprover/lean4 VulnCheck
https://github.com/leanprover/lean4/commit/a39eab69e1eee9ad38f4efe507907b1026a77808 VulnCheck
https://github.com/leanprover/lean4/issues/14576 VulnCheck
https://github.com/leanprover/lean4/pull/14577 VulnCheck
https://github.com/xrchz/CollatzLean VulnCheck
https://www.openwall.com/lists/oss-security/2026/08/02/1 VulnCheck
https://www.vulncheck.com/advisories/lean-4-kernel-type-checking-bypass-via-mismatched-structure-projections VulnCheck

Weakness Enumeration

CWE-ID CWE Name Source
CWE-843 Access of Resource Using Incompatible Type ('Type Confusion') VulnCheck  

Change History

1 change records found show changes

Quick Info

CVE Dictionary Entry:
CVE-2026-72844
NVD Published Date:
08/20/2026
NVD Last Modified:
08/20/2026
Source:
VulnCheck