Verification is source-state-specific, and the human grades the findings

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;

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,43 @@ 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 mitigates only the last, by breaking author correlation, and
+only before code exists — it does not make a spec complete.
 
-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 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.
+
+**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
 

skills/old-coder/references/gauntlet.md

@@ -197,7 +197,9 @@ scenario so the evidence report's spec→test mapping is mechanical.
 - Toolchain: <pinned versions file, e.g. requirements-dev.txt>
 - Entry point: <single command that reruns every layer>
 - Independent verification: <not performed | passed | failed | blocked>
-  (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: <host / model family>; fresh context; which inputs it received;
   what correlation that breaks and what it does not.
-- Rounds: <n> (cap <m>); verdict per round.
+- Rounds: <n> (cap <m>); verdict per round, each against the state it saw.
+- Grading: who classified each finding behavioural vs description, and who
+  approved stopping.
 - Attacked: <what was tried, not only what was found>.
 - Findings: behavioural (fixed, then re-verified in a new context) vs
   description/mapping (fixed and disclosed, no new round).

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.