Skip to content
Fencer Intel
medium 6.3

CVE-2026-72844 json

Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections

published 2mo ago modified 3d ago also EUVD-2026-63487

cvss
6.3
version 3.1, CNA
cisa kev
Not listed
not in CISA's catalog
epss
0.2%
EPSS 0.2% chance of exploitation in 30 days, percentile 8%
public exploits
0
none known

Summary

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.

Patch / fix

  • leanprover lean4 4.32.2

Is CVE-2026-72844 in your stack? Fencer shows which of your repositories are affected as soon as an advisory lands, and opens the fix as a pull request.

Check with Fencer

CISA SSVC

Exploitation
Proof of concept is public
Automatable
no
Technical impact
partial
Assessed
2mo ago

Exploit prediction

0.19% chance of exploitation in the next 30 days, higher than 8% of all scored CVEs (FIRST EPSS, 2026-11-11).

Exploits and checks

  • github.com https://github.com/endrazine/lean-cve-poc referenced PoC, tagged "exploit" by a source, unverified
  • github.com https://github.com/xrchz/CollatzLean referenced PoC, tagged "exploit" by a source, unverified

CVSS scores

assigned by version score vector
CNA 3.1 6.3 CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N
CNA 4.0 6.8 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
CNA 4.0 6.8 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/E:X/CR:X/IR:X/AR:X/MAV:X/MAC:X/MAT:X/MPR:X/MUI:X/MVC:X/MVI:X/MVA:X/MSC:X/MSI:X/MSA:X/S:X/AU:X/R:X/V:X/RE:X/U:X

Affected products

  • leanprover lean4

Classification

Weakness
  • CWE-843 Access of Resource Using Incompatible Type

References

Sources

Fencer Intel keeps one entry per vulnerability: the CVE id wins, then GHSA, and records that alias each other are merged, except that two CVEs always keep separate entries. The same data is available as JSON.