{"cve":"CVE-2026-72705","nvd":{"published":"2026-08-24T20:17:18.520","modified":"2026-10-26T02:17:07.363","status":"Deferred","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.","cvss_v4":{"vector":"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","score":6.8},"cvss_v3":{"version":"3.1","vector":"CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N","score":6.3},"cwes":["CWE-670"],"references":["https://github.com/endrazine/rocq-cve-poc-21683","https://github.com/rocq-prover/rocq","https://github.com/rocq-prover/rocq/issues/21683","https://github.com/rocq-prover/rocq/pull/21684","https://www.vulncheck.com/advisories/rocq-prover-before-guard-checker-accepts-fixpoint-passed-as-a-higher-order-argument"],"products":[],"source":"nvd","synced_at":"2026-10-26T02:37:26.505365588+00:00"},"epss":{"cve":"CVE-2026-72705","score":0.00176,"percentile":0.07064,"date":"2026-10-25"},"kev":null,"osv":[],"attribution":["This product uses the NVD API but is not endorsed or certified by the NVD.","EPSS scores: FIRST Exploit Prediction Scoring System, https://www.first.org/epss","Known exploited vulnerabilities: CISA Known Exploited Vulnerabilities Catalog, https://www.cisa.gov/known-exploited-vulnerabilities-catalog","Package advisories: OSV (https://osv.dev), from the GitHub Advisory Database, PyPA, Go, RustSec and other ecosystem databases, under CC-BY 4.0 or CC0","CVE records: the CVE Program's CVE List (https://www.cve.org), under its terms of use (https://www.cve.org/Legal/TermsOfUse). CVE is a registered trademark of The MITRE Corporation; this product is not affiliated with the CVE Program."]}