{"id":"CVE-2026-72705","title":"The guard checker in Rocq Prover does not follow recursive calls made through a fixpoint's own arguments","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 …","severity":"medium","cvss":6.3,"cvssVector":"CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N","cwe":["CWE-670"],"published":"2026-08-24","updated":"2026-09-08","sourceUpdated":"2026-09-08T20:23:49.880","source":"NVD","sourceUrl":"https://nvd.nist.gov/vuln/detail/CVE-2026-72705","references":[{"url":"https://github.com/endrazine/rocq-cve-poc-21683","label":"disclosure@vulncheck.com"},{"url":"https://github.com/rocq-prover/rocq","label":"disclosure@vulncheck.com"},{"url":"https://github.com/rocq-prover/rocq/issues/21683","label":"disclosure@vulncheck.com"},{"url":"https://github.com/rocq-prover/rocq/pull/21684","label":"disclosure@vulncheck.com"},{"url":"https://www.vulncheck.com/advisories/rocq-prover-before-guard-checker-accepts-fixpoint-passed-as-a-higher-order-argument","label":"disclosure@vulncheck.com"}],"tags":["nvd"],"epss":0.0012,"epssPercentile":0.02112,"ingestedAt":"2026-09-08T21:11:12.285Z","slug":"CVE-2026-72705","body":"## Overview\n\nThe 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.\n\n## Remediation\n\nRefer to the linked advisories for vendor-supplied fixes and affected version ranges.","depth":"sunlit","depthScore":35,"depthScoreParts":{"impact":34.7,"likelihood":0,"exploitation":0,"ransomware":0},"changes":[]}