Skip to content
Fencer Vulns
medium 6.3

CVE-2026-72711 json

Lean 4 before 4.32.2 Kernel Accepts Opaque Declaration With an Unbound Free Variable

published 2026-08-24 2 mo ago modified 2026-10-26 14 d ago also EUVD-2026-65142

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 7%
public exploits
0
none known

Summary

The Lean 4 kernel does not check that the body of an opaque declaration is closed. environment::add_opaque omits the check_no_metavar_no_fvar call that the definition and theorem paths perform, so a value containing a free variable that is absent from the local context is not rejected outright. A metaprogram can first cause the kernel to create a temporary local of type False and record its type in the type checker's inference cache, then restore the local context while that cache entry persists on the same type checker instance, and finally submit an opaque declaration whose value is the now-unbound variable. The cache lookup answers before the branch that would test membership of the local context, so the kernel infers the cached type and admits an opaque constant of type False, from which any proposition follows. The declaration is accepted through the ordinary checked path at maximum kernel checking, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, foreign code or a modified .olean file, and the result carries no axioms. Fixed in 4.32.2 by adding the missing closure check.

Patch / fix

  • leanprover lean4 4.32.2

CISA SSVC

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

Exploit prediction

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

Exploits and checks

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

CVSS scores

assigned by version score vector
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 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/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-20 Improper Input Validation

References

Sources

Fencer Vulns 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.