The vulnerability in rocq-prover arises because the universe graph maintains its own copy of the universe checking flag, which is not restored when a module that locally disables universe checking ends. Although the global flag is restored, the universe graph remains disabled, causing a mismatch between the test universe checking and the kernel's actual state. This discrepancy disables enforcement of constraints between universes, enabling Hurkens' paradox to produce a proof of False. The exploit requires no axioms, plugins, or unsafe features once the module is closed, and standard audits do not detect the altered kernel state.

The vulnerability allows the kernel to accept universe-inconsistent terms, leading to a proof of False from which any proposition can be derived. This undermines the soundness of proofs generated by rocq-prover, potentially invalidating all proofs relying on universe consistency. The issue does not require elevated privileges or unsafe features to exploit once the module is closed, making it a significant integrity risk for users relying on the prover's correctness.

No fix or patch is currently available for this vulnerability. Users should be aware of the risk and consider avoiding use of modules that locally disable universe checking until an official remediation is provided. Monitor vendor advisories for updates on remediation status.