CVE-2026-72711
Received Received - Intake

Lean 4 Kernel Opaque Declaration Free Variable Bypass

Publication date: 2026-08-24

Last updated on: 2026-08-24

Assigner: VulnCheck

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.

CVSS Scores

EPSS Scores

Probability:
Percentile:

Meta Information

Published
2026-08-24
Last Modified
2026-08-24
Generated
2026-08-25
AI Q&A
2026-08-24
EPSS Evaluated
N/A
NVD
CVE-2026-72711
EUVD
EUVD-2026-65142

Affected Vendors & Products

Showing 3 associated CPEs
Vendor Product Version / Range
lean lean 4.32.2
leanprover lean4 4.32.2
leanprover lean4 to 4.32.2 (exc)

Helpful Resources

Exploitability

CWE
CWE Icon
KEV
KEV Icon
CWE ID Description
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.

Attack-Flow Graph

AI Quick Actions

Instant insights powered by AI
Executive Summary

This is a Lean 4 kernel soundness bug where the system fails to validate that opaque declarations are closed (free of unbound variables). The kernel's add_opaque function omits a closure check performed for definitions and theorems. An attacker can exploit this by manipulating the type checker's inference cache to create a stale entry for a temporary local of type False, then reference this unbound variable in an opaque declaration. The cache lookup returns False before validating the variable's membership in the local context, allowing the kernel to admit an opaque constant of type False without axioms or unsafe operations.

Detection Guidance

This vulnerability is specific to Lean 4 theorem prover systems and cannot be detected using standard network or system commands. It requires checking Lean 4 kernel versions and verifying if opaque declarations are properly validated. Use 'lean --version' to check the installed version and ensure it is 4.32.2 or later.

Impact Analysis

This vulnerability allows an adversarial metaprogram to prove False (e.g., 0=1) without using axioms or unsafe operations. It affects any system relying on Lean's kernel-checked proofs, including formally verified software, proof-carrying code, and AI-generated proof systems. The exploit works even with --trust=0 and passes leanchecker --fresh, making it dangerous for systems where proof correctness is critical.

Compliance Impact

This vulnerability primarily affects systems relying on Lean 4's kernel-checked proofs, such as formally verified software or proof-carrying code. It does not directly impact GDPR or HIPAA compliance unless the system's integrity is compromised by the ability to prove false statements, which could undermine data integrity requirements.

Mitigation Strategies

Upgrade Lean 4 to version 4.32.2 or later immediately. The fix adds the missing closure check for opaque declarations. If upgrading is not possible, avoid using metaprograms that manipulate the kernel's type checker cache or local contexts.

Chat Assistant

Ask questions about this CVE
Hi! I’m here to help you understand CVE-2026-72711. Ask me anything about the vulnerability, its impact, or mitigation strategies.
0/70

EPSS Chart