Verification is source-state-specific, and the human grades the findings - #5
Merged
Conversation
…ndings 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) <noreply@anthropic.com>
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) <noreply@anthropic.com>
…erturned 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) <noreply@anthropic.com>
This was referenced Aug 12, 2026
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.
Follow-up to #4, from review. Four fixes, 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. The protocol's own four states forbid exactly that.The fix is neither a seventh round nor 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 — recorded as a declared downgrade, with the earlier rounds kept as history rather than as a certificate. The demo's report now says so in its first lines.Who grades the findings
"Behavioural findings buy a round, description findings do not" was left to whoever holds the pen — the builder, who has an obvious incentive to call a boundary defect a documentation defect and skip the round. 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 precisely whether the document is wrong about correct code, or whether it has exposed a behavioural requirement nobody wrote down. That is already the human's call under the rule that sends SPEC gaps to the human.
Two accuracy fixes
Over-claiming for the gauntlet
The text said the gauntlet "proves the code satisfies every constraint the spec expresses" and "is not what is in question here" — while the case study behind this whole line of work shows a coverage layer that could not fail, a mutation runner executing the wrong bytecode, and a checker guarding a spelling rather than a behaviour. The gauntlet is evidence, not self-authentication: its checkers can be unsound, its mappings can overclaim, and the spec can be incomplete.
Also
The case study moved to
references/verifier-case-study.mdand 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 — the protocol should not hand the verifier its answers.SKILL.md's verification section is down from 57 lines to 39.
🤖 Generated with Claude Code