CVE-2026-72705 — Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument
The guard checker in Rocq Prover does not follow recursive calls made through a fixpoint's own arguments. A fixpoint may pass itself as a higher-order argument to a second fixpoint, which then applies it to a value that is not a subterm of the structural argument. Passing the recursive function to a plain definition is rejected because the checker unfolds the definition and observes the call, but passing it to a fixpoint is accepted because higher-order recursive calls through fixpoint arguments are not tracked. This admits a type that is definitionally equal to its own negation, so self-application produces False in purely definitional code, without tactics, axioms, plugins or unsafe flags, and Print Assumptions reports the result as closed under the global context. Fixed in Rocq 9.2.0.
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-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
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-72705 is "Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument", 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.