CVE-2026-72703
Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls
- Published
- Updated
- Reserved
- Assigned by
- VulnCheck
Description
The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find_uniform_parameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes that every parameter is uniform. A parameter that grows through a cross-call from one body to another therefore keeps the subterm specification it inherited from the enclosing fixpoint, and a recursive call guarded by that specification is accepted although the argument is not structurally smaller. A non-terminating definition is admitted as structurally decreasing, which yields a term whose value equals its own successor and so a proof of False, from which any proposition follows. The proof requires no axioms, plugins or unsafe flags and Print Assumptions reports it as closed under the global context. Introduced in Coq 8.20 and fixed in Rocq 9.2.0.
Public exploit
A reference of the record is tagged as an exploit or proof of concept: anyone can try it against an unpatched system. CISA's SSVC rates its exploitation: a proof of concept is public.
Timeline
ID reserved
By VulnCheck
- 14 days later
· 14 days later
Published
- 2 months later
· 2 months later
Record updated
Changes after publication (a new score, a public exploit, EPSS crossing 1, 10 or 50 %, leaving KEV) are kept since November 2026; earlier ones are not known.
Scores
| Scored by | CVSS | Score | Vector |
|---|---|---|---|
| VulnCheckCNA (assigner) | 4.0 | Medium6.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 |
| VulnCheckCNA (assigner) | 3.1 | Medium6.3 | CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N |
| NVDNVD · Deferred | 4.0 | Medium6.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 |
- EPSS (exploitation in 30 days)
- 0.18% · top 93% of all CVEs (7 Nov 2026)
- CISA SSVC
- Exploitation: poc · Automatable: no · Technical impact: partial
The list uses the assigner's score when there is one, then CISA's, then NVD's: Medium 6.8.
Weakness
Affected products
- affected 8.20 – < 9.2.0
References (6)
- https://github.com/rocq-prover/rocq (opens in a new tab)product
- https://github.com/rocq-prover/rocq/issues/21682 (opens in a new tab)issue-tracking
- https://github.com/rocq-prover/rocq/pull/21684 (opens in a new tab)issue-trackingpatch
- https://github.com/endrazine/rocq-cve-poc-21682 (opens in a new tab)exploit
- VulnCheck Advisory: Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls (opens in a new tab)third-party-advisory
- http://www.openwall.com/lists/oss-security/2026/10/26/4 (opens in a new tab)
Sources
The same CVE in the primary databases and aggregators, to check against.
- CVE.org record (opens in a new tab)
- CVE List JSON (GitHub) (opens in a new tab)
- NVD (opens in a new tab)
- FIRST EPSS (opens in a new tab)
- OSV.dev (opens in a new tab)
- GitHub Advisories (opens in a new tab)
- CIRCL Vulnerability-Lookup (opens in a new tab)
Badge for a README or a ticket
[](https://trackcve.app/cve/CVE-2026-72703)Record last updated .