From 99486c9d103926389ed6828a6284b9b2fa11a0a8 Mon Sep 17 00:00:00 2001 From: "Li, Amazing Ang" Date: Mon, 10 Aug 2026 18:28:18 +0800 Subject: [PATCH 1/3] skill: verification is source-state-specific, and the human grades findings MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Follow-up to #4. Four things that review caught, one of them a self-contradiction in the protocol as shipped. **The blocker.** The demo's EVIDENCE was finalized while the last verifier round returned `failed`, one of its findings was behavioural, and the state that ships was never verified — which the protocol's own four states forbid. The fix is not a seventh round and not a fifth state: a verdict attaches to the state a verifier actually saw, so a state none saw is `not performed`, however many rounds preceded it. Fixing a behavioural finding after the final permitted round therefore ships an unverified state, and that is recorded as a declared downgrade with the earlier rounds kept as history. The demo's report now says so at the top. **Who grades.** "Behavioural findings buy a round, description findings do not" was left for whoever was holding the pen — which is the builder, who has an obvious incentive to call a boundary defect a documentation defect. The human decides any material or disputed grade and approves stopping at the cap. It matters most when a finding touches the SPEC, where the question is exactly whether the document is wrong about correct code or has exposed a requirement nobody wrote down — the same call that already sends SPEC gaps to the human. **"Exactly four inputs"** was literally false: phase two hands over the draft EVIDENCE. Retitled to blind-phase inputs. The first attack step also told the verifier that a mismatch means the draft is wrong — before it can see the draft, and ignoring that a mismatch can come from environment, freshness or nondeterminism. It now suspends the claim until those are reconciled instead of picking a winner. **Over-claiming for the gauntlet.** The text said it "proves the code satisfies every constraint the spec expresses" and "is not what is in question here", while the case study behind it shows a coverage layer that could not fail, a mutation runner executing the wrong bytecode, and a checker guarding a spelling. The gauntlet is evidence, not self-authentication. Also: the case study moved to references/verifier-case-study.md and is marked do-not-load-while-running. It names the defect classes one codebase happened to have, and an attacker primed with that list looks there first and elsewhere second. SKILL.md's section is down from 57 lines to 39. Co-Authored-By: Claude Opus 5 (1M context) --- demo-rate-limiter/evidence.md | 20 +++- skills/old-coder/SKILL.md | 93 ++++++++----------- skills/old-coder/references/gauntlet.md | 8 +- .../references/verifier-case-study.md | 36 +++++++ skills/old-coder/references/verifier.md | 70 +++++++------- 5 files changed, 130 insertions(+), 97 deletions(-) create mode 100644 skills/old-coder/references/verifier-case-study.md diff --git a/demo-rate-limiter/evidence.md b/demo-rate-limiter/evidence.md index 255ca24..57255b1 100644 --- a/demo-rate-limiter/evidence.md +++ b/demo-rate-limiter/evidence.md @@ -4,9 +4,13 @@ each contract change item by item before implementation. Earlier revisions (2026-07-25, 2026-07-27) were autonomous and are still unapproved; treat them as the weaker part of the spec. -- Independent verification: **six fresh-context rounds**, the last against - commit `d0b506c`. See "Independent verification" below — including what the - final round found and what was deliberately left unfixed. +- Independent verification: **not performed against the final source state + `8b88bda`.** Six earlier rounds were performed; the last verified state + `d0b506c` returned `failed`, and the fixes made since — one of them + behavioural — are disclosed below as unverified. This report is finalized as + a **declared downgrade**, not on the strength of a passing verdict. A + verdict attaches to the state a verifier actually saw, and no verifier has + seen this one. - Source state: git commit `8b88bda`; sha256 tree hash `c80e8cccf0a1ed3a` — reproduce both with `./tools/source_state.sh` (works from any directory; now includes `.github/workflows`, which decides whether the gauntlet runs @@ -126,8 +130,14 @@ converge just because one round comes back clean. **Verification stopped after round 6, deliberately.** A rule of "fix every finding, then start a new verifier" only terminates when a round returns the -empty set, and prose has no such fixpoint. The findings below were fixed after -round 6 and are therefore **not independently verified**: +empty set, and prose has no such fixpoint. + +That decision has a price this report states rather than hides: round 6's +verdict was `failed`, one of its findings was behavioural, and the state that +ships was never verified. Under the protocol's own four states, that makes the +final state `not performed` — the earlier rounds are history, not a +certificate. The following were fixed after round 6 and are **not +independently verified**: - the sweep threshold magnitude test and mutant M23; - the vacuous-pass assertion added to the clock-ordering test; diff --git a/skills/old-coder/SKILL.md b/skills/old-coder/SKILL.md index 297aafa..3489720 100644 --- a/skills/old-coder/SKILL.md +++ b/skills/old-coder/SKILL.md @@ -12,9 +12,11 @@ Your job is to make those two artifacts trustworthy enough that line-by-line review becomes optional within the spec's boundaries. This inverts the normal review model: **trust moves from inspection to -constraints.** Be honest about what that buys: the gauntlet proves the code -satisfies every constraint the spec expresses — it cannot prove the spec -expresses everything that matters. That is exactly why the human approves the +constraints.** Be honest about what that buys: the gauntlet turns the +constraints the spec expresses into executable evidence — it cannot show the +spec expresses everything that matters, and it is not self-authenticating, +because a checker can be unsound and a mapping can claim more than it +demonstrates. That is exactly why the human approves the SPEC (the one artifact that breaks the everything-authored-by-the-same-agent correlation), and why EVIDENCE reports layered, auditable confidence, never absolute proof. Every shortcut you take against the gauntlet destroys the only @@ -228,59 +230,42 @@ Scale effort to blast radius, and say which tier you chose: ## Independent verification (Tier 3 option, experimental) -The gauntlet is not what is in question here. It proves the code satisfies -every constraint the spec expresses, and it does that well. What no layer can -check is whether the **spec expresses the right constraints**, or whether -EVIDENCE honestly describes the code that shipped. Human spec approval is this -skill's answer to the first — but it happens before any code exists, so it -cannot catch anything you did afterwards. +The gauntlet is evidence, not self-authentication: its checkers can be +unsound, its mappings can overclaim, and the spec can be incomplete. Human +spec approval covers only the last, and only before any code exists. -Independent verification is a second answer for stakes that justify one: a +Independent verification answers the rest where the stakes justify it: a fresh-context agent that attacks the finished work before EVIDENCE is signed. -It reduces **task-context** correlation — your framing, your justifications, -the assumption you carried since turn 3. On the same model or model family, -model-level blind spots remain. Neither is independence in a strong sense, and -EVIDENCE says so. - -**It is not a gauntlet layer.** Every layer is a command that returns an exit -code in seconds. This is an agent that takes minutes, costs tokens on the -order of a small task, and returns **prose someone has to judge** — findings -to grade, equivalent mutants to rule out, false positives to dismiss. It -spends the one resource this skill otherwise guards carefully: human -attention. Reach for it when a spec gap would be expensive and the code is -already green, not because a task feels important. - -Marked experimental: the evidence for it is one case study, written up in -`references/verifier.md`, not a benchmark. - -The non-negotiable rules — **the protocol is `references/verifier.md`, and -verification has not been performed until that file has been read in full and -executed. Missing or unreadable → `blocked`, never `passed`.** - -- **Fresh context, four inputs only**: the task contract (the request plus - every requirement the human has approved since), the approved SPEC, the repo - at an exact source state, the gauntlet entry point. Never your conversation. -- **Blind first, compare second.** The verifier reproduces and attacks alone, - records what it found, and only then sees the draft EVIDENCE. That record is - append-only afterwards. -- **It fixes nothing.** A verifier that patches code becomes an author. A SPEC - gap goes back to the **human**, never to the builder to self-amend. -- **Grade the findings, or this never terminates.** A **behavioural** finding - (the code does the wrong thing; a gate cannot fail) is fixed and re-verified - in a *new* verifier context. A **description or mapping** finding (the spec, - a comment, or EVIDENCE says something untrue about code that is correct) is - fixed and disclosed, and does **not** buy another round. Without this split, - "fix every finding" times "re-verify after every change" is a loop that ends - only when a round returns the empty set — and prose has no such fixpoint. - The trade is real: grading buys termination by giving up completeness, and a - behavioural gap can survive inside a round you chose not to run. -- **Cap the rounds.** Two by default; more needs explicit human approval. The - cap does not stop the spending, it makes the spending someone's decision. -- **Four states in EVIDENCE**: `passed` finalizes; `failed` and `blocked` - (verification could not be completed) do not; `not performed` finalizes only - as a declared downgrade, following the same rule as an unapproved spec. On - Tier 3, `not performed` is the default and needs no apology — say so and - claim correspondingly less. +It reduces **task-context** correlation, not model correlation. **It is not a +gauntlet layer** — a layer is a command returning an exit code in seconds; +this is an agent returning prose a human must judge, spending the one resource +this skill otherwise guards. Experimental: the evidence is one case study +(`references/verifier-case-study.md` — for deciding whether to run this, not +for the verifier to read), not a benchmark. + +**The protocol is `references/verifier.md`. Verification has not been performed +until that file has been read in full and executed; missing or unreadable → +`blocked`, never `passed`.** What cannot be traded away: + +- **Fresh context, blind first**, four inputs only — the task contract, the + approved SPEC, an exact source state, the entry point. Never your + conversation. The draft EVIDENCE comes after its own results, not before. +- **It fixes nothing.** A SPEC gap goes to the human, never to the builder to + self-amend. +- **The human grades the findings.** Behavioural findings are fixed and + re-verified in a new context; description and mapping findings are fixed and + disclosed without buying another round. Propose a grade if you like — the + human decides any disputed or material one, and approves stopping at the + cap. Self-grading is the obvious way to make this rule fail open. +- **Cap at two rounds**, more only by explicit approval. The cap does not limit + the spending; it makes the spending someone's decision. +- **Verification is source-state-specific.** A state no verifier saw is + `not performed`, whatever earlier rounds concluded. Fixing a behavioural + finding after the final permitted round therefore ships an unverified state: + record that as a declared downgrade and keep the earlier rounds as history. +- **Four states**: `passed` finalizes; `failed` and `blocked` do not; + `not performed` finalizes only as a declared downgrade, like an unapproved + spec. On Tier 3 it needs no apology — say so and claim less. ## Setup diff --git a/skills/old-coder/references/gauntlet.md b/skills/old-coder/references/gauntlet.md index aea70a2..72abd77 100644 --- a/skills/old-coder/references/gauntlet.md +++ b/skills/old-coder/references/gauntlet.md @@ -197,7 +197,9 @@ scenario so the evidence report's spec→test mapping is mechanical. - Toolchain: - Entry point: - Independent verification: - (Tier 3; protocol and full template in `verifier.md`) + **against the final source state** — a state no verifier saw is + `not performed` however many rounds preceded it (Tier 3; protocol in + `verifier.md`) ### Spec → Test mapping Status is one of: **pass / fail / unverified / n-a**. A row mapped to @@ -224,7 +226,9 @@ Status is one of: **pass / fail / unverified / n-a**. A row mapped to ### Independent verification (never omit; see verifier.md) - Verifier: ; fresh context; which inputs it received; what correlation that breaks and what it does not. -- Rounds: (cap ); verdict per round. +- Rounds: (cap ); verdict per round, each against the state it saw. +- Grading: who classified each finding behavioural vs description, and who + approved stopping. - Attacked: . - Findings: behavioural (fixed, then re-verified in a new context) vs description/mapping (fixed and disclosed, no new round). diff --git a/skills/old-coder/references/verifier-case-study.md b/skills/old-coder/references/verifier-case-study.md new file mode 100644 index 0000000..1aab97f --- /dev/null +++ b/skills/old-coder/references/verifier-case-study.md @@ -0,0 +1,36 @@ +# Case study: six rounds against an already-green gauntlet + +**Do not load this while running the protocol.** It names the defect classes +one codebase turned out to have, and an attacker primed with that list looks +there first and elsewhere second. It is here for someone deciding *whether* +to run verification and what it costs — not for the verifier. + +Six rounds against a 99-line Python rate limiter that was already passing ten +gauntlet layers, 100% branch coverage and 8/8 mutation, with a +multiply-rebound evidence report. Same model as the builder throughout, so +this measures reproducibility, not model independence. Roughly 550k tokens. + +- **Rounds 1–3 found five behavioural defects** nothing in the gauntlet could + reach: an unbounded key map usable as a remote memory-exhaustion attack + against the component meant to prevent one; `limit=NaN` producing a limiter + that always allowed; 2× over-allow under threads; a lock that covered + check-and-append but not the clock read; and — the most transferable one — + a mutation runner reporting kills for mutants it never executed, because + two same-size mutants written in the same second shared a bytecode cache. + That last defect could only ever inflate the score, so it could never + surface as a red gauntlet. +- **Rounds 4–6 found one behavioural gap and a stream of prose inaccuracies**, + two of which were introduced by the round that fixed the previous one. That + is why a single clean round does not mean converged, and why the grading + rule above exists. The marginal round was clearly negative by round 5. +- **An A/B design failed.** Planting a defect in one copy and verifying a + clean copy as a false-positive control did not work: the "clean" copy was + not clean — it independently invented the planted mutation and correctly + reported it. No false-positive rate could be measured. The two false + positives that did occur were both caused by feeding the verifier a + subdirectory instead of the repository, and a tree polluted by an editable + install. **Verifier noise tracked input quality.** +- **Verification's late-stage output is not bugs.** It is the discovery that + SPEC and EVIDENCE are describing code that does something else — which + matters precisely because those two documents are the only things the human + reads. diff --git a/skills/old-coder/references/verifier.md b/skills/old-coder/references/verifier.md index 57ddc9e..024e5bb 100644 --- a/skills/old-coder/references/verifier.md +++ b/skills/old-coder/references/verifier.md @@ -9,9 +9,9 @@ command returning an exit code; this is an agent returning prose that a human has to grade. It exists because the gauntlet can only check what the spec says — the gauntlet is not what is in question. -## Inputs — exactly four +## Blind-phase inputs — exactly four -Give the verifier: +Give the verifier, before it sees anything else: 1. **The task contract.** The user's original request *plus every requirement, scope change and spec revision a human has explicitly approved since*. Not @@ -44,8 +44,10 @@ builder's framing and its fresh context is wasted. Record what was tried at each surface, including the attacks that found nothing. The attack list is the deliverable; findings are a bonus. -1. **The run.** Execute the entry point from the stated source state. Numbers - that disagree with the draft EVIDENCE mean the draft is wrong, not the run. +1. **The run.** Execute the entry point from the stated source state and + record the result blind. Once the draft EVIDENCE is revealed, any mismatch + suspends its claim until source state, environment, freshness and + determinism have been reconciled — do not silently prefer either number. First confirm the environment actually tests the tree it claims to — a copied virtualenv, a stale install, or a cached artifact can silently exercise the original sources and make every later result meaningless. @@ -95,6 +97,15 @@ builder to write a test that asserts non-behavior. | **Behavioural**: the code does the wrong thing, or a gate cannot fail | fix, then re-verify in a **new** verifier context | | **Description / mapping**: the spec, a comment or EVIDENCE says something untrue about code that is correct | fix and disclose; **no new round** | +**The human grades, not the builder.** The builder may propose a grade; the +human decides any material or disputed one and approves stopping at the cap. +Left to self-grading this rule fails open in the obvious way — call a boundary +defect a documentation defect and the round is avoided. It matters most when +the finding touches the SPEC, where the question is precisely whether the +document is wrong about correct code, or whether it has exposed a behavioural +requirement nobody wrote down. That is the human's call by the same rule that +sends SPEC gaps to the human in the first place. + Without this split, "fix every finding" times "start a new verifier after any change" is a loop that terminates only when a round returns the empty set. Prose has no such fixpoint. @@ -110,6 +121,25 @@ Cap at two rounds by default. More needs explicit human approval, recorded. The cap does not stop the spending; it makes the spending someone's decision, which is the part that was missing when this protocol was first drafted. +## Verification is source-state-specific + +A verdict attaches to the state that was verified, not to the project. A state +no verifier has seen is `not performed`, however many rounds preceded it and +whatever they concluded. + +This bites at exactly one place: a behavioural finding fixed after the final +permitted round. The fix is correct and the round cap is correct, and the +shipped state is still unverified. Do not launder that by inheriting the +previous verdict, and do not invent a fifth state for it. Record the final +state as `not performed` — a declared downgrade — and keep the earlier rounds +as history: + +```text +Independent verification: not performed against final source state . + earlier rounds were performed; the last verified state returned +, and the fixes made since are disclosed below as unverified. +``` + ## Four states, recorded in EVIDENCE | State | May EVIDENCE be finalized? | @@ -139,35 +169,3 @@ last verified state, say which — they are not independently verified. - Canary: - Fixed after the last verified state, therefore unverified: ``` - -## What one case study showed - -Six rounds against a 99-line Python rate limiter that was already passing ten -gauntlet layers, 100% branch coverage and 8/8 mutation, with a -multiply-rebound evidence report. Same model as the builder throughout, so -this measures reproducibility, not model independence. Roughly 550k tokens. - -- **Rounds 1–3 found five behavioural defects** nothing in the gauntlet could - reach: an unbounded key map usable as a remote memory-exhaustion attack - against the component meant to prevent one; `limit=NaN` producing a limiter - that always allowed; 2× over-allow under threads; a lock that covered - check-and-append but not the clock read; and — the most transferable one — - a mutation runner reporting kills for mutants it never executed, because - two same-size mutants written in the same second shared a bytecode cache. - That last defect could only ever inflate the score, so it could never - surface as a red gauntlet. -- **Rounds 4–6 found one behavioural gap and a stream of prose inaccuracies**, - two of which were introduced by the round that fixed the previous one. That - is why a single clean round does not mean converged, and why the grading - rule above exists. The marginal round was clearly negative by round 5. -- **An A/B design failed.** Planting a defect in one copy and verifying a - clean copy as a false-positive control did not work: the "clean" copy was - not clean — it independently invented the planted mutation and correctly - reported it. No false-positive rate could be measured. The two false - positives that did occur were both caused by feeding the verifier a - subdirectory instead of the repository, and a tree polluted by an editable - install. **Verifier noise tracked input quality.** -- **Verification's late-stage output is not bugs.** It is the discovery that - SPEC and EVIDENCE are describing code that does something else — which - matters precisely because those two documents are the only things the human - reads. From f92459383a83a80ef0b9a551d586d6337283af90 Mon Sep 17 00:00:00 2001 From: "Li, Amazing Ang" Date: Mon, 10 Aug 2026 18:28:51 +0800 Subject: [PATCH 2/3] docs: fix a reference left dangling by moving the case study MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The grading section pointed at 'the case study below' for its evidence that skipping a round can hide a behavioural gap. The case study is now its own file, so the pointer went nowhere — the same class of stale cross-reference the verifier rounds kept finding in this project. Co-Authored-By: Claude Opus 5 (1M context) --- skills/old-coder/references/verifier.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/skills/old-coder/references/verifier.md b/skills/old-coder/references/verifier.md index 024e5bb..1c2781e 100644 --- a/skills/old-coder/references/verifier.md +++ b/skills/old-coder/references/verifier.md @@ -111,11 +111,11 @@ change" is a loop that terminates only when a round returns the empty set. Prose has no such fixpoint. **Be clear about the trade.** Grading buys termination by giving up -completeness. A behavioural gap can live inside a round you chose not to run — -in the case study below, the round that would have been skipped under this -rule is the one that found an unpinned threshold magnitude. That is the price, -and it is worth paying, because the alternative is a process with no stopping -condition at all. Say in EVIDENCE which rounds were not run. +completeness. A behavioural gap can live inside a round you chose not to run, +and that is not hypothetical — it has happened at least once, in the run +written up in `verifier-case-study.md`. The price is worth paying because the +alternative is a process with no stopping condition at all. Say in EVIDENCE +which rounds were not run. Cap at two rounds by default. More needs explicit human approval, recorded. The cap does not stop the spending; it makes the spending someone's decision, From de5afeeb83268bf2a342702e11e3d8fb30601797 Mon Sep 17 00:00:00 2001 From: "Li, Amazing Ang" Date: Mon, 10 Aug 2026 18:47:09 +0800 Subject: [PATCH 3/3] skill: verifier.md still carried the conclusion the rest of the PR overturned MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Its opening said "the gauntlet can only check what the spec says — the gauntlet is not what is in question", which SKILL.md had already been changed away from and which the protocol's own attack order contradicts: it goes after the run, the checkers and the mapping, and in the case study behind all of this it was the checkers that turned out to be unsound. The gauntlet is necessary but not self-authenticating, and the verifier attacks all four surfaces — incomplete spec, unsound checker, overclaiming mapping, and EVIDENCE that does not describe the state that shipped. Three smaller corrections: - "Human spec approval covers only the last" claimed too much. Approval does not make a spec complete; it breaks author correlation, and only before code exists. Said that way instead. - "A layer is a command returning an exit code in seconds" is not the real distinction — mutation and fuzzing runs take minutes too. A layer is an executable check with a machine-evaluable result; this returns prose a human must judge. That is the difference that matters. - Readers could reasonably ask whether the protocol is itself a fifth input to a process that permits exactly four. It is instruction, not task evidence: the limit applies to task-specific inputs. The verifier is expected to know how to attack; it is not expected to know anything about this task that the four items do not carry. The case study is named alongside the builder's conversation and the draft EVIDENCE as something to withhold. Co-Authored-By: Claude Opus 5 (1M context) --- skills/old-coder/SKILL.md | 9 +++++---- skills/old-coder/references/verifier.md | 19 +++++++++++++------ 2 files changed, 18 insertions(+), 10 deletions(-) diff --git a/skills/old-coder/SKILL.md b/skills/old-coder/SKILL.md index 3489720..966fc6e 100644 --- a/skills/old-coder/SKILL.md +++ b/skills/old-coder/SKILL.md @@ -232,14 +232,15 @@ Scale effort to blast radius, and say which tier you chose: The gauntlet is evidence, not self-authentication: its checkers can be unsound, its mappings can overclaim, and the spec can be incomplete. Human -spec approval covers only the last, and only before any code exists. +spec approval mitigates only the last, by breaking author correlation, and +only before code exists — it does not make a spec complete. Independent verification answers the rest where the stakes justify it: a fresh-context agent that attacks the finished work before EVIDENCE is signed. It reduces **task-context** correlation, not model correlation. **It is not a -gauntlet layer** — a layer is a command returning an exit code in seconds; -this is an agent returning prose a human must judge, spending the one resource -this skill otherwise guards. Experimental: the evidence is one case study +gauntlet layer** — a layer is an executable check with a machine-evaluable +result; this is an agent returning prose a human must judge, spending the one +resource this skill otherwise guards. Experimental: the evidence is one case study (`references/verifier-case-study.md` — for deciding whether to run this, not for the verifier to read), not a benchmark. diff --git a/skills/old-coder/references/verifier.md b/skills/old-coder/references/verifier.md index 1c2781e..2f033c0 100644 --- a/skills/old-coder/references/verifier.md +++ b/skills/old-coder/references/verifier.md @@ -4,10 +4,12 @@ The protocol for the "Independent verification" section of SKILL.md. Read it in full before claiming verification was performed; the summary in SKILL.md is not the protocol. -This is not a gauntlet layer and should not be run like one. Every layer is a -command returning an exit code; this is an agent returning prose that a human -has to grade. It exists because the gauntlet can only check what the spec -says — the gauntlet is not what is in question. +This is not a gauntlet layer and should not be run like one. A layer is an +executable check with a machine-evaluable result; this is an agent returning +prose a human has to grade. It exists because the gauntlet is necessary but +not self-authenticating: the spec may be incomplete, a checker may be unsound, +a mapping may overclaim, and EVIDENCE may not describe the state that shipped. +The attack order below goes after all four. ## Blind-phase inputs — exactly four @@ -24,8 +26,13 @@ Give the verifier, before it sees anything else: when git is absent). 4. **The gauntlet entry point.** -Withhold the builder's conversation and the draft EVIDENCE. If a claim needs -the builder's justification to stand, it is not proven. +This protocol is instruction, not task evidence; the four-item limit applies +to task-specific inputs. The verifier is expected to know how to attack — it +is not expected to know anything about this task that the four items do not +carry. + +Withhold the builder's conversation, the draft EVIDENCE, and the case study. +If a claim needs the builder's justification to stand, it is not proven. The verifier reads the implementation freely — it is an attacker, not the human whose review you are trying to make optional.