Gaëtan Gilbert

**Name of the Vulnerable Software and Affected Versions** Rocq Prover (affected versions not specified) **Description** The software fails to restore the universe graph's copy of the universe checking flag after a module that locally disabled the check is closed. While the global flag is restored, the universe graph retains a disabled state, causing a discrepancy where the system reports the check as enabled while the kernel continues to accept universe-inconsistent terms. This allows the application of Hurkens' paradox—a logical contradiction—to produce a proof of False, enabling any proposition to be proven. This state persists even without the use of axioms, plugins, or unsafe features, and is not reflected in the assumption audit or flag queries. **Recommendations** At the moment, there is no information about a newer version that contains a fix for this vulnerability.