CVE-2026-72704: Rocq Prover through 9.2.0 Guard Checker Trusts Corrupted Recursive Tree After Transport
The guard checker in Rocq Prover does not recheck the recursive tree representation of an inductive type parameter after that parameter has been changed by transport. A fixpoint may apply a rewrite along an equality between types to its recursive argument, which the guard checker accepts because the inductive type is preserved, while the recursive tree recorded for the parameter is altered. A second fixpoint that calls the first inherits the altered recursive tree without verification, so a call that is not structurally decreasing is accepted as terminating. The resulting non-terminating definition proves that a natural number equals its own successor and therefore False, from which any proposition follows. The demonstration uses two axioms that follow from univalence and are consistent with the calculus of inductive constructions, so the contradiction comes from the guard check rather than from the assumptions. A fix is proposed but not merged.
Affected Software
Event History
Frequently Asked Questions
Who is exposed to this issue?
Users of Rocq Prover through version 9.2.0 are affected when they rely on the prover's guard checker to enforce termination and preserve logical consistency. Exploitation requires accepting or compiling a crafted proof development; it is not a remote attack.
What does an attacker need to exploit the flaw?
An attacker needs to construct fixpoints that rewrite a recursive argument through an equality between types, then use a second fixpoint that inherits the altered recursive tree. The demonstrated contradiction also uses two axioms following from univalence, although the issue attributes the unsoundness to the missing guard-check verification.
What is the practical impact of a successful exploit?
A successful exploit permits a non-terminating definition to be accepted as terminating. This can prove that a natural number equals its successor, derive False, and consequently prove any proposition.
Is a fix available?
A fix has been proposed, but it was not merged as of the provided information. No released fixed version is identified.