CVE-2026-72711: Lean 4 Kernel Privilege Escalation Flaw

CVE-2026-72711 Overview

CVE-2026-72711 is a soundness vulnerability in the Lean 4 theorem prover kernel. The kernel does not verify that the body of an opaque declaration is closed. Specifically, environment::add_opaque omits the check_no_metavar_no_fvar call that the definition and theorem code paths perform. A crafted metaprogram can prime the type checker inference cache with a free variable of type False, restore the local context, then submit an opaque declaration referencing the now-unbound variable. The kernel admits a constant of type False, from which any proposition can be derived. The issue is fixed in Lean 4.32.2.

Critical Impact
Attackers can construct a proof of False through the ordinary checked kernel path without sorry, unsafeCast, addDeclWithoutChecking, or modified .olean files, breaking the soundness guarantees that downstream verified software depends on.

Affected Products

Lean 4 theorem prover kernel prior to version 4.32.2
Projects and libraries that trust externally supplied Lean proofs
Verified software builds relying on Lean 4 kernel soundness

Discovery Timeline

2026-08-24 - CVE-2026-72711 published to NVD
2026-08-24 - Last updated in NVD database

Technical Details for CVE-2026-72711

Vulnerability Analysis

The Lean 4 kernel enforces that declaration bodies contain no free variables absent from the surrounding local context. This closure check is applied inside the code paths that handle definition and theorem additions. The opaque code path in environment::add_opaque skips the check_no_metavar_no_fvar invocation, leaving the closure invariant unenforced for opaque constants.

The flaw is classified as improper input validation [CWE-20]. Kernel soundness relies on every accepted declaration being well-formed, so a single missing validation call collapses the trust boundary between metaprograms and the kernel. An accepted opaque constant of type False yields False.elim-driven proofs of arbitrary propositions.

Root Cause

The root cause is a missing invariant check in one branch of the declaration acceptance logic. The type checker's inference cache is keyed in a way that does not revalidate free-variable membership in the current local context on cache hits. When environment::add_opaque accepts a body without calling check_no_metavar_no_fvar, and the type is served from the cache, the kernel infers the cached type before the local-context membership branch would run.

Attack Vector

Exploitation requires the attacker to supply or influence a Lean metaprogram that is elaborated by a trusted Lean 4 instance. The metaprogram creates a temporary local variable of type False, forces the type checker to cache its inferred type, restores the local context so the variable becomes unbound, then submits an opaque declaration whose value references that variable. The resulting constant carries no axioms and passes maximum kernel checking. See the Lean4 Issue #14484 and the public proof-of-concept for the reproduction. No verified exploit code is reproduced here; refer to those upstream references for technical details.

Detection Methods for CVE-2026-72711

Indicators of Compromise

Lean source files that emit opaque declarations of type False, Empty, or other uninhabited propositions from user-controlled metaprograms
.olean artifacts produced by Lean 4 versions below 4.32.2 whose environments contain axiomless proofs of contradictory propositions
Metaprograms that manipulate the local context around inference cache use, particularly patterns that create and drop free variables before calling addDecl with an opaque body

Detection Strategies

Audit repositories and build pipelines for the installed Lean 4 toolchain version and flag any instance older than 4.32.2
Statically scan Lean sources for opaque declarations whose bodies invoke metaprogramming APIs that manipulate free variables and the type checker cache
Use #print axioms on critical theorems to confirm they do not transitively depend on suspicious opaque constants introduced by third-party libraries

Monitoring Recommendations

Monitor CI systems that build Lean projects for toolchain version drift and enforce a minimum version pin of 4.32.2
Track ingestion of third-party .olean files and require rebuilds from source on a patched toolchain before trusting proofs
Log elaboration failures and kernel errors from Lean build processes to identify anomalous metaprogram behavior

How to Mitigate CVE-2026-72711

Immediate Actions Required

Upgrade all Lean 4 installations to version 4.32.2 or later, which adds the missing closure check in environment::add_opaque
Rebuild dependent projects and .olean caches on the patched toolchain to invalidate any environments produced by vulnerable kernels
Revalidate proofs supplied by untrusted contributors and reject artifacts elaborated by pre-4.32.2 kernels

Patch Information

The fix is delivered in Lean 4.32.2 through the change tracked in Lean4 Pull Request #14498, which adds the missing check_no_metavar_no_fvar closure check to the opaque declaration path. Additional context is available in the VulnCheck Security Advisory and the upstream Lean4 GitHub Repository.

Workarounds

Restrict Lean elaboration to trusted source inputs until the toolchain upgrade is complete
Avoid consuming precompiled .olean files from untrusted sources on vulnerable kernels
Review any local patches that touch environment::add_opaque to confirm the closure check is present before deployment

bash

# Configuration example
# Pin Lean toolchain to the patched release in lean-toolchain
echo "leanprover/lean4:v4.32.2" > lean-toolchain
lake clean
lake build