CVE-2026-72703: Rocq Prover Privilege Escalation Vulnerability

CVE-2026-72703 Overview

CVE-2026-72703 is a soundness flaw in the Rocq Prover (formerly Coq) guard checker. The find_uniform_parameters function in kernel/inductive.ml inspects only self-recursive calls when classifying parameters of a nested mutual fixpoint as uniform. When no body calls itself, the checker concludes that every parameter is uniform, ignoring cross-calls between distinct bodies. A parameter that grows through a cross-call retains the subterm specification of the enclosing fixpoint, so a recursive call guarded by that specification is accepted even though the argument is not structurally smaller. The result is that a non-terminating definition is admitted as structurally decreasing, allowing derivation of a proof of False and therefore of any proposition. The flaw was introduced in Coq 8.20 and fixed in Rocq 9.2.0.

Critical Impact
Any Rocq/Coq development between 8.20 and 9.2.0 can be used to construct a closed proof of False without axioms, plugins, or unsafe flags, invalidating the trust base of dependent formal proofs.

Affected Products

Coq Proof Assistant 8.20 and later 8.x releases
Rocq Prover releases prior to 9.2.0
Downstream libraries and developments compiled against the affected kernel

Discovery Timeline

2026-08-24 - CVE-2026-72703 published to the National Vulnerability Database
2026-08-27 - Last updated in NVD database

Technical Details for CVE-2026-72703

Vulnerability Analysis

Rocq's kernel enforces logical consistency by requiring that every recursive definition terminates. The guard checker approves a fixpoint only when each recursive call is made on a structurally smaller argument. For nested mutual fixpoints, the kernel first identifies uniform parameters, those that remain unchanged across recursive calls, and then propagates subterm specifications through them. The function find_uniform_parameters in kernel/inductive.ml performs this classification. It walks the body of each fixpoint component looking for self-recursive calls and checks whether their arguments match the declared parameter positions. It does not, however, inspect calls made from one body of the mutual block to a sibling body. When every component of the mutual fixpoint lacks a self-recursive call, the traversal finds nothing to constrain the parameters, and the checker defaults to marking them all uniform. A cross-call can then pass a strictly growing argument in one of those positions while the callee reuses the caller's subterm specification. The kernel accepts a non-terminating definition as structurally decreasing, and the resulting term evaluates to its own successor, yielding an inhabitant of False.

Root Cause

The defect is an improper control-flow assumption tracked as [CWE-670]. The uniform-parameter analysis is not sound with respect to mutual recursion because it examines only intra-body recursion. The fix in Rocq 9.2.0 extends the analysis to consider cross-body calls when determining uniformity.

Attack Vector

Exploitation requires an author to write and typecheck a specifically shaped mutual fixpoint. Print Assumptions reports the resulting proof of False as closed under the global context, so the malicious proof is indistinguishable from a legitimate one to any consumer that trusts the compiled .vo output. The primary risk is supply-chain: a malicious or mistaken library can distribute an unsound term that downstream projects import and rely on. See the VulnCheck advisory and the upstream issue #21682 for detailed technical discussion.

A proof-of-concept demonstrating the derivation of False is published at the rocq-cve-poc-21682 repository.

Detection Methods for CVE-2026-72703

Indicators of Compromise

Rocq or Coq installations reporting a version between 8.20 and any release prior to 9.2.0 via rocq --version or coqc --version.
Source files defining nested mutual fixpoints where no component contains a self-recursive call but bodies call each other with a growing argument.
.vo object files produced by an affected compiler that later fail to typecheck under Rocq 9.2.0 or newer.

Detection Strategies

Recompile all first-party and vendored Rocq developments under Rocq 9.2.0 and treat guard-checker rejections as findings requiring review.
Audit dependency manifests such as opam files and dune-project for pinned Coq or Rocq versions in the 8.20 through 9.1.x range.
Search source trees for Fixpoint ... with ... and CoFixpoint ... with ... constructs and inspect each for cross-call growth patterns.

Monitoring Recommendations

Track the Rocq compiler version used in continuous-integration pipelines and alert when builds run on affected releases.
Monitor package registries and Git submodules that pull Rocq libraries for advisories referencing CVE-2026-72703.
Retain build logs from coqc and rocq compile invocations so that historical proofs can be re-validated after the upgrade.

How to Mitigate CVE-2026-72703

Immediate Actions Required

Upgrade all Rocq Prover installations to version 9.2.0 or later on developer workstations, build servers, and continuous-integration runners.
Rebuild every downstream library and proof development from source under the patched compiler and treat any new guard-checker error as a correctness issue.
Revoke trust in pre-built .vo artifacts distributed by third parties until they are recompiled under Rocq 9.2.0 or later.

Patch Information

The fix landed in Rocq 9.2.0 via pull request #21684 in the rocq-prover/rocq repository. The patch extends find_uniform_parameters in kernel/inductive.ml so that cross-calls between components of a mutual fixpoint are inspected when determining whether a parameter is uniform.

Workarounds

Prohibit the use of nested mutual fixpoints in reviewed code until the upgrade is complete.
Require peer review of any commit that introduces a Fixpoint ... with ... block and reject definitions that rely on cross-call growth.
Run Print Assumptions on critical theorems and manually inspect proofs originating from untrusted sources, keeping in mind that this command alone will not flag the exploit.

bash

# Verify the installed Rocq version and upgrade via opam
rocq --version
opam update
opam install rocq-prover.9.2.0
# Rebuild dependent developments under the patched compiler
dune build --force