Skip to content
Fencer Vulns
medium 6.3

CVE-2026-72703 json

Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls

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

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

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.

Patch / fix

  • rocq-prover rocq 9.2.0

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-72703 updated cvss 6.3

rocq: Rocq Prover: Logical Flaw Allows Arbitrary Proof Generation via Unchecked Cross-Calls

  • 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/endrazine/rocq-cve-poc-21682 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
  • CWE-670 Always-Incorrect Control Flow Implementation

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.