Rocq kernel bug yields a checked proof of False
Original title: CVE-2026-72714: Rocq universe checking state desynchronised after module close (0 = 1 demonstrated) — 0-day
Closing a module that used Local Unset Universe Checking does not restore the flag, and Print Assumptions still reports the proof closed.
Jonathan Brossard reported CVE-2026-72714, a soundness bug in the Rocq (formerly Coq) kernel. It allows a checked proof of False, and therefore any proposition including 0 = 1, without axioms, plugins, or unsafe flags. Print Assumptions reports the proof as closed. The module system does not restore the universe checking flag after a module that used Local Unset Universe Checking is closed. The title calls it a 0-day.
Unconfirmed: The title calls it a 0-day, but the text does not say attackers exploit it or name a fix.
- The bug is in universe-checking state after a module closes.
- No axioms, plugins, or unsafe flags are required.
- The post demonstrates a proof of 0 = 1.
- No fixed version is stated.
Impact: Checked proofs of arbitrary propositions without axioms
| Product | Affected |
|---|---|
| Rocq | — |
| Coq | — |
Vulnerabilities mentioned
All| CVE | Vulnerability | CVSS | EPSS | Signals | Published |
|---|---|---|---|---|---|
| CVE-2026-72714 | Rocq Prover does not restore the universe graph's copy of the universe checking flag when a module that locally disabled the check is closed | 6.8 | <1% |
From the original article
Posted by Jonathan Brossard on Oct 25 1. Summary ========== A soundness bug in the Rocq (formerly Coq) kernel allows construction of a checked proof of False — and by extension, any proposition, including 0 = 1 — without axioms, plugins, or unsafe flags. Print Assumptions reports the proof as closed under the global context.
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.