The Lean 4 kernel fails to check that the body of an opaque declaration is closed because environment::add_opaque omits the check_no_metavar_no_fvar call that other declaration paths perform. This omission allows a metaprogram to create a temporary local of type False, cache its type, restore the local context, and then submit an opaque declaration with the now-unbound variable. The kernel infers the cached type without verifying local context membership, admitting an opaque constant of type False. This bypass occurs through the standard checked path at maximum kernel checking without requiring unsafe operations or modified files. The vulnerability is fixed in version 4.32.2 by adding the missing closure check.

An attacker can cause the kernel to accept an opaque constant of type False, from which any proposition follows, potentially compromising the logical soundness of proofs or programs relying on Lean 4. This could lead to incorrect theorem proofs or unsound reasoning within the environment.

A fix is available in Lean 4 version 4.32.2, which adds the missing closure check to environment::add_opaque. Users should upgrade to version 4.32.2 or later to remediate this vulnerability.