Lean 4 kernel accepts false proofs via opaque declarations (CVE-2026-72711)
Original title: CVE-2026-72711: Lean 4 kernel soundness bug — inference cache poisoning via opaque declarations (0 = 1 demonstrated)
A checked proof of False, including 0 = 1, passes the Lean 4 kernel at --trust=0 without axioms or unsafe features.
Jonathan Brossard reported CVE-2026-72711, a soundness bug in the Lean 4 kernel. The add_opaque path skips the closure check, check_no_metavar_no_fvar, that definition and theorem paths perform. That lets a proof of False, and therefore any proposition including 0 = 1, pass maximum checking without axioms, sorry, unsafeCast, debug.skipKernelTC, or modified .olean files. The post describes this as inference cache poisoning; the snippet cuts off before the full mechanism.
Unconfirmed: The feed snippet ends at “A stale,” so the rest of the cache-poisoning description is not available.
- Posted to oss-security on October 25 by Jonathan Brossard.
- The proof is accepted at --trust=0.
- add_opaque omits check_no_metavar_no_fvar.
- No fixed Lean version is stated in the snippet.
Impact: Checked proofs of false propositions are accepted
| Product | Affected |
|---|---|
| Lean 4 | — |
Vulnerabilities mentioned
All| CVE | Vulnerability | CVSS | EPSS | Signals | Published |
|---|---|---|---|---|---|
| CVE-2026-72711 | The Lean 4 kernel does not check that the body of an opaque declaration is closed | 6.8 | <1% |
From the original article
Posted by Jonathan Brossard on Oct 25 1. Summary ========== A soundness bug in the Lean 4 kernel allows construction of a checked proof of False — and by extension, any proposition, including 0 = 1 — without axioms, sorry, unsafeCast, debug. skipKernelTC, or modified .
seclists.org
A short excerpt; the article and its images belong to the publisher. Summary, key facts and assessment above are AI-written from the article and can be wrong.