CVE-2026-72705
Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument
- Published
- Aug 24, 2026
- Updated
- Oct 26, 2026
- Assigning CNA
- VulnCheck
- Evidence observed
- Oct 26, 2026
Primary CVSS
nvd · CVSS 4.0
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:XLow · next 30 days
- Percentile
- 7.1%
- Model date
- Oct 25, 2026
EPSS is a statistical estimate, not a certainty or a measure of impact. Combine it with CVSS, KEV status, exposure and your environment.
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.
Sources
CVE-2026-72705 — Rocq Guard Checker Accepts Fixpoint Passed as Higher-Order Argument
Responsible use
Use vulnerability information only on systems you own or are authorized to test. Kitploit links to public research metadata and does not store exploit code or malicious payloads.