The Rocq proof kernel fails to restore its universe‑checking flag when a module that has locally disabled the check is closed. Although the module’s local state is cleared, the kernel’s universe graph retains a copy of the flag that remains disabled. As a result the kernel accepts constructs that violate universe constraints while the external flag reports that checking is enabled. This desynchronisation creates a loophole that an attacker can exploit with Hurkens’ paradox to construct a proof of "False" using only core language constructs, thereby allowing arbitrary propositions to become provable and compromising the integrity of all subsequent proofs.

Any installation of Rocq Prover version 9.2.0 or earlier is affected. The vendor product is rocq-prover:rocq. Versions prior to 9.2.0 are not impacted.

The CVSS score of 6.8 indicates moderate severity. The EPSS score is unavailable and the vulnerability is not listed in the CISA KEV catalog, so the probability of widespread exploitation is unknown. The exploit requires the ability to load a module that temporarily disables universe checking and then close it. Because no patch exists, this attack path remains persistently available to any user who can influence module content. An attacker who succeeds can cause the kernel to accept inconsistent terms and prove "False", breaking the logical soundness guarantees of the system.