CVE-2026-72705

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.

• CWE-670

• 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

Published

Aug 24, 2026

Last Modified

Sep 8, 2026

Status

Deferred

• How Strix found a critical auth bypass in etcdStrix autonomously discovered a critical authentication bypass in etcd, later designated CVE-2026-33413.
• Autonomous PentestingAI agents that find and validate exploitable vulnerabilities like this one across your applications.
• PR ReviewsPentest every pull request so vulnerable code is caught before it ships to production.
• AI Penetration TestingHow AI-driven penetration testing continuously covers your attack surface.

• CVE-2026-7270An operator precedence bug in the kernel results in a scenar…7.8
• CVE-2026-72700The getgrav/grav-plugin-login Composer plugin before 3.9.1 (…7.5
• CVE-2026-72701Grav CMS before 2.0.16 contains a timing vulnerability in Ut…3.7
• CVE-2026-72702Grav CMS before 2.0.16 contains an origin validation bypass …5.4
• CVE-2026-72703The guard checker in Rocq Prover treats a parameter of a nes…6.3
• CVE-2026-72704The guard checker in Rocq Prover does not recheck the recurs…6.3
• CVE-2026-72708SPIP before 4.4.18 contains an unauthenticated blind SQL inj…7.5
• CVE-2026-72709SPIP before version 4.4.18 contains a missing authorization …9.8
• CVE-2026-7271A vulnerability was detected in DV0x creative-ad-agent up to…5.5
• CVE-2026-72710SPIP before 4.4.18 contains a mass assignment vulnerability …9.8
• CVE-2026-72711The Lean 4 kernel does not check that the body of an opaque …6.3
• CVE-2026-72712Nmap versions up to and including 7.99 contains a denial of …6.5