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..966fc6e 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,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 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..2f033c0 100644 --- a/skills/old-coder/references/verifier.md +++ b/skills/old-coder/references/verifier.md @@ -4,14 +4,16 @@ 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. -## 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 @@ -24,8 +26,13 @@ Give the verifier: 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. @@ -44,8 +51,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,21 +104,49 @@ 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. **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, 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 +176,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.