CVE-2026-72714 — Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close
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.
Who exploits it and how urgent it is
A 0–100 score combining confirmed exploitation, ransomware and APT use, public exploits, EPSS and severity.
How the score was calculated
- EPSS 0.2% (30-day exploitation probability)+1
- Technical severity (medium)+3
- CISA SSVC: exploitation "poc"+5
The score orders the patch queue; it does not replace your asset context (internet exposure, criticality, compensating controls).
Triage
Is it exploited, how likely is exploitation, what does it touch, and how severe do the sources call it.
CISA SSVC assessment CISA
Three decision points CISA publishes for the CVEs it assesses (SSVC 2.0.3). A stakeholder decision, not a severity score.
Remediation
Fixes and mitigations documented by the sources — linked to the original advisory.
No fix documented by the sources we poll. That does not mean none exists: check the vendor advisory.
First 24 hours
Ordered from the record’s own fields — exposure first, because you cannot patch what you have not found. A rule-generated starting point.
- Identify exposed assets running the affected vendor/product/version combinations (Rocq-prover Rocq).
- No fix documented in the sources: reduce exposure and monitor the vendor advisory.
- Exploitation requires user interaction: tighten email/web filtering and warn affected users.
- Search available logs for exploit probes, errors and authentication anomalies.
Affected scope
Vendor, product and versions as the sources word them.
| Vendor | Product | Versions | Status | Source |
|---|---|---|---|---|
| Rocq-prover | Rocq | ≤ 9.2.0 | Vulnerable | CVE Program (cve.org) e CISA ADP |
Attack characteristics
The CVSS vector, decoded. It describes the attack, not your exposure to it.
Every base score collected
Sources score independently and may disagree; each row says who scored it and under which version.
| Score | Version | Severity | Expl. | Impact | Scored by |
|---|---|---|---|---|---|
| 6.8 | CVSS 4.0 | Medium | — | — | disclosure@vulncheck.com via NIST National Vulnerability Database |
| 6.8 | CVSS 4.0 | Medium | — | — | VulnCheck via CVE Program (cve.org) e CISA ADP |
| 6.3 | CVSS 3.1 | Medium | 1.8 | 4.0 | disclosure@vulncheck.com via NIST National Vulnerability Database |
| 6.3 | CVSS 3.1 | Medium | — | — | VulnCheck via CVE Program (cve.org) e CISA ADP |
CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N (score shown at the top: disclosure@vulncheck.com) Weakness MITRE
Weakness class according to MITRE’s CWE catalog.
EPSS over time FIRST
Oct 13, 2026 → Oct 14, 2026 · 2 reading(s) · max 0.18%
Detection
Read off the CVSS vector and the weakness class. Starting points, not tested rules.
- Local/physical vector: focus on endpoint telemetry (EDR) from affected hosts.
Timeline
What happened to this CVE, newest first.
- 2026
- Affected products added · rocq-prover/rocq
- SSVC assessment updated
- Record published
- CVSS changed · 6.3
- Source status changed · → Deferred
- Record created in this database
- CVE published
Source activity
Repeated readings are counted rather than listed.
- 1× Official description updated · Oct 13, 2026 – Oct 13, 2026
References
4 on the record
Elsewhere on this site
Related CVEs (same products)
- Medium CVE-2026-72704 Rocq Prover through 9.2.0 Guard Checker Trusts Corrupted Recursive Tree After Transport Aug 24, 2026
- Medium CVE-2026-72703 Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls Aug 24, 2026
- Medium CVE-2026-72705 Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument Aug 24, 2026
- Medium CVE-2020-37268 Coq and Rocq Prover Print Assumptions Omits Unsafe Universe Checking Inlined Through Parameter Inline Aug 24, 2026
Not in any source we poll
Listed rather than left blank: an empty field and an unmeasured one look identical on screen, and only one is a reason to look elsewhere.
- No fixed version, patch or mitigation documented.
- No confirmed IOCs, IP addresses, domains, file hashes, or malware artifacts supplied.
- No organization-specific asset inventory, compensating-control status, or patch deployment evidence supplied.
- No exploit packet captures, log samples, or incident case IDs supplied.
Answered from this record
Text assembled only from the fields above — no additional claims.
What should defenders know first?
CVE-2026-72714 is "Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close", rated Medium. It affects Rocq (Rocq-prover); versions are in the scope table. It is not in CISA KEV, which does not rule out exploitation. CVSS 6.3 describes technical severity. EPSS 0.18% estimates the probability of exploitation in 30 days; neither replaces your asset context. First verify whether exposed or business-critical assets run the affected versions, apply vendor fixes or mitigations, and preserve logs for review.
Comments
Moderated technical discussion. Read the community guidelines.
No comments yet.
Sign in or create an account to comment and suggest corrections.