CVE-2026-72711Medium· 6.3▾ TwilightPoC availableThe 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 …
▾ Twilight zone — High severity, or a signal on a lesser flaw
impact 34.7 · likelihood 0 · exploitation 12
A public proof-of-concept already exists for this vulnerability — see Exploit availability below.
Public exploit / PoC code seen in 1 source. Availability, not in-the-wild use.
Stakeholder-Specific Vulnerability Categorization from CISA's ADP record at CVE.org: whether exploitation is observed, whether an attack can be automated, and how much of the system is at stake.
Exploit-prediction probability, daily snapshots since Sep 24.
Disclosure to exploitation, from the record and what we observed since indexing it.
Disclosed via NVD
0.2%
Last analysed / modified upstream
1 GitHub repo (last check)
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.
Refer to the linked advisories for vendor-supplied fixes and affected version ranges.
Connected by shared product, vendor, weakness, or advisory.
CVE-2026-72844Medium· 6.3The 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 appli…
CVE-2021-45105Medium· 5.9Apache Log4j2 versions 2.0-alpha1 through 2.16.0 (excluding 2.12.3 and 2.3.1) did not protect from uncontrolled recursion from self-referential lookups
CVE-2023-24329High· 7.5An issue in the urllib.parse component of Python before 3.11.4 allows attackers to bypass blocklisting methods by supplying a URL that starts with blank characters.
CVE-2022-35252Low· 3.7When curl is used to retrieve and parse cookies from a HTTP(S) server, itaccepts cookies using control codes that when later are sent back to a HTTPserver might make the server return 400 responses
CVE-2014-0114High· 7.5Apache Commons BeanUtils, as distributed in lib/commons-beanutils-1.8.0.jar in Apache Struts 1.x through 1.3.10 and in other products requiring commons-beanutils through 1.9.2, does not suppress the class property, which allows remote at…
CVE-2021-22924Low· 3.7libcurl keeps previously used connections in a connection pool for subsequenttransfers to reuse, if one of them matches the setup.Due to errors in the logic, the config matching function did not take 'issuercert' into account and it comp…