CVE-2026-72704

Name of the Vulnerable Software and Affected Versions Rocq Prover (affected versions not specified)

Description The guard checker fails to recheck the recursive tree representation of an inductive type parameter after it has been modified by transport. This allows a fixpoint to apply a rewrite along an equality between types to its recursive argument; while the guard checker accepts this because the inductive type is preserved, the recorded recursive tree for the parameter is altered. A subsequent fixpoint calling the first inherits this altered tree without verification, allowing non-structurally decreasing calls to be accepted as terminating. This can lead to non-terminating definitions that prove false propositions, such as a natural number equaling its own successor.

Recommendations At the moment, there is no information about a newer version that contains a fix for this vulnerability.