{"id":"CVE-2026-72705","revision":"8bfa1ad315a049deaa33c873dade3142","records":[{"revision":"8bfa1ad315a049deaa33c873dade3142","observedAt":"2026-10-26T03:25:11.129+00:00","statement":{"source":"cve-program","id":"CVE-2026-72705","aliases":[],"title":"Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument","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.","state":0,"publishedAt":"2026-08-24T20:08:32.535+00:00","modifiedAt":"2026-10-26T01:23:56.439+00:00","affected":[{"ecosystem":"Vendor product","name":"rocq","ranges":[],"versions":[],"rawVersionEvidence":"{\n                    \"vendor\": \"rocq-prover\",\n                    \"product\": \"rocq\",\n                    \"repo\": \"https://github.com/rocq-prover/rocq\",\n                    \"packageURL\": \"pkg:github/rocq-prover/rocq\",\n                    \"defaultStatus\": \"unaffected\",\n                    \"versions\": [\n                        {\n                            \"version\": \"0\",\n                            \"lessThan\": \"9.2.0\",\n                            \"status\": \"affected\",\n                            \"versionType\": \"custom\"\n                        }\n                    ]\n                }"}],"metrics":[{"system":"CVSS 4.0","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,"severity":"MEDIUM"},{"system":"CVSS 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,"severity":"MEDIUM"}],"references":["https://github.com/rocq-prover/rocq","https://github.com/rocq-prover/rocq/issues/21683","https://github.com/rocq-prover/rocq/pull/21684","https://github.com/endrazine/rocq-cve-poc-21683","https://www.vulncheck.com/advisories/rocq-prover-before-guard-checker-accepts-fixpoint-passed-as-a-higher-order-argument"],"sourceUrl":"https://www.cve.org/CVERecord?id=CVE-2026-72705","license":"CVE Program Terms of Use","key":"cve-program:CVE-2026-72705","identifiers":["CVE-2026-72705"]},"retained":false,"historicalAffected":[]}],"coverage":[]}