Patrick Hulin

**Name of the Vulnerable Software and Affected Versions** Lean 4 versions prior to 4.32.2 **Description** The kernel fails to verify that the body of an opaque declaration is closed. Specifically, the `environment::add opaque` function omits the `check no metavar no fvar()` call used in definition and theorem paths, allowing values with free variables absent from the local context to be accepted. A metaprogram can exploit this by creating a temporary local of type False and recording it in the type checker's inference cache. By restoring the local context while the cache entry persists and submitting an opaque declaration with the unbound variable, the kernel may infer the cached type and admit an opaque constant of type False, which allows any proposition to follow. This occurs during ordinary checked paths at maximum kernel checking without requiring axioms or unsafe casts. **Recommendations** Update to version 4.32.2.