The vulnerability in rocq-prover's rocq arises because the guard checker does not recheck the recursive tree representation of an inductive type parameter after it has been changed by transport. Specifically, a fixpoint may rewrite its recursive argument along an equality between types, which the guard checker accepts since the inductive type remains the same, but the recursive tree is altered. A second fixpoint calling the first inherits this altered recursive tree without verification, allowing a call that is not structurally decreasing to be accepted as terminating. This flaw enables the construction of a non-terminating definition that proves a natural number equals its own successor and thus False, from which any proposition can be derived. The demonstration relies on two axioms consistent with the calculus of inductive constructions, indicating the contradiction stems from the guard check implementation rather than the axioms themselves. Although a fix has been proposed, it has not been merged into the codebase.

This vulnerability undermines the logical soundness of the rocq-prover system by allowing non-terminating definitions to be accepted as terminating. This leads to the derivation of false propositions, effectively breaking the trustworthiness of proofs constructed using the affected versions. The impact is significant within the context of formal verification and theorem proving, as it compromises the integrity of proofs relying on the system.

No official fix or patch is currently available for this vulnerability. A fix has been proposed but not merged. Users should monitor the vendor's advisories for updates regarding an official remediation. Until a fix is released, caution is advised when using affected versions, especially in contexts requiring high assurance of proof correctness.