6.8
MEDIUM CVSS 4.0
CVE-2026-72844
Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections
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.

INFO

Published Date :

Aug. 20, 2026, 5:19 p.m.

Last Modified :

Aug. 20, 2026, 5:19 p.m.

Remotely Exploit :

No

Source :

VulnCheck
Affected Products

The following products are affected by CVE-2026-72844 vulnerability. Even if cvefeed.io is aware of the exact versions of the products that are affected, the information is not represented in the table below.

No affected product recoded yet

CVSS Scores
The Common Vulnerability Scoring System is a standardized framework for assessing the severity of vulnerabilities in software and systems. We collect and displays CVSS scores from various sources for each CVE.
Score Version Severity Vector Exploitability Score Impact Score Source
CVSS 3.1 MEDIUM 83251b91-4cc7-4094-a5c7-464a1b83ea10
CVSS 4.0 MEDIUM 83251b91-4cc7-4094-a5c7-464a1b83ea10
Solution
Update Lean 4 kernel and associated components to fix type confusion vulnerabilities.
  • Update the Lean 4 kernel to the latest version.
  • Apply security patches for inductive type checking.
  • Review metaprogramming and declaration additive processes.
  • Validate nested inductive application type checking.

We scan GitHub repositories to detect new proof-of-concept exploits. Following list is a collection of public exploits and proof-of-concepts, which have been published on GitHub (sorted by the most recently updated).

Results are limited to the first 15 repositories due to potential performance issues.

The following list is the news that have been mention CVE-2026-72844 vulnerability anywhere in the article.

EPSS is a daily estimate of the probability of exploitation activity being observed over the next 30 days. Following chart shows the EPSS score history of the vulnerability.