{"id":"CVE-2026-72705","summary":"Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument","details":"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.","modified":"2026-09-10T03:30:49.725578858Z","published":"2026-08-24T20:08:32.535Z","database_specific":{"cwe_ids":["CWE-670"],"osv_generated_from":"https://github.com/CVEProject/cvelistV5/tree/main/cves/2026/72xxx/CVE-2026-72705.json","cna_assigner":"VulnCheck"},"references":[{"type":"ADVISORY","url":"https://github.com/CVEProject/cvelistV5/tree/main/cves/2026/72xxx/CVE-2026-72705.json"},{"type":"ADVISORY","url":"https://nvd.nist.gov/vuln/detail/CVE-2026-72705"},{"type":"ADVISORY","url":"https://www.vulncheck.com/advisories/rocq-prover-before-guard-checker-accepts-fixpoint-passed-as-a-higher-order-argument"},{"type":"REPORT","url":"https://github.com/rocq-prover/rocq/issues/21683"},{"type":"FIX","url":"https://github.com/rocq-prover/rocq/pull/21684"},{"type":"PACKAGE","url":"https://github.com/rocq-prover/rocq"},{"type":"EVIDENCE","url":"https://github.com/endrazine/rocq-cve-poc-21683"}],"affected":[{"ranges":[{"type":"GIT","repo":"https://github.com/rocq-prover/rocq","events":[{"introduced":"0"},{"fixed":"adfbf1855c348766beb4b790dcc8ebc02f908f63"}],"database_specific":{"source":"AFFECTED_FIELD","extracted_events":[{"introduced":"0"},{"fixed":"9.2.0"}]}}],"versions":["V9.2+rc2","V9.2+rc1","V8.21+alpha","V8.19+alpha","V8.10+alpha","V8.9+alpha","V8.8+alpha","V8.7+alpha"],"database_specific":{"source":"https://storage.googleapis.com/cve-osv-conversion/osv-output/CVE-2026-72705.json"}}],"schema_version":"1.9.0","severity":[{"type":"CVSS_V4","score":"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"}]}