Description

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.

Executive Summary

Technical Details

Mitigations

References

Additional Metadata

{
  "score": "6.3",
  "pubDate": "2026-08-24T20:17:18.390Z",
  "pubdate": "2026-08-24T20:17:18.390Z",
  "executiveSummary": "A logic bypass vulnerability exists in the guard checker of Rocq Prover, resulting in unsoundness of the logical system and allowing the derivation of arbitrary propositions including False.\nThe vulnerability stems from the failure to recheck the recursive tree representation of an inductive type parameter after transport modifications via type equalities.\nAn attacker or user with the ability to define functions within the prover can construct non-terminating definitions that bypass structural recursion checks.\nSuccessful exploitation compromises the consistency of the theorem prover, enabling proofs of contradictory statements such as natural numbers equaling their own successors.\nThe risk implication is severe for formal verification pipelines, as false theorems can be proven using unproven or inconsistent axioms introduced by the bypassed guard mechanism.",
  "technicalDetails": "The vulnerable component is the guard checker within Rocq Prover, responsible for ensuring that fixpoint definitions are structurally terminating to maintain logical consistency under the calculus of inductive constructions.\nThe root cause of the vulnerability is that the guard checker fails to recheck the recursive tree representation of an inductive type parameter after that parameter has been altered by transport operations.\nExploitation occurs when a fixpoint applies a rewrite along an equality between types to its recursive argument. The guard checker accepts this because the outer inductive type is preserved, while the underlying recursive tree recorded for the parameter is covertly altered.\nA second fixpoint that subsequently calls the first inherits this altered recursive tree without performing additional verification.\nConsequently, a function call that is not structurally decreasing is improperly accepted by the system as terminating, allowing non-terminating recursion into the logic.\nThe resulting non-terminating definition enables the proof of contradictory statements, such as demonstrating that a natural number equals its own successor, ultimately deriving False and subverting the soundness guarantees of the prover."
}