endrazine/rocq-cve-poc-21683CVE-2026-72705 — Rocq Guard Checker Accepts Fixpoint Passed as Higher-Order Argument
Proving 0 = 1 axiom-free via Russell's paradox through guard checker fixpoint bypass.
Discovered autonomously by Claude Opus 4.6 (Anthropic).
| Field | Value |
|---|---|
| Bug report | rocq-prover/rocq#21683 |
| Fix | PR #21684 |
| Affected | Rocq ≤ 9.1.0 / all Coq versions with guard checker |
| Fixed in | 9.2.0 |
| CVSS 3.1 | AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1 |
| CWE | CWE-670 (Always-Incorrect Control Flow Implementation) |
| CVE | CVE-2026-72705 |
The guard checker accepts fixpoints that pass themselves as higher-order
arguments to another fixpoint, which then calls them on non-subterms of
the structural argument. Passing a recursive function to a Definition
(non-fixpoint constant) is correctly rejected — the guard checker unfolds
it and sees the problematic call. But passing it to a Fixpoint is
incorrectly accepted.
This creates a Russell-style paradox in 4 lines:
Definition delta (x : russell 1) : False := x x.
Definition omega : False := delta delta.
where russell 1 is definitionally equal to russell 1 -> False — a type
that is its own negation. Self-application gives False directly.
The exploit:
Print Assumptions reports "Closed under the global context"False is 4 lines of functional codeQed — purely definitionaldocker build -t rocq-cve-poc-21683 .
docker run --rm rocq-cve-poc-21683
Any system that trusts Rocq's kernel-checked proofs is affected:
iterate_to_neg f n seed :=
match n with
| 0 => f seed -> False (* negate after n steps *)
| S m => iterate_to_neg f m seed
end
russell n :=
match n with
| 0 => True
| S m => iterate_to_neg russell 1 (S m) (* passes ITSELF *)
end
The guard checker should reject russell because it passes itself as a
higher-order argument to iterate_to_neg, which then calls it on S m
(not a subterm of n). But the checker only tracks direct recursive calls,
not calls through higher-order fixpoint arguments.
russell 1 = iterate_to_neg russell 1 1
= iterate_to_neg russell 0 1
= russell 1 -> False
So russell 1 ≡ russell 1 -> False. This is the classical Russell set:
the set of all sets that don't contain themselves. Self-application gives:
delta : russell 1 -> False (* russell 1 = russell 1 -> False *)
delta x := x x (* x : russell 1 = russell 1 -> False *)
omega : False
omega := delta delta (* delta : russell 1 -> False = russell 1 *)
This bug was found autonomously by Claude Opus 4.6 during an overnight
fuzzing run set up by Tristan Stérin (@tcosmo), based on pointers from
Yannick Forster (@yforster) on the guard checker. The AI identified the
higher-order fixpoint bypass pattern and constructed the minimal
iterate_to_neg/russell exploit.
See: Zulip thread