{"apiVersion":"1.0","identifier":"CVE-2026-72705","description":"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.","publishedAt":"2026-08-24T20:17:18","lastModifiedAt":"2026-08-26T17:17:13","sourceUrl":"https://nvd.nist.gov/vuln/detail/CVE-2026-72705","cvssScore":6.3,"cvssVector":"CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N","epssProbability":0.0012,"riskScore":0.64,"affectedProduct":"Rocq Prover","affectedVersions":"<9.2.0","vulnerabilityType":"Library","operatingSystems":[],"links":{"self":"https://www.redsauce.net/api/cves/CVE-2026-72705","webPages":{"es":"https://www.redsauce.net/es/cves/CVE-2026-72705","en":"https://www.redsauce.net/en/cves/CVE-2026-72705","fr":"https://www.redsauce.net/fr/cves/CVE-2026-72705","pt":"https://www.redsauce.net/pt/cves/CVE-2026-72705","de":"https://www.redsauce.net/de/cves/CVE-2026-72705","sk":"https://www.redsauce.net/sk/cves/CVE-2026-72705","el":"https://www.redsauce.net/el/cves/CVE-2026-72705"},"source":"https://nvd.nist.gov/vuln/detail/CVE-2026-72705"}}