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-72711 Detail

Description

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.


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-14484 VulnCheck
https://github.com/leanprover/lean4 VulnCheck
https://github.com/leanprover/lean4/issues/14484 VulnCheck
https://github.com/leanprover/lean4/pull/14498 VulnCheck
https://www.vulncheck.com/advisories/lean-4-before-kernel-accepts-opaque-declaration-with-an-unbound-free-variable VulnCheck

Weakness Enumeration

CWE-ID CWE Name Source
CWE-20 Improper Input Validation VulnCheck  

Change History

2 change records found show changes

Quick Info

CVE Dictionary Entry:
CVE-2026-72711
NVD Published Date:
08/24/2026
NVD Last Modified:
08/24/2026
Source:
VulnCheck