TI-2026-50941 Aliases CVE-2026-72703 GHSA-q4cf-fp8g-gjg9

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

MEDIUM 63CWE-670Published 2026-08-24 · Updated 2026-10-26

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

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

Vendor	Product	Affected versions	Fixed in	Status	Source
rocq-prover	rocq	8.20 to before 9.2.0	9.2.0	Patch available	CNA

rocq Vendorrocq-prover Affected 8.20 to 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 · 2026-08-24
rocq-prover rocq 9.2.0
2 records Highest priority Priority MEDIUM 2 MEDIUM
Other records, highest priority first
- TI-2026-50943 Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order ArgumentPriority MEDIUM 63
Show all 2 records →

Vendor assessments

Red Hat

Red Hat's page for this CVE →

Not affected: 1 product

Red Hat

Timeline

2026-10-02 Threatist record created from CVE-2026-72703
2026-10-03 Alias added: GHSA-q4cf-fp8g-gjg9

References

Exploit 1

https://github.com/endrazine/rocq-cve-poc-21682

Patch 1

https://github.com/rocq-prover/rocq/pull/21684

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-50943 Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument 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-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