CVE-2026-72714: Rocq universe checking state desynchronised after module close (0 = 1 demonstrated) — 0-day
// AI summary
Rocq kernel has a soundness bug allowing construction of a checked proof of False, such as 0 = 1, because the module system fails to restore the universe checking flag after module closure.
// from the source
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. The module system does not correctly restore the universe checking flag when a module that locally disabled the check (`Local Unset Universe Checking`) is...