Read the docs
TI-2026-50950 Aliases CVE-2026-72714GHSA-95gm-3748-rx8v

Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close

Priority MEDIUM 63CWE-459Published · Updated

Key facts

Attack vector
Local
Privileges required
None
User interaction
Passive
Attack complexity
Low
Attack requirements
None
Impact type
—
Confidentiality · integrity · availability
None · High · None
Fix status
No fix listed

Attack profile from CVSS 4.0 · CNA. Fix status from CNA.

Summary

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 its own copy which is left disabled. The two views then disagree: Test Universe Checking reports the check as enabled while the kernel continues to accept universe-inconsistent terms. With the constraint between two universes no longer enforced, Hurkens' paradox applies and yields a proof of False, from which any proposition follows. The proof uses no axioms, plugins or unsafe features once the module has closed, and Print Assumptions reports it as closed under the global context, so neither the assumption audit nor the flag query reflects the actual kernel state. No fix is available.

Why it matters now

Exploitation Proof of concept CISA SSVC · not in CISA KEV
EPSS 0.00176 7th percentileScored 2026-11-07
Public exploit Yes 1 exploit referenceTagged by the CNA
Fix No fix listed No fixed version in the sources yet

SSVC decision points

CISA ADP · SSVC 2.0.3

Exploitation
Poc
Automatable
No
Technical impact
Partial

The decision (Track, Attend, Act) also depends on your mission and well-being impact; see CISA's SSVC guide.

Affected products

VendorProductAffected versionsFixed inStatusSource
rocq-proverrocqup to 9.2.0—No fix listedCNA
  • rocq Vendorrocq-prover Affected up to 9.2.0 Fixed in — No fix listed CNA

Remediation

No fixed version listed by the sources yet.

Vendor assessments

Red Hat

Red Hat's page for this CVE →

Not affected: 1 product
  • Red Hat

Timeline

  1. 2026-10-02 Threatist record created from CVE-2026-72714
  2. 2026-10-03 Alias added: GHSA-95gm-3748-rx8v

References

Exploit 1

Other 2

  • TI-2026-50943 Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument CVSS 4.0MEDIUM 6.8
  • TI-2026-50942 Rocq Prover through 9.2.0 Guard Checker Trusts Corrupted Recursive Tree After Transport CVSS 4.0MEDIUM 6.8
  • TI-2026-50941 Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls CVSS 4.0MEDIUM 6.8
  • TI-2020-19392 Coq and Rocq Prover Print Assumptions Omits Unsafe Universe Checking Inlined Through Parameter Inline CVSS 4.0MEDIUM 6.8

Sources

This product uses the NVD API but is not endorsed or certified by the NVD. Sources and licences