CVE-2026-72714

A flaw was found in Rocq Prover. When a module that locally disabled the universe checking flag is closed, the prover fails to restore the universe graph's copy of this flag. This desynchronization allows the kernel to accept terms that are inconsistent with the universe, even though the system...

CVE-2020-37268

A flaw was found in Coq and Rocq provers. The Print Assumptions feature, which is used to audit the soundness of proofs, fails to report when a definition was created without proper "universe checking" a mechanism to ensure logical consistency. This occurs when the definition is incorporated...

EUVD-2026-65143

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. Local Unset Universe Checking inside a module is expected to last only until the module ends, and the global flag is restored, but the universe graph keeps...

CVE-2026-72714

Rocq Prover (through 9.2.0) contains a state desynchronization in its universe checking mechanism. When a module that locally disabled the universe checking flag is closed, the global flag is restored but the universe graph retains its own copy left disabled . The kernel then accepts universe-inc...

EUVD-2020-31263

Print Assumptions does not report that a definition was produced while universe checking was disabled when that definition reaches the caller through Parameter Inline in a module type. Applying a functor inlines the body of the parameter, and the inlining drops the record that the term was built...