# CVE-2026-72705

## Summary

- **CVE ID:** CVE-2026-72705
- **Severity:** MEDIUM
- **CVSS Score:** 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)
- **CWE:** CWE-670
- **Published:** Aug 24, 2026
- **Last Modified:** Aug 29, 2026

## Description

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.

## Affected Products

- rocq-prover — rocq (0)

## References

- [CNA](https://github.com/rocq-prover/rocq)
- [CNA](https://github.com/rocq-prover/rocq/issues/21683)
- [CNA](https://github.com/rocq-prover/rocq/pull/21684)
- [CNA](https://github.com/endrazine/rocq-cve-poc-21683)
- [CNA](https://www.vulncheck.com/advisories/rocq-prover-before-guard-checker-accepts-fixpoint-passed-as-a-higher-order-argument)

## Exploitation Prediction (EPSS)

- **EPSS Score:** 0.12%
- **EPSS Percentile:** 2.1

---
_Exported from OnDuty AI Vulnerability Intelligence on 2026-09-10._