Read the docs
TI-2026-50943 Aliases CVE-2026-72705GHSA-f4rc-7978-q94g

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

Priority MEDIUM 63CWE-670Published · Updated

Key facts

Attack vector
Local
Privileges required
None
User interaction
Passive
Attack complexity
Low
Attack requirements
None
Impact type
—
Confidentiality · integrity · availability
None · High · None
Fix status
Fixed

Attack profile from CVSS 4.0 · CNA. Fix status from CNA.

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.

Why it matters now

Exploitation Proof of concept CISA SSVC · not in CISA KEV
EPSS 0.00176 7th percentileScored 2026-11-07
Public exploit Yes 1 exploit referenceTagged by the CNA
Fix Fixed rocq (rocq-prover): 9.2.0

SSVC decision points

CISA ADP · SSVC 2.0.3

Exploitation
Poc
Automatable
No
Technical impact
Partial

The decision (Track, Attend, Act) also depends on your mission and well-being impact; see CISA's SSVC guide.

Affected products

VendorProductAffected versionsFixed inStatusSource
rocq-proverrocqbefore 9.2.09.2.0Patch availableCNA
  • rocq Vendorrocq-prover Affected before 9.2.0 Fixed in 9.2.0 Patch available CNA

Remediation

  • Fix · CNA rocq (rocq-prover) Fixed in 9.2.0

Fixed in the same release

Records fixed by the same vendor advisory or release, as the CNA lists them.

  • Release ·

    rocq-prover rocq 9.2.0

    2 records Highest priority Priority MEDIUM 2 MEDIUM

    Other records, highest priority first

    • TI-2026-50941 Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-CallsPriority MEDIUM 63
    Show all 2 records →

Vendor assessments

Red Hat

Red Hat's page for this CVE →

Not affected: 1 product
  • Red Hat

Timeline

  1. 2026-10-02 Threatist record created from CVE-2026-72705
  2. 2026-10-03 Alias added: GHSA-f4rc-7978-q94g

References

Exploit 1

Patch 1

Other 2

  • TI-2026-50950 Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close CVSS 4.0MEDIUM 6.8
  • TI-2026-50942 Rocq Prover through 9.2.0 Guard Checker Trusts Corrupted Recursive Tree After Transport CVSS 4.0MEDIUM 6.8
  • TI-2026-50941 Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls CVSS 4.0MEDIUM 6.8
  • TI-2020-19392 Coq and Rocq Prover Print Assumptions Omits Unsafe Universe Checking Inlined Through Parameter Inline CVSS 4.0MEDIUM 6.8

Sources

This product uses the NVD API but is not endorsed or certified by the NVD. Sources and licences