CVE-2026-72705: Always-Incorrect Control Flow Implementation in rocq-prover rocq
CVE-2026-72705 is a vulnerability in Rocq Prover's guard checker that incorrectly handles recursive calls made through a fixpoint's own arguments. This flaw allows a fixpoint to pass itself as a higher-order argument to another fixpoint, enabling a type to be definitionally equal to its own negation. This leads to self-application producing False in purely definitional code without requiring tactics, axioms, plugins, or unsafe flags. The issue is fixed in Rocq version 9.2.0.
AI Analysis
Technical Summary
The guard checker in Rocq Prover fails to track recursive calls passed as higher-order arguments through fixpoints. While passing a recursive function to a plain definition is rejected due to unfolding and observation of the call, passing it to a fixpoint is accepted because such higher-order recursive calls are not tracked. This flaw permits a type to be definitionally equal to its own negation, causing self-application to yield False purely through definitional code. The vulnerability does not require additional tactics, axioms, plugins, or unsafe flags, and the result is reported as closed under the global context. The issue is resolved in Rocq 9.2.0.
Potential Impact
This vulnerability undermines the soundness of the Rocq Prover by allowing a type to be equal to its own negation, effectively breaking logical consistency within the system. This could lead to incorrect proofs or verification results, impacting the reliability of software or systems verified using affected versions of Rocq Prover.
Mitigation Recommendations
Upgrade to Rocq version 9.2.0 or later, where this vulnerability has been fixed. No other mitigation or workaround is indicated.
CVE-2026-72705: Always-Incorrect Control Flow Implementation in rocq-prover rocq
Description
CVE-2026-72705 is a vulnerability in Rocq Prover's guard checker that incorrectly handles recursive calls made through a fixpoint's own arguments. This flaw allows a fixpoint to pass itself as a higher-order argument to another fixpoint, enabling a type to be definitionally equal to its own negation. This leads to self-application producing False in purely definitional code without requiring tactics, axioms, plugins, or unsafe flags. The issue is fixed in Rocq version 9.2.0.
CVSS v4.0
Score 6.8medium
Affected software
Run on your own infrastructure? Check whether these packages are installed with threat-finder — our free open-source scanner.
AI-Powered Analysis
Machine-generated threat intelligence
Technical Analysis
The guard checker in Rocq Prover fails to track recursive calls passed as higher-order arguments through fixpoints. While passing a recursive function to a plain definition is rejected due to unfolding and observation of the call, passing it to a fixpoint is accepted because such higher-order recursive calls are not tracked. This flaw permits a type to be definitionally equal to its own negation, causing self-application to yield False purely through definitional code. The vulnerability does not require additional tactics, axioms, plugins, or unsafe flags, and the result is reported as closed under the global context. The issue is resolved in Rocq 9.2.0.
Potential Impact
This vulnerability undermines the soundness of the Rocq Prover by allowing a type to be equal to its own negation, effectively breaking logical consistency within the system. This could lead to incorrect proofs or verification results, impacting the reliability of software or systems verified using affected versions of Rocq Prover.
Mitigation Recommendations
Upgrade to Rocq version 9.2.0 or later, where this vulnerability has been fixed. No other mitigation or workaround is indicated.
Technical Details
- Data Version
- 5.2
- Assigner Short Name
- VulnCheck
- Date Reserved
- 2026-08-10T13:02:52.001Z
- Cvss Version
- 4.0
- State
- PUBLISHED
- Remediation Level
- null
Threat ID: 6a8ca814acd9273b49150590
Added to database: 08/24/2026, 20:22:44 UTC
Last enriched: 08/24/2026, 20:37:31 UTC
Last updated: 08/24/2026, 20:47:01 UTC
Views: 4
Community Reviews
0 reviewsCrowdsource mitigation strategies, share intel context, and vote on the most helpful responses. Sign in to add your voice and help keep defenders ahead.
Want to contribute mitigation steps or threat intel context? Sign in or create an account to join the community discussion.
Actions
Updates to AI analysis require Pro Console access. Upgrade inside Console → Billing.
Need more coverage?
Upgrade to Pro Console for AI refresh and higher limits.
For incident response and remediation, OffSeq services can help resolve threats faster.
Latest Threats
Check if your credentials are on the dark web
Instant breach scanning across billions of leaked records. Free tier available.