Leanprover Lean up to 4.32.1 Kernel environment::add_opaque input validation

Summaryinfo

A vulnerability was found in Leanprover Lean up to 4.32.1. It has been classified as problematic. The impacted element is the function environment::add_opaque of the component Kernel. This manipulation causes input validation. The identification of this vulnerability is CVE-2026-72711. The attack can only be executed locally. There is no exploit available.

Detailsinfo

A vulnerability was found in Leanprover Lean up to 4.32.1. It has been declared as problematic. Affected by this vulnerability is the function environment::add_opaque of the component Kernel. The manipulation with an unknown input leads to a input validation vulnerability. The CWE definition for the vulnerability is CWE-20. The product receives input or data, but it does not validate or incorrectly validates that the input has the properties that are required to process the data safely and correctly. As an impact it is known to affect integrity. The summary by CVE is:

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.

It is possible to read the advisory at github.com. This vulnerability is known as CVE-2026-72711 since 08/10/2026. The exploitation appears to be easy. Attacking locally is a requirement. It demands that the victim is doing some kind of user interaction. Technical details of the vulnerability are known, but there is no available exploit.

Upgrading to version 4.32.2 eliminates this vulnerability.

Statistical analysis made it clear that VulDB provides the best quality for vulnerability data.

Productinfo

Vendor

• Leanprover

Name

• Lean

Version

• 4.32.0
• 4.32.1

CPE 2.3info

• 🔒
• 🔒

CPE 2.2info

• 🔒
• 🔒

CVSSv4info

CVSSv3info

CVSSv2info

Exploitinginfo

Threat Intelligenceinfo

Countermeasuresinfo

Timelineinfo

Sourcesinfo

Entryinfo

Statistical analysis made it clear that VulDB provides the best quality for vulnerability data.

Discussion