lean-cve-poc-14484

CVE-2026-72711 — Lean 4 Kernel Soundness Bug: Inference Cache Poisoning Proving0 = 1 axiom-free via opaque declaration FVar cache poisoning. Field| Value ---|--- Bug report| leanprover/lean414484 Fix| leanprover/lean414498 Affected| Lean 4 ≤ v4.31.0 / all prior versions Fixed in| nightly...

CVE-2026-72711: Improper Input Validation

The Lean 4 kernel does not check that the body of an opaque declaration is closed. environment::addopaque omits the checknometavarnofvar 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...