CVE-2026-72705
Received Received - Intake

Type Confusion in Rocq Prover via Higher-Order Fixpoint Arguments

Publication date: 2026-08-24

Last updated on: 2026-08-24

Assigner: VulnCheck

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 Scores

EPSS Scores

Probability:
Percentile:

Meta Information

Published
2026-08-24
Last Modified
2026-08-24
Generated
2026-08-25
AI Q&A
2026-08-24
EPSS Evaluated
N/A
NVD
CVE-2026-72705
EUVD
EUVD-2026-65141

Affected Vendors & Products

Showing 4 associated CPEs
Vendor Product Version / Range
rocq prover 9.2.0
rocq_prover rocq 9.2.0
rocq_prover rocq to 9.2.0 (exc)
coq coq *

Helpful Resources

Exploitability

CWE
CWE Icon
KEV
KEV Icon
CWE ID Description
CWE-670 The code contains a control flow path that does not reflect the algorithm that the path is intended to implement, leading to incorrect behavior any time this path is navigated.

Attack-Flow Graph

AI Quick Actions

Instant insights powered by AI
Executive Summary

This vulnerability in Rocq Prover (formerly Coq) allows bypassing the guard checker to prove False (0 = 1) without using axioms or unsafe features. It occurs because the guard checker incorrectly accepts fixpoints that pass themselves as higher-order arguments to another fixpoint, which then calls them on non-subterms of the structural argument. This enables a Russell-style paradox in just 4 lines of code, constructing a type that is definitionally equal to its own negation.

Detection Guidance

This vulnerability is specific to the Rocq Prover (formerly Coq) and cannot be detected using standard network or system commands. Instead, check if your Rocq version is 9.1.0 or earlier. If so, the system is vulnerable. Upgrade to Rocq 9.2.0 or later to resolve the issue.

Impact Analysis

The impact is severe as any system trusting Rocq's kernel-checked proofs could be compromised. This includes formally verified software like CompCert or CertiKOS, smart contracts, AI-generated proofs, and other systems relying on Rocq's correctness guarantees. The vulnerability allows proving False, which could undermine the integrity of proofs in these systems.

Compliance Impact

This vulnerability allows proving False in purely definitional code without axioms or unsafe flags, compromising the integrity of proofs in Rocq. Systems relying on Rocq's kernel-checked proofs, such as formally verified software, could produce incorrect results, potentially violating compliance with standards requiring data integrity and proof correctness like GDPR's accuracy principle or HIPAA's integrity requirements.

Mitigation Strategies
  • Upgrade Rocq Prover to version 9.2.0 or later immediately to patch the guard checker vulnerability.
  • Review all proof scripts for potential paradoxical constructs or proofs of False, especially those using higher-order fixpoints.
  • Avoid using versions of Rocq or Coq prior to 9.2.0 for critical or security-sensitive applications.

Chat Assistant

Ask questions about this CVE
Hi! I’m here to help you understand CVE-2026-72705. Ask me anything about the vulnerability, its impact, or mitigation strategies.
0/70

EPSS Chart