Skip to content
Fencer Vulns
medium 6.3

CVE-2026-72714 json

Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close

published 2026-08-24 2 mo ago modified 2026-10-26 14 d ago also EUVD-2026-65143

cvss
6.3
version 3.1, CNA
cisa kev
Not listed
not in CISA's catalog
epss
0.2%
EPSS 0.2% chance of exploitation in 30 days, percentile 7%
public exploits
0
none known

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.

Vendor advisories

What the vendors themselves say about their products: affected, fixed or not affected, and what to do.

red hat product security vex CVE-2026-72714 updated cvss 6.3

rocq: Rocq Prover: Critical integrity bypass via universe checking state desynchronization.

  • Red Hat All currently supported Red Hat products
    not affected: vulnerable code not present

Red Hat CSAF VEX © Red Hat, Inc., from https://security.access.redhat.com/data/csaf/v2/vex/; changed: reduced to product statuses and remediations. CC BY 4.0 · csaf

CISA SSVC

Exploitation
Proof of concept is public
Automatable
no
Technical impact
partial
Assessed
2 mo ago

Exploit prediction

0.18% chance of exploitation in the next 30 days, higher than 7% of all scored CVEs (FIRST EPSS, 2026-11-08).

Exploits and checks

  • github.com https://github.com/rocq-prover/rocq/issues/22287 referenced PoC, tagged "exploit" by a source, unverified
  • github.com https://github.com/endrazine/rocq-cve-poc-22287 referenced PoC, tagged "exploit" by a source, unverified

CVSS scores

assigned by version score vector
CNA 4.0 6.8 CVSS:4.0/AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N
CNA 3.1 6.3 CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N
CNA 4.0 6.8 CVSS:4.0/AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N/E:X/CR:X/IR:X/AR:X/MAV:X/MAC:X/MAT:X/MPR:X/MUI:X/MVC:X/MVI:X/MVA:X/MSC:X/MSI:X/MSA:X/S:X/AU:X/R:X/V:X/RE:X/U:X

Affected products

  • rocq-prover rocq

Classification

Weakness

References

Sources

Fencer Vulns keeps one entry per vulnerability: the CVE id wins, then GHSA, and records that alias each other are merged, except that two CVEs always keep separate entries. The same data is available as JSON.