Independent verification: what six fresh-context rounds found in a gauntlet that was already green - #4
Merged
Merged
Conversation
Two fresh-context verification passes attacked the demo at 9540d72 while the full gauntlet was green. They converged on three MATERIAL defects that 10 layers, 100% branch coverage and 8/8 mutants could not reach, plus a fail-open layer inside the gauntlet itself. Spec-level (approved as REVISION 4): - limit=NaN/inf/2.5/bool were accepted and produced a limiter that allows forever — the exact fail-open class fixed for window_seconds in the 2026-07-25 revision, never swept to the sibling parameter. - allow() accepted None/int/bytes/"" as keys, so a missing HTTP header silently became one shared quota bucket for every unidentified caller. - Key eviction was lazy: keys that never returned were never reaped, so distinct callers grew the map without bound (200k keys, 171 MB measured). Memory is now bounded by the keys seen within one window. - allow() was a non-atomic read-prune-check-append; 2x over-allow was measured under threads. Now guarded by a lock, and the autonomous "single-threaded use only" de-scoping is withdrawn. Gauntlet-level: - Coverage was report-only: dropping to 89% still exited 0. Now gated with --cov-fail-under=100. - The no-real-time scan matched `time.` and missed `from time import sleep`. Pattern now covers usage forms; fixed in the pattern, not by excluding files. - Property strategies saw three distinct keys, so a key-hardcoded implementation would have scored 100%/8-of-8. Widened, then re-tuned after layer attribution showed over-widening had blunted the layer (M5 survived the property suite). - Mutants M9/M10/M12/M13 added, one per failure-model row that was claiming coverage it did not have. M11 (prune one per call) was proposed by verification as a surviving mutant proving quota loss. It is EQUIVALENT — 0 divergences over 200k randomized monotone sequences — and is documented as such rather than killed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…harness that reported kills it never executed The round-2 verifier found the mutation layer itself was fail-open. CPython validates a cached .pyc against (source mtime in whole seconds, source size); M4 and M5 are both exactly one byte shorter than the original and adjacent, so M5 -- the fail-open mutant -- could run M4's bytecode and be reported KILLED without executing. Reproduced directly: clean cache gives True/True, M4-then-M5 in one second gives True/False. The bias is always toward inflating the kill count, so it can never surface as a red gauntlet. - mutants.py clears __pycache__, runs pytest with PYTHONDONTWRITEBYTECODE, and hard-fails if a cache reappears. New --negative-control runs a killer and a strictly-equivalent mutant of identical size under one pinned mtime; it is a gauntlet gate, and it was proven non-vacuous by removing the cache defence and watching the equivalent mutant be misreported as KILLED. - The first negative control was itself vacuous: it waited for two writes to land in the same second instead of pinning the mtime, and passed with the defence removed. Its C2 was also not strictly equivalent (the sweep throttle differs at now - last_sweep == window, which the memory bound now contracts). Historical check, stated precisely: on 9540d72 the runner was structurally vulnerable and exactly one adjacent pair could collide (M4/M5, both 1675 bytes). Re-derived under a sound procedure, all 8 historical mutants are genuinely killed, M5 included. The published 8/8 is therefore correct in outcome even though the procedure that produced it was unsound; whether that archived run took the collision path cannot be determined, and does not change the number. Other round-2 findings: - window_seconds had no type guard: True built a 1.0s window, "60" raised a bare TypeError. Validation extracted to _validate() so the constructor stays inside the complexity budget. - Nothing pinned key identity: every key in the suite was lowercase, so key.lower() survived everything. Scenario + M14. - P2's key strategy was left on sampled_from("abc") directly beneath the comment explaining why that was too narrow; the target key is now taken from the data instead of hardcoded, so the property cannot hold vacuously. - The under-allowing row cited M6 (which over-allows) and M8 (claimed by the memory row); it now cites the mutant its scenario actually kills. - Secret scan now covers .github, spec.md and the dependency files. - The no-real-time claim is downgraded to what a regex can enforce, and the concurrency tests' deadlock-guard timeouts are declared as an exception rather than excluded from the scan. - Clock finiteness and the cardinal (vs temporal) memory residual are recorded as accepted caller obligations. - Concurrency: a deterministic fault-injection atomicity test now kills M13 5/5; the threaded stress test goes to 400 rounds (measured 5.9% per-round detection; at 60 rounds the mutant survived 1 run in 50) and corroborates rather than carries the row. - __pycache__ is cleared at gauntlet start; the scans were grepping bytecode. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Round 3 found that REVISION 4's own concurrency fix was incomplete: the lock covered check-and-append but `now = self._clock()` sat outside it. Two callers can therefore commit in the opposite order from which they read the clock, leaving the deque unsorted. _prune breaks fail-closed; _sweep breaks fail-open — it judges a key by a stale newest-hit and forgets one that still has a live hit, resetting that caller's quota. Reproduced: limit=2 window=60 with hits [100.0, 99.0] allows 3 requests inside one window, violating P1 and approved contract item (d). The mutant that IS the fix (M16, read the clock outside the lock) survived the entire suite before this change: both existing concurrency tests hold time constant, so no test could distinguish the two lock placements. The new test gates the clock itself to force two callers to read different values, and asserts the recorded hits stay ascending. Cost recorded in the clock contract: `clock` must not call back into the same limiter, which would now deadlock. Other round-3 findings: - The 4b clock contract claimed a NaN-poisoned key would eventually be swept. It cannot — _sweep uses the same comparison. The key is immortal and its caller denied forever, which falsifies the temporal memory bound for that path; both sentences corrected rather than softened. - Key normalisation coverage was case-folding only; key.strip() survived, helped by a P2 pool containing "c " but not "c". Padding and whitespace-only keys are now pinned, pool fixed, M17 added. - _sweep's expiry boundary was unpinned while _prune's was; the surviving mutant was fail-open (forgets a key with a live hit). Scenario + M18. - Secret scan missed "-----BEGIN RSA PRIVATE KEY-----" (space separator). - source_state.sh did not hash .github/workflows, so evidence could rebind to a tree whose CI config had silently changed. - _prune's docstring still described key-forgetting it no longer does. - The negative control validates the two cache defences as a conjunction, not individually; the comment now states the asymmetry instead of "both needed". Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Round 4 returned VERDICT passed with no MATERIAL finding: the core semantics
survived a 180k-op differential fuzz (0 divergences) and 17 fresh mutants, and
every home-grown gate was fed known-bad input and failed closed — including
the negative control's specific non-vacuity claim, which reproduced stepwise
exactly as documented.
Its four MINOR findings were accuracy defects, and two of them had real teeth:
- The memory bound was documented as one window in both the class docstring
and the Must NOT. It is two: the sweep is throttled to once per window, so a
key can sit idle for just under 2W. Only the residual-risk section had it
right, and the idle-keys test probed at exactly 2W so it passed under either
reading and pinned neither. New test pins both sides.
- A backward clock jump suspended the sweep entirely: the throttle compared
now against a _last_sweep it could no longer reach. Measured 20,001 keys
retained across seven windows of monotone time. The docstring's "a backward
jumping clock fails closed" was true of quota and false of memory. Fixed in
code rather than documented away: the throttle is now two-sided, so a
negative delta re-arms it at the new time. M20 pins it.
- The sweep throttle was an asserted design property with no catcher —
deleting its bookkeeping left the suite green while turning every request
into an O(distinct keys) scan. Test + M19.
- Declared exception (h) named one wall-clock dependence; there are two, and
they fail in opposite directions. The 0.3s wait in the clock-ordering test
is not a deadlock guard: on healthy code it always times out, and its
spurious direction is a false PASS — a surviving fail-open mutant. Measured
margin ~470x, so accepted, but now described accurately.
- The NaN-clock paragraph described the never-expiring hit as the whole mode;
NaN also destroys the sweep throttle permanently.
- P2's comment claimed an attribution the measurement contradicts.
The must-not time scan matched `time.` inside ordinary prose ("sweep time.
After"); narrowed to attribute access, in the pattern rather than by excluding
files, and verified to still catch real `time.sleep`.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…w false claim Round 5 found no behavioural defect and every executable layer fail-closed on demand, but failed the project's own accuracy standard with one MATERIAL: The 4d clock-contract paragraph claimed a NaN reading "destroys the sweep throttle permanently ... an O(distinct keys) scan on every request for the life of the process". False. _sweep unconditionally re-anchors _last_sweep after its early return, so the next finite reading heals the throttle. Measured: nan, then 100.0 at t=100, still 100.0 at t=101/102/110. The true cost of one NaN reading is one extra sweep. This was written by the revision that fixed the previous inaccuracy in the same paragraph, which is the point worth recording: a fix round can introduce a fresh MATERIAL of the same class. Also fixed: - The memory bound omitted its load-bearing qualifier. Sweeping happens only inside allow(), so while traffic is silent nothing is reclaimed at all: 1000 keys survive ~166,000 idle windows and drop only on the next request. The bound is "keys seen in the two windows preceding the most recent request". Now pinned by a test across an idle gap, not just asserted. - The sweep throttle's own boundary was the last age comparison in the file with no test behind it (_prune's had M2, _sweep's had M18). tools/mutants.py had even noted the gap in passing and used it to justify a different control rather than closing it. Test + M21. - The -inf sentinel had the same shape: every clock in the suite starts at 0.0 or beyond a window, so replacing it with 0.0 was invisible. Test + M22. - mutants.py had the two cache defences backwards. Measured three ways: removing the rmtree alone leaves the control green; removing PYTHONDONTWRITEBYTECODE alone trips the tripwire; only removing both plus the tripwire reproduces the misreport. DONTWRITEBYTECODE closes the leak. - mutants.py claimed --negative-control was exercised by test_gauntlet_checks.sh; it is not — that script covers must_not_match only. A false cross-reference inside the layer meant to prove the mutation ran. - Five tests existed only as prose while the test module claims a 1:1 map to spec scenarios; scenarios added. Two demonstrated failure modes from 4d had a test and a mutant but no failure-model row; rows added. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…here Round 6 found no fail-open and no surviving mutant that changes an allow/deny outcome, but two findings had teeth: - _sweep's idle threshold had its BOUNDARY pinned (M18 kills >=) and its MAGNITUDE unpinned: `> window * 1.5`, and even `* 1.99`, left 40 tests, 100% coverage and 21/21 mutants green while inflating the human-approved two-window retention bound by up to 50%. Every memory test asserted deletion only at age >= 2W, so any threshold in (W, 2W) satisfied all of them. The twin function's magnitude WAS pinned; this one was not. Test + M23. - test_clock_is_read_inside_the_critical_section asserted only that the deque was sorted. A one-element list is trivially sorted, so a second caller that died satisfied it vacuously — demonstrated with a double-clock-read mutant that raised out of the gated clock while the test still reported 1 passed. It now asserts both callers committed. Prose corrections, all mine: - "worst-case retention is just under 2W" is false; 2W is attained, and the sweep that drops a key runs strictly later than 2W after its last hit. - The stress test's per-round detection rate was quoted as 5.9%. Re-measured against the real source mutant rather than a Python replica: 3.7% here, so the 400-round miss probability is ~3e-7, not 3e-11. Now marked machine-dependent. - The negative control's comment said its mutants are "each one byte shorter than the original" and, nine lines later, "length-preserving". The second is true; the first describes M4/M5. - The time-scan comment justified its pattern partly with an invented claim (that a word-boundary pattern would fire on test_non_monotonic_clock_*, a name containing no "time"). - The test module claimed a 1:1 test-to-scenario map; it is 24 tests to 22 scenarios, the rest mapping to a Must NOT or a failure-model row. - The silent-traffic measurement quotes 1000 keys where the scenario uses 50. Six rounds of fresh-context verification stop here. Rounds 1-3 found five behavioural defects; rounds 4-6 found one behavioural gap and a steady stream of prose inaccuracies, two of which were introduced by the round that fixed the previous one. Remaining known items are disclosed in evidence.md rather than chased, because a rule of "fix every finding, then re-verify" only terminates when a round returns the empty set, and prose has no such fixpoint. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Numbers from one fresh run at commit 66df5cd / tree 402ed5f682f8543f: 41 tests, 100% branch coverage (gated), 22/22 mutants with the harness negative control green, all layers clean. Records what the six fresh-context rounds cost and produced, that the A/B design failed, that verification was stopped deliberately rather than run to a fixpoint, and which post-round-6 fixes are therefore unverified. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
spec.md had grown to 339 lines against a 99-line implementation, most of it forensics: what an earlier revision claimed, which mutant a row used to cite, what a verification round measured. That material is real but it belongs in evidence.md's honest notes and in git, not in the one artifact a human is supposed to read before any code exists. The contract is unchanged — same scenarios, same invariants, same Must NOTs, same clock obligations, same residual risk, same failure-model rows and the same falsification procedures. What is gone is the archaeology; a short revision-history section points at where it lives. 339 -> 255 lines. Comments in the tests and tooling got the same treatment: the reason a value or a pattern is what it is stays, the account of what a previous revision got wrong goes. Gauntlet green after the prune: 41 tests, 100% branch coverage, negative control ok, 22/22 mutants. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Same numbers (41 tests, 100% gated coverage, 22/22 mutants, control green); new source state, plus a note that the spec was pruned to a contract and where the forensics went. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
VERIFY — a fresh-context adversarial pass before EVIDENCE is finalized,
Tier 3, marked experimental. 40 lines in SKILL.md carrying only the
non-negotiables; the protocol lives in references/verifier.md behind a hard
gate ("not performed until that file has been read in full"), so Tier 1/2
never load it.
The rule that distinguishes this from the version I would have written before
running it: grade the findings. A behavioural finding is fixed and re-verified
in a new context; a description-or-mapping finding is fixed and disclosed and
does NOT buy another round. Without the split, "fix every finding" times
"re-verify after any change" only terminates when a round returns the empty
set, and prose has no such fixpoint. Rounds are capped at two by default.
references/verifier.md carries the four inputs (including the task contract:
the request PLUS every human-approved change since, or legitimate scope
revisions read as spec gaps), blind-first, the attack order, the
prove-divergence-before-reporting-a-survivor rule, the four states, the report
template, and what one case study actually showed — including that its A/B
design failed and that its late rounds were negative value.
Two rules from the same experiment that belong to GAUNTLET, not VERIFY:
- A coverage layer must exit nonzero when its threshold is missed. This repo's
own coverage layer printed a percentage and exited 0; dropping to 89% left
the gauntlet green. A layer that cannot fail is a report.
- A negative control proves one known-bad case reaches the checker's failure
path. It does not prove the checker recognises every violation of the rule
it serves — a grep gate can fail closed perfectly and still guard a spelling
rather than a behaviour. And a negative control must itself be shown
non-vacuous by removing the defence it validates: the first one written here
passed with the defence removed.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
It was numbered step 6, between GAUNTLET and EVIDENCE, which put it alongside RED/GREEN/GAUNTLET and implied it is the same kind of thing. It is not. Every gauntlet layer is a command that returns an exit code in seconds; this is an agent that takes minutes and returns prose a human has to grade — findings to classify, equivalent mutants to rule out, false positives to dismiss. Framing it as a stage promised a fit the form does not have, and it quietly spent the one resource this skill otherwise guards: human attention. Now a Tier 3 assurance option after Calibration, with the loop back to its six stages. Content unchanged; position and self-description are not. Two things the earlier framing left unsaid and now says: - The gauntlet is not what is in question. It proves the code satisfies every constraint the spec expresses and does that well. Verification exists because the SPEC can be incomplete and EVIDENCE can describe code that does something else — not because the layers are inadequate. Without that line, "you also need another agent" reads as a retreat from the skill's own claim that constraints replace inspection. - Grading findings buys termination by giving up completeness, and the case study proves it: the round that this rule would have skipped is the round that found an unpinned threshold magnitude. The cap is likewise not a spending limit — it converts silent spending into someone's decision, which is exactly what was missing when six rounds ran unchecked. On Tier 3, `not performed` is now stated as the default that needs no apology. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The prune of spec.md (339 -> 255 lines, 8b88bda) came after the last verified state and was not listed alongside the other post-round-6 changes. No clause changed, but it is a large edit to the document a verifier attacks hardest, and omitting it is the same accuracy defect six rounds kept finding. Also notes why the cited commit is not HEAD: later commits touch only skills/, which is outside the hashed tree, so the binding is current rather than stale. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The demo was passing ten gauntlet layers, 100% branch coverage and 8/8 mutation, with an evidence report that had been rebound several times. A fresh-context agent — given only the task contract, the approved SPEC, the repo at a commit, and the entry point, and never the builder's reasoning — was asked to attack it. Six rounds later, this is the result.
What it found that the gauntlet could not
Five behavioural defects in the first three rounds:
limit=NaN/infproducing a limiter that always allows.spec.mdcalls this exact class a security bug, and the 2026-07-25 revision fixed it — forwindow_secondsonly. The sibling parameter was never swept..pycon (mtime in whole seconds, source size); M4 and M5 are both one byte shorter than the original and adjacent in the list, so M5 — the fail-open mutant — ran M4's bytecode. The bias is always toward inflating the score, so it could never surface as a red gauntlet.Historical note, stated precisely: re-derived under a sound procedure, all 8 historical mutants are genuinely killed. The published 8/8 is correct in outcome even though the procedure that produced it was unsound.
Rounds 4–6 found one more behavioural gap (a threshold whose boundary was pinned and whose magnitude was not) and a steady stream of inaccuracies in the prose — two of which were introduced by the round that fixed the previous one.
Skill changes
references/verifier.mdso Tier 1/2 never pay for it.The rule that matters most in that protocol: grade the findings. Behavioural findings are fixed and re-verified in a new context; description and mapping findings are fixed and disclosed and do not buy another round. Without that split, "fix every finding" times "re-verify after every change" only terminates when a round returns the empty set, and prose has no such fixpoint. The trade is real and is stated in the text: grading buys termination by giving up completeness.
Honest cost
Roughly 550k tokens across six rounds. Rounds 1–3 produced every rule that made it into the skill; rounds 4–6 produced one behavioural gap and a lot of wording. The marginal round was clearly negative by round 5.
The A/B design this started as failed: the "clean" control arm independently invented the defect planted in the other arm and correctly reported it, so no false-positive rate could be measured. This is an exploratory case study, not a benchmark, and
references/verifier.mdsays so. All six rounds ran on the same model as the builder, so convergence shows the findings are reproducible, not independent of model bias.Notes for review
CI has never run on this branch — the workflow triggers only on
push: mainandpull_request, so every green result so far is local macOS / Python 3.14. This PR is the first cross-environment check against ubuntu / Python 3.12.This includes real behavioural changes to the demo library:
allow(None)andallow(12345)now raise,window_seconds=Trueis rejected, andallow()takes a lock.🤖 Generated with Claude Code