CVE-2026-72703
Received Received - Intake

Rocq Prover Guard Checker Parameter Uniformity Flaw

Publication date: 2026-08-24

Last updated on: 2026-08-24

Assigner: VulnCheck

Description
The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find_uniform_parameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes that every parameter is uniform. A parameter that grows through a cross-call from one body to another therefore keeps the subterm specification it inherited from the enclosing fixpoint, and a recursive call guarded by that specification is accepted although the argument is not structurally smaller. A non-terminating definition is admitted as structurally decreasing, which yields a term whose value equals its own successor and so a proof of False, from which any proposition follows. The proof requires no axioms, plugins or unsafe flags and Print Assumptions reports it as closed under the global context. Introduced in Coq 8.20 and fixed in Rocq 9.2.0.

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-72703
EUVD
EUVD-2026-65139

Affected Vendors & Products

Showing 5 associated CPEs
Vendor Product Version / Range
inria coq 8.20
inria coq 9.2.0
rocq_prover rocq 8.20
rocq_prover rocq 9.1.0
rocq_prover rocq 9.2.0

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

This vulnerability in Rocq Prover (formerly Coq) involves the guard checker incorrectly treating parameters of nested mutual fixpoints as uniform without checking cross-calls between different fixpoint bodies. The function find_uniform_parameters only inspects self-recursive calls, so if no function calls itself, it assumes all parameters are uniform. This allows non-terminating fixpoints to be accepted as structurally decreasing, enabling proofs of False without requiring axioms or unsafe flags.

Detection Guidance

This vulnerability is specific to the Rocq Prover/Coq proof assistant and cannot be detected using standard network or system commands. It requires checking the version of Rocq/Coq installed on your system. If you are using Rocq/Coq versions prior to 9.2.0, your system is vulnerable.

Impact Analysis

The vulnerability allows attackers to construct proofs of False in Rocq Prover, which can then be used to derive any proposition. This undermines the soundness of proofs created with affected versions, potentially leading to incorrect or malicious results in formal verification tasks.

Compliance Impact

This vulnerability does not directly affect compliance with GDPR, HIPAA, or similar standards. It is a technical flaw in the Rocq Prover's guard checker that allows non-terminating fixpoints and proofs of False, which could undermine the reliability of formal proofs but does not inherently violate regulatory requirements.

Mitigation Strategies
  • Upgrade Rocq Prover to version 9.2.0 or later to address the guard checker unsoundness.
  • Review and update any proofs or definitions using nested mutual fixpoints to ensure they do not rely on the vulnerable behavior.
  • Monitor official Rocq Prover or Coq channels for further updates or patches related to this issue.

Chat Assistant

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

EPSS Chart