Guard Checker Flaw in Rocq Prover Affects Recursive Type Parameter Validation

CVE-2026-72704

What is CVE-2026-72704?

The Rocq Prover's guard checker contains a significant flaw whereby alterations to a recursive type parameter are not validated post-transport. This oversight allows a fixpoint to apply rewrites based on type equality, which may lead to the acceptance of an altered recursive tree that has not undergone proper verification. Consequently, calls to fixpoints that are not structurally decreasing could incorrectly be allowed, leading to non-terminating definitions such as asserting that a natural number equals its successor, which results in an inconsistency. This vulnerability undermines the fundamental veracity of logical assertions within the system, promoting false conclusions based on valid constructions. Although a proposed fix exists, it remains unmerged and highlights the need for immediate attention.

References