CVE-2026-72703 in Rocq
Summary
by MITRE • 08/24/2026
The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find_uniform_parameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes that every parameter is uniform. A parameter that grows through a cross-call from one body to another therefore keeps the subterm specification it inherited from the enclosing fixpoint, and a recursive call guarded by that specification is accepted although the argument is not structurally smaller. A non-terminating definition is admitted as structurally decreasing, which yields a term whose value equals its own successor and so a proof of False, from which any proposition follows. The proof requires no axioms, plugins or unsafe flags and Print Assumptions reports it as closed under the global context. Introduced in Coq 8.20 and fixed in Rocq 9.2.0.
If you want to get best quality of vulnerability data, you may have to visit VulDB.
Analysis
by VulDB Data Team • 08/24/2026
The vulnerability identified within the Rocq Prover represents a critical logical inconsistency arising from flawed termination checking mechanisms for nested mutual fixpoints. The core of this issue lies in how the guard checker, specifically the find_uniform_parameters function located in kernel/inductive.ml, evaluates structural recursion constraints. In formal verification systems like Coq and its successor Rocq, ensuring that recursive definitions terminate is paramount to maintaining logical soundness. The system relies on a concept known as uniformity, where parameters are checked to ensure they decrease structurally with each recursive call. However, the implementation flaw causes the checker to treat all parameters of a nested mutual fixpoint as uniformly decreasing without adequately examining the cross-calls between different bodies within that same mutual recursion block. This oversight means that if no individual body calls itself directly, the function incorrectly concludes that every parameter is uniform and thus structurally decreasing, regardless of how arguments are actually transformed during inter-body recursive steps.
This technical flaw allows for the construction of non-terminating definitions that are erroneously accepted as valid structural recursions. When a parameter grows through a cross-call from one body to another in a mutual fixpoint, it retains the subterm specification inherited from the enclosing context rather than being re-evaluated against its new value. Consequently, recursive calls guarded by this incorrect uniformity assumption are admitted even when their arguments do not become structurally smaller. This leads to the admission of terms whose values equal their own successors, a mathematical impossibility in standard type theory that effectively breaks the consistency of the logic. By exploiting this gap, an attacker or malicious user can construct a proof for False without requiring any additional axioms, plugins, or unsafe flags. The resulting term is reported as closed under the global context by Print Assumptions, giving a false sense of security regarding the validity and safety of the verified code.
The operational impact of this vulnerability is severe, as it undermines the fundamental guarantee of logical consistency provided by dependent type theory systems. In formal methods, if False can be proven, then any proposition becomes provable due to the principle of explosion. This renders all previously verified proofs within that context unreliable and potentially invalid. The flaw was introduced in Coq version 8.20 and persisted through subsequent releases until it was addressed in Rocq version 9.2.0. Systems relying on these versions for critical verification tasks, such as hardware correctness proofs or cryptographic protocol verifications, are at risk of accepting incorrect results if they utilize nested mutual fixpoints with cross-recursive calls that do not strictly decrease all parameters across the entire recursion cycle.
To mitigate this vulnerability, organizations must ensure their development environments and continuous integration pipelines are updated to use Rocq version 9.2.0 or later, where the guard checker has been corrected to properly inspect cross-calls within mutual fixpoints. For projects currently locked on older versions, manual review of all nested mutual recursive definitions is necessary to verify that every path through the recursion results in a structurally smaller argument for at least one parameter. Developers should also consider employing additional termination proofs or well-founded induction strategies as a defensive measure when dealing with complex mutual recursions until an upgrade can be performed. This issue highlights the importance of rigorous testing of core logical kernels, particularly regarding edge cases involving nested and mutually recursive structures that challenge standard uniformity assumptions.
From a classification perspective, this vulnerability aligns with CWE-20 Improper Input Validation, as the system fails to properly validate the structural decrease property across all relevant code paths within mutual recursions. It also relates to CWE-835 Loop of Doom, specifically involving infinite loops or non-terminating processes that are incorrectly deemed safe by static analysis tools. In terms of the MITRE ATT&CK framework for software development and supply chain security, this falls under T1602 Software Data Integrity Weaknesses, as it allows an adversary to inject logically invalid constructs into a trusted system without triggering standard safety checks. The lack of requirement for external plugins or unsafe flags makes this particularly dangerous in automated verification pipelines where such safeguards are typically the primary defense against logical errors.