State Desynchronization Vulnerability in Rocq Prover by Rocq

CVE-2026-72714

What is CVE-2026-72714?

Rocq Prover contains a vulnerability where the universe graph fails to restore the checking flag for universe validation after a module that disables this check is closed. Normally, this local setting should only persist for the lifespan of the module, reverting to a global state upon closure. However, the universe graph retains its disabled state, leading to a disagreement between the Test Universe Checking system and the kernel. Consequently, this desynchronization allows for the acceptance of universe-inconsistent terms, consequently enabling proofs that can be exploited by generating false statements without relying on any axioms or unsafe features. As a result, the integrity of the universe checking mechanism within Rocq Prover is significantly compromised, and there is currently no fix available.

References