CVE-2026-72705
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.
- CVSS 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 - CVSS 3.1
- 6.3
CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N - EPSS
- 0.2% chance of exploitation in the next 30 days; higher than 7% of CVEs (scores of 2026-10-25)
- CWE
- CWE-670
- Published
- Modified
- Record from
- the NVD, synced