Lean 4 Kernel Opaque Declaration Vulnerability in Lean Prover

CVE-2026-72711

What is CVE-2026-72711?

The Lean 4 kernel contains a flaw where it fails to properly check that the body of an opaque declaration is closed. Specifically, the method environment::add_opaque omits the crucial check found in the definition and theorem paths, allowing for a scenario where a value may contain free variables not present in the local context. This oversight means that a metaprogram can make use of a temporary local type of False, storing it in the inference cache. Subsequently, the local context can be restored while the cache entry remains valid, and an opaque declaration with the unbound variable can be submitted. Given that the kernel's cache lookup occurs prior to checking local context membership, it mistakenly infers the cached type, permitting an opaque constant of type False to be accepted. This declaration is processed via the kernel's standard checking procedures without utilizing unsafe practices or modifications, resulting in a potentially dangerous acceptance of invalid declarations. This vulnerability was addressed in version 4.32.2 by introducing the missing closure check.

References