Rocq kernel bugs accept checked proofs of false
First merged summary.
Jonathan Brossard disclosed Rocq kernel soundness bugs that accept checked proofs of false, including 0 = 1, with no fixes stated.
Jonathan Brossard posted a series of Rocq kernel soundness reports to oss-security on October 25, 2026. The bugs, in the prover formerly known as Coq, let the kernel accept unsound fixpoints or universe-checking state and produce a checked proof of False, including 0 = 1, while Print Assumptions reports the proof closed. The posts cover unchecked nested mutual-fixpoint cross-calls (CVE-2026-72703), a recursive tree trusted after eq_rect or rew transport (CVE-2026-72704), a fixpoint passed as a higher-order argument (CVE-2026-72705), and a universe-checking flag left unset after a module closes (CVE-2026-72714). CVE-2020-37268 drops Unset Universe Checking metadata when Parameter Inline is inlined by functor application; the post says it has been unfixed since 2020. No affected or fixed versions are stated.
- CVE-2026-72703 treats nested mutual fixpoint parameters as uniform and skips cross-calls.
- CVE-2026-72704 trusts the recursive tree after eq_rect or rew without rechecking.
- CVE-2026-72705 does not track calls when a fixpoint is passed through its own arguments.
- CVE-2026-72714 leaves Local Unset Universe Checking in effect after the module closes.
- CVE-2020-37268 drops universe-checking metadata via Parameter Inline; called unfixed since 2020.
- Posts label two 2026 issues 0-days and state no patched versions.
Timeline
dated events in the reporting · oldest first- Oct 25, 2026Brossard posts Rocq kernel soundness reports to oss-security · oss-security
What each outlet adds
beyond the shared facts- oss-securityFive Brossard posts detail distinct Rocq kernel CVEs and closed 0=1 proofs.
Coverage
oldest first · one row per article · UTC- · 4h ago
oss-securityFirst report
Rocq guard checker accepts non-terminating cross-calls (CVE-2026-72703)
Nested mutual fixpoint parameters are treated as uniform without examining cross-calls between them.
- · 4h ago
Rocq guard checker trusts rewritten recursive tree (CVE-2026-72704)
After eq_rect or rew changes an inductive parameter, the checker does not recheck the recursive tree.
- · 4h ago
Rocq guard checker misses recursive calls via higher-order arguments (CVE-2026-72705)
A checked proof of False, including 0 = 1, needs no axioms, tactics, plugins, or unsafe flags.
- · 4h ago
Rocq kernel bug yields a checked proof of False
Closing a module that used Local Unset Universe Checking does not restore the flag, and Print Assumptions still reports the proof closed.
- · 4h ago
Rocq Print Assumptions hides unsafe universe checks
Inlining a Parameter Inline body drops metadata that the definition was made with universe checking unset, and no fix is stated.
Vulnerabilities in this story
All| CVE | Vulnerability | CVSS | EPSS | Signals | Published |
|---|---|---|---|---|---|
| CVE-2020-37268 | Print Assumptions does not report that a definition was produced while universe checking was disabled when that definition reaches the caller through Parameter… | 6.8 | <1% | ||
| CVE-2026-72703 | The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint | 6.8 | <1% | ||
| CVE-2026-72704 | The guard checker in Rocq Prover does not recheck the recursive tree representation of an inductive type parameter after that parameter has been changed by… | 6.8 | <1% | ||
| CVE-2026-72705 | The guard checker in Rocq Prover does not follow recursive calls made through a fixpoint's own arguments | 6.8 | <1% | ||
| 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% |