Skip to content
Fencer Vulns
medium 6.3

CVE-2026-72705 json

Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument

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

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 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.

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

rocq: Rocq Prover: Logical inconsistency via untracked higher-order fixpoint arguments

  • 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-21683 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.