CVE-2026-72704
Received Received - Intake

Guard Checker Bypass in Rocq Prover Leads to False Proof

Publication date: 2026-08-24

Last updated on: 2026-08-24

Assigner: VulnCheck

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.

CVSS Scores

EPSS Scores

Probability:
Percentile:

Meta Information

Published
2026-08-24
Last Modified
2026-08-24
Generated
2026-08-25
AI Q&A
2026-08-24
EPSS Evaluated
N/A
NVD
CVE-2026-72704
EUVD
EUVD-2026-65140

Affected Vendors & Products

Showing 4 associated CPEs
Vendor Product Version / Range
rocq_prover rocq_prover to 9.2.0 (inc)
rocq_prover rocq_prover to 9.1 (inc)
coq coq 8.*
rocq_prover rocq_prover *

Helpful Resources

Exploitability

CWE
CWE Icon
KEV
KEV Icon
CWE ID Description
CWE-670 The code contains a control flow path that does not reflect the algorithm that the path is intended to implement, leading to incorrect behavior any time this path is navigated.

Attack-Flow Graph

AI Quick Actions

Instant insights powered by AI
Executive Summary

CVE-2026-72704 is a vulnerability in the Rocq Prover (formerly Coq) kernel's guard checker. The guard checker fails to recheck the recursive tree representation of an inductive type parameter after it is modified by transport. This allows a fixpoint to apply a rewrite along an equality between types to its recursive argument, which the guard checker accepts because the inductive type is preserved. However, the recursive tree recorded for the parameter is altered, leading to a non-terminating definition being accepted as terminating. This can prove false statements like 0 equals 1, deriving a contradiction from consistent axioms.

Detection Guidance

This vulnerability is specific to the Rocq Prover (formerly Coq) and cannot be detected via standard network or system commands. It requires checking the version of Rocq/Coq installed and verifying if it is affected (versions ≤ 9.2.0). Use commands like 'rocqc --version' or 'coqc --version' to check the installed version.

Impact Analysis

This vulnerability allows attackers to exploit the guard checker to prove false statements, such as 0 equals 1, from consistent axioms. Systems relying on Rocq's kernel-checked proofs with axioms consistent with univalence are affected. This includes formally verified software like CompCert, CertiKOS, and Iris, as well as proof-carrying code. The impact is significant for any system where proof correctness is critical.

Compliance Impact

This vulnerability does not directly affect compliance with GDPR or HIPAA as it pertains to a proof assistant's kernel soundness rather than data protection or healthcare systems. However, systems relying on Rocq's kernel-checked proofs for formal verification (e.g., CompCert, CertiKOS) could produce unsound results, potentially undermining compliance in contexts where such proofs are required for certification or validation.

Mitigation Strategies

Immediately upgrade Rocq Prover to a version beyond 9.2.0 or apply the fix from PR #22027. If using Coq, ensure you are on a patched version. Avoid using univalence or related axioms in proofs until the fix is applied. Review and re-verify all proofs that rely on fixpoints or inductive types.

Chat Assistant

Ask questions about this CVE
Hi! I’m here to help you understand CVE-2026-72704. Ask me anything about the vulnerability, its impact, or mitigation strategies.
0/70

EPSS Chart