CVE-2026-72704 — Rocq Prover through 9.2.0 Guard Checker Trusts Corrupted Recursive Tree After Transport
The guard checker in Rocq Prover does not recheck the recursive tree representation of an inductive type parameter after that parameter has been changed by transport. A fixpoint may apply a rewrite along an equality between types to its recursive argument, which the guard checker accepts because the inductive type is preserved, while the recursive tree recorded for the parameter is altered. A second fixpoint that calls the first inherits the altered recursive tree without verification, so a call that is not structurally decreasing is accepted as terminating. The resulting non-terminating definition proves that a natural number equals its own successor and therefore False, from which any proposition follows. The demonstration uses two axioms that follow from univalence and are consistent with the calculus of inductive constructions, so the contradiction comes from the guard check rather than from the assumptions. A fix is proposed but not merged.
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 matching the vulnerability class (logic error), 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
5 on the record
Elsewhere on this site
Related CVEs (same products)
- Medium CVE-2026-72714 Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close 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-72704 is "Rocq Prover through 9.2.0 Guard Checker Trusts Corrupted Recursive Tree After Transport", 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.