{"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"],"vendor":"rocq-prover","product":"rocq","affected":["rocq < 9.2.0"],"published":"2026-08-24","updated":"2026-10-12","sourceUpdated":"2026-10-12T15:10:00.207","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","cve.org","exploit-available"],"epss":0.00176,"epssPercentile":0.07066,"exploitAvailable":true,"ssvc":{"exploitation":"poc","automatable":"no","technicalImpact":"partial","timestamp":"2026-08-26T15:46:51.503814Z"},"ingestedAt":"2026-09-08T21:11:12.285Z","exploits":{"github":1,"githubRepos":["https://github.com/endrazine/rocq-cve-poc-21683"],"checkedAt":"2026-10-27T19:10:50.260Z"},"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":"twilight","depthScore":47,"depthScoreParts":{"impact":34.7,"likelihood":0,"exploitation":12,"ransomware":0},"changes":[{"seq":210263,"id":"CVE-2026-72705","ts":1790264824808,"field":"exploit_available","old":"false","new":"true"}]}