Skip to content

tooling(claude): resource-bounded self-verification and adversarial R-15 invariant reviews #1034

Open

Description

@qnbs

Claude Code self-verification — bounded implementation owner

Disposition (2026-10-13): NEW, PLANNED, SOURCE NOT ADMITTED. Requested explicitly by the maintainer to implement a practical, low-cost, self-verifying Claude Code CLI workflow as soon as the active security stack permits. This is not an extra merge authority or mandatory CI gate. Relationship: #780 (review-convergence policy parent), #931 (provider-neutral exact-head reviewer aggregation), #550 (cost/latency), #764 (Stryker tooling), #922/#359 (R-15 semantic authority), #926 (v1.30 release), Linear QNB-194 (existing agentic correction/perfection owner), QNB-183 (test-evidence architecture). Do not recreate anti-cascade governance cancelled in QNB-194.

Problem and observed need

Codex on PR #1033 identified material faults that green deterministic CI did not catch: the public raw commit_root bypass of exclusive admission; a phase-transition publisher accepting bootstrap revision zero without a predecessor; and P2-B whereby prepared phase-changing root recovery completes under shared admission after step-F failure. Earlier CodeAnt found an alias TOCTOU. These are multi-module, crash/recovery and alternate-publisher counterexamples, not lint issues. The latter was empirically reproduced on head 8017776b, tracked as VALID/DEFERRED/MUST-FIX in #359 comment 6151082206. E2c is being addressed in separately admitted PR #1035 (scope evidence: GH #359 comment 6151692274); it is not a #1034 implementation and was still unmerged at the last checked snapshot. This issue may not change #1035 scope, waive #1033's P2-B, or merge either PR.

Outcome

Equip the existing local Claude Code CLI writer (VS Code, Ubuntu 24.04, constrained disk/CPU) with a small, opt-in, reproducible verification loop:
contract/acceptance -> invariants -> falsifiable counterexamples -> targeted negative/regression tests -> read-only independent subagent -> signed commit/prepush -> exact-head hosted CI/Codex -> finding disposition.
The verifier is a test/review assistant, not an oracle. Model testimony never becomes required merge evidence. Existing policies remain authoritative: AGENTS.md, docs/PR-CI-MERGE-WORKFLOW.md, docs/REVIEWER-GOVERNANCE.md, path-scoped contracts. No main writes, automatic merges, admin bypass, release/cutover authority, PR branch rewrites, Vercel deletion, privileged workflows or additional required statuses.

Phase 0 — NOW, read-only, zero repository mutation (P1)

  1. Inventory .claude/agents/, .claude/skills/, existing Claude hooks/settings, nested CLAUDE.md, CI/prepush and available local disk. Follow existing permission scopes; no installation or edits until a discrete source admission. Use current CLI docs, not guessed hooks API.
  2. Build a bounded blind-review reference corpus from feat(core): publish a journal phase change only under exclusive admission #1033 and optionally feat(core): iterate the inventory and leave CONVERT through the conversion session (#445) #1017/R-15 Gate 4C: journal manifest + paged inventory codec #956/feat(core): serialize every root commit through a cross-process root_commit_mutex (#445) #950. Redact tokens, keys, user data and private artifacts. For every known finding: reviewed HEAD, entrypoint, cross-module call chain, precondition, step before durable write, actual evidence (confirmed vs hypothesis), severity, disposition, and deterministic negative test.
  3. Measure current time/token/runner usage, local CPU/memory/disk overhead and reviewer detection. Compare against a no-agent baseline; do not assert a general 75% reduction from anecdote.
  4. Deliver an agreed threat/verification matrix and specific opt-in implementation slice with prospective PR budget. Historical findings are fixtures, not a claim that a model found a previously unknown bug.

Phase 1 — smallest practical MVP, independent bounded PR (P1; after active E2c security slice is safely handed over/terminal)

Implement only if a maintainer/source admission covers the exact files, behavior and deployment:

  • One project-scoped .claude/agents/r15-invariant-verifier.md with tight YAML frontmatter and a deliberately read-only allowlist (e.g. Read/Grep/Glob, no Bash/network, no Edit/Write/commit/GitHub mutations); verify actual permission behavior in the installed CLI. Noninteractive dontAsk where supported; never bypassPermissions. Be mindful that parent agent permission modes may be inherited: investigate/document this fail-closed.
  • One on-demand .claude/skills/verify-r15/SKILL.md, explicitly manually invoked, no automatic install/run on each edit. Takes PR base/head, scope and 1–3 named safety invariants, reconstructs call sites/alternate API routes and step-wise crash windows; delegates a fresh-context adversarial audit that does not receive the author's rationale. Avoid burning full-context duplicates.
  • A concise, machine-readable-or-Markdown VerificationEvidence template, manual first; no new workflow/check/secret/service. Output: evaluated HEAD, exact contract anchor, invariants, attempted counterexample, path/lines, deterministic reproduction/test and its before/after behavior, coverage boundary, UNKNOWN assumptions, cost, finding disposition and next allowed action. If no proof exists state UNPROVEN.
  • Canonical taxonomy: PUBLIC_API_BYPASS, INTERNAL_TYPESTATE_BYPASS, BOOTSTRAP_PREDECESSOR, ALIAS_TOCTOU, PHASE/OWNERSHIP/FENCE, SHARED_EXCLUSIVE_ADMISSION, C/E1/E2/F_CRASH_WINDOW, REPLAY/RETRY/TAKEOVER, AUTHENTICATED_LOCATOR, BOUNDED_IO, PRESERVE_FIRST, SOURCE_VS_CONTRACT_CLAIM.
  • Source and documentation change budgets strictly obey <=30 files, <=3000 meaningful lines, <=15 signed commits; aim far below, one correction wave, no scope expansion into R-15 production code within the tooling PR.
  • The verifier has no write authority. Only the admitted main writer may add tests/fixes on its own approved feature branch.

Phase 2 — evidence/reproducer quality (P1/P2; own source admission)

  • Pre-/post-fix reproducibility with negative tests; prove they fail on vulnerable behavior and pass after; where a reversible controlled negative baseline is unavailable record that honestly. Avoid executing old vulnerable branches against real data.
  • Differential checks against known historical cases; pass/fail oracle is a checked test / precise static API assertion, not reviewer self-agreement or autogenerated snapshot approval.
  • Ensure a negative test checks zero durable writes at all relevant locations and provider anchor (not only intercepted file reads) when the contract claims no write.
  • Crash matrix for C (anchor prepare), E1 (target slot), E2 (pointer), F (anchor commit), ambiguous outcomes, restart and shared/exclusive admission; strict result classification. Windows-portable tests on existing hosted matrix.
  • Prioritize type-level guarantees (compile-fail/positive doctest) when a claimed property is type-based; use narrow Kani/Loom/fuzz/cargo-mutants experiments only when concrete blind spots warrant them. Do not make optional tools new required prerequisites for R-15 Gate 4/5/v1.30.
  • Preserve independent Codex review on current head; its findings are triaged through all three GitHub comment/review channels with exact SHA, no autoreply/auto-resolve.

Phase 3 — optional integration, explicitly later (P2)

Independent acceptance and qualification

  1. Pre-registered benchmark of >=5 historical issues/PR-deltas, including the three feat(core): publish a journal phase change only under exclusive admission #1033 Codex findings and one deliberately clean or misleading case, plus at least one previously unseen approved R-15 slice. Separate replay/benchmark (known answer) from novel detection.
  2. Each true positive cites a line-level source/call path, falsifiable preconditions and deterministic repro/expected failure; every false positive classified, not silently dropped. Must correctly identify P2-B even though ordinary-data E1 barrier currently reduces exposure; no unsafe claim that source code was fully proven.
  3. No write operations from the verifier in a permission-denial probe, including adverse prompt-injection text in repo comments/fixtures; no key/PII/network exfiltration.
  4. Evidence packet is SHA-bound, repeatable and distinguishes verified facts from hypotheses. Missing test means NOT_PROVEN, not PASS.
  5. Cost/run-time/resource budget reported (tokens, wall time, peak disk/temp churn, optional GitHub minutes, unique validated findings per 100 changed lines); stop at resource threshold; no extra always-on local Rust analyzers; no concurrent heavy local tasks. Scrutinize /tmp scratch cache cleanup by owner and prevent test debris in commits.
  6. External independent exact-head Codex retains its role; no changes to reviewer branch protection, release gates or production authority.
  7. Adoption only after two pilot PRs demonstrate value without material latency regression or review storms; otherwise roll back the optional helper cleanly.
  8. Release remains fail-closed: RELEASE_ALLOWED=NO, PRODUCTION_AUTHORITY_SWITCH_ALLOWED=NO, GATE_4_TERMINAL=NO until existing gates establish otherwise.

Ownership / sequence / non-goals

Priority P1 for Phase 0 and small MVP; P2 for optional hooks/advanced test tooling. Read-only Phase 0 may start immediately; Source Phase 1 is a new bounded separately admitted work item after immediate recovery E2c and required per-merge postchecks/retention, not as a surprise extra commit in #1033, #1021 or existing privacy/hold PRs. Do not delay E2c security fix to set up the verifier. Keep one local writer (Claude Code CLI) and serialize heavy operations on Ubuntu.

Linear plan mirror: the workspace free issue limit prevented new issue creation. The detailed Linear document is already attached to canonical QNB-194: https://linear.app/qnbs/document/worldscript-studio-claude-self-verification-umsetzungsplan-1034-qnb-bcced70eb0be. Do not retry a duplicate Linear issue or create a new governance parent. Update #780/#931/#550/QNB-194 with pointers only, not another independent policy. Parent scope remains with their existing owners. No PR or code was created as part of this planning issue.

Official Claude Code docs consulted: https://code.claude.com/docs/en/sub-agents , https://code.claude.com/docs/en/skills , https://code.claude.com/docs/en/hooks , https://code.claude.com/docs/en/best-practices (check locally installed version and current docs when implementing).


2026-10-13 refinement — prevent review cascades without shrinking required security proofs

Owner decision and non-goal. Expand the self-verification capability with evidence-driven, low-friction scope planning and correction-wave prevention. This is an enhancement of #1034, not a new anti-cascade governance workstream. The later, explicit QNB-194 maintainer decision prohibiting a standalone anti-cascade policy/tooling/hooks/check/budget PR stays in force. Do not create an extra mandatory gate, lower budget limits, write a new anti-cascade script, or mutate AGENTS.md/workflows/branch protection solely for this refinement. Keep all enhancements inside existing Phase-0 analysis and the already planned, separately admitted minimal agent/skill MVP; advanced components remain optional.

A. Verified case and budget truth — three distinct diffs, never one misleading number

  • At this checkpoint feat(core): publish a journal phase change only under exclusive admission #1033 (E2b) has 6 commits, 16 files, +1,257/-111 GitHub diff lines; fix(core): complete a prepared binding change only under the exclusive admission #1035 targets main and shows 8 commits, 21 files, +2,043/-189 because it contains feat(core): publish a journal phase change only under exclusive admission #1033's six predecessor commits. Actual E2c-only 8017776b...bff6e34b comparison: 2 commits, 14 files, +801/-93 GitHub diff lines. These are ordinary additions/deletions, NOT automatically the governance script's meaningful lines; use the existing evaluator for the authoritative budget. Both PRs were open/unmerged at this read; re-fetch before action.
  • Every verification packet should distinguish: (1) cumulative PR diff against its actual live PR base; (2) independent semantic slice diff from the prior admitted commit; (3) last review delta since the most recent substantive reviewer evidence. Record base/head/merge-base, base type, SHA lineage, and review epoch. If a PR is retargeted from a stacked base to main, explicitly identify any inherited predecessor commits and do not label a composite PR as an independent two-commit change.
  • Existing scripts/check-pr-size.mjs and docs/PR-CI-MERGE-WORKFLOW.md are authority: preferred target ≤8 files/≤400 meaningful lines/≤6 commits; hard-advisory ≤20/≤1200/≤10; absolute ≤30/≤3000/≤15. No new size ceiling or blanket splitting rule. Normal vs convergence vs saturation remain governed by the existing evaluator.

B. Contract-first Slice Passport — brief in-run analysis, NOT another required document

Before a first implementation commit, the existing writer answers in its current plan/issue: one falsifiable invariant; intended production entrypoint(s); all other reachable publishers/recovery/bootstrap/retry/takeover callers; affected authority states and irreversible crash windows; positive and negative oracle; actual potential file families; an approximate budget/uncertainty class; and the evidence that proves the split would leave no unsafe intermediate state. For low-risk fixes this can be three lines. Do not impose a standard multi-page form, new approval workflow, or extraneous separate documentation.

  • Execution-boundary cohesion > arbitrary LOC: group the minimal code, tests, type API and contract corrections needed to make one safety invariant true at every reachable entrypoint. Split independent guarantees/optional refactors/side-effectful families before coding only when each prospective intermediate main is independently safe, builds, and can be reviewed. If a split would temporarily introduce an authority bypass, keep the inseparable transition together even if it exceeds the preferred target; respect absolute caps and ordinary owner admission.
  • Early uncertainty branch: if caller census, recovery write points, platform semantics or previous invariant is unknown, the next action is read-only source reconnaissance (or a carefully scoped fault-model proof), not a speculative implementation or extra governance work.

C. Two lightweight, bounded adversarial verification passes

Pass 1 — BEFORE FIRST SOURCE COMMIT: fresh read-only r15-invariant-verifier considers the source/contract and proposed invariant, without the author's defended patch explanation. It asks whether another public/crate API, shared holder, bootstrap, restart, candidate journal or alias can produce the allegedly exclusive state; enumerates 1–3 highest-risk counterexamples, not an exhaustive speculative essay. A strong finding may reshape the admitted slice plan before coding. It must not silently expand owner authorization.
Pass 2 — AFTER TARGETED TESTS, BEFORE FIRST PUSH: inspect only the actual changed code plus neighboring authority paths and the adverse cases from Pass 1; try to falsify each security claim. Return an evidence packet with VALID_REPRO, PROBABLE_UNPROVEN, NOT_REPRODUCIBLE, DUPLICATE, OUT_OF_SCOPE_OWNER and UNKNOWN dispositions; author alone implements corrections and runs admissible tests.
Optional post-review surgical pass: only when Codex/CodeAnt found a new material root cause, inspect the sibling paths that could share it before the next correction push. Avoid an unbounded third/fourth subagent invocation, status-only PR pushes, full-context duplicate reviews or broad restyling.
Model-generated conclusions are hypotheses; a deterministic red-on-vulnerable/green-on-correct negative test, type-level proof, or explicitly bounded static call-graph check is the real oracle. External Codex remains independently useful and must not be replaced by Claude reviewing itself.

D. Proof design that avoids oversized test scaffolding

  • Prove at least one counterexample per material invariant and that required acceptance behavior still works. For multi-surface claims such as 'zero I/O' or 'no committed phase change', assert root slots, pointer, journal, anchor and any alternate root rather than sampling one mock call. Prefer narrow shared fixture helpers, parameterized crash-state tables and real typed API checks, provided abstraction does not hide semantics.
  • Favor a type-level non-compilability proof for forbidden call sites; explicit typed refusal for runtime invalid transitions; negative tests across bootstrap and restart. Do not create hundreds of repetitive variants merely to inflate coverage. Prove the test fails on a controlled bad implementation when reasonably feasible, otherwise mark this limitation honestly.
  • On R-15 request one compact adversarial schedule/authority matrix spanning authenticated predecessor, exclusive admission, root identity and durable steps C/E1/E2/F; expand only where risk or reviewer evidence warrants it. No blanket cargo test, Kani, Loom, mutation or browser matrix on local Ubuntu.

E. Forecast, review reserve, and split/no-split decision — advisory planning only

  • Estimate a range for semantic net code+proof+docs, file families, review-risk and possible follow-up. On high-risk paths, try to preserve approximately 20–30% of the relevant upcoming budget tier for findings when practical; this is a forecast, not a new rejection threshold or permission to omit required safety tests.
  • Before implementation and at first CONVERGENCE notice, classify projected remaining work into REQUIRED_SAME_INVARIANT, INDEPENDENT_SEAM, OPTIONAL_CLEANUP, NEW_UNADMITTED_SCOPE. Never sacrifice REQUIRED proof to make a prettier PR size. Never hide an unsafe residual behind a misleading doc claim.
  • If an independent seam can be delivered safely, plan the successor BEFORE repeated correction pushes. If not, keep the dependent code+proof together, manage correction wave and hard budget per existing policy. At absolute saturation, freeze and seek a safe successor/owner decision; do not rewrite commits or merge a known defect to manufacture capacity.
  • Do not treat the number of commits as a quality metric to game: preserve SSH-signing, auditability, reviewed exact-head and meaningful root-cause commits.

F. Correction-wave convergence and reviewer signal

  • In existing three-channel review reconciliation, cluster findings by root cause and execution boundary, review related paths once, reply with exact evidence, then implement the smallest complete correction. An additional validated P1/P2 after a correction is new information, not a 'process violation'; it still blocks unsafe merging. Nitpicks/format churn do not justify a new semantics-modifying push in CONVERGENCE.
  • Report REVIEWED_CLEAN, FINDINGS, RATE_LIMITED, QUOTA_EXHAUSTED, STALE_HEAD, UNKNOWN truthfully. Rate-limited optional reviewers are not silently transformed into passes or extra blanket merge vetoes; existing required deterministic checks and protection policy still apply. Allow no model, hook or assistant to auto-dismiss actionable Codex threads.
  • The goal is to detect paths before first push, not suppress or postpone legitimate discoveries. No 'never more than one wave' rule that overrides a real security finding.

G. Stacked PR review truth and GitHub branch safety

H. Secure, low-cost CLI implementation refinements

  • Skill is manual: frontmatter disable-model-invocation: true (verified official docs), concise on-demand instructions, explicit invocation and bounded output; do not use a skill allowed-tools field to inadvertently grant extra command access. The project subagent should use actual verified frontmatter such as tools: Read, Grep, Glob plus a narrow maxTurns and no write-capable MCP exposure; use a cheaper model for shallow census only if empirical recall remains adequate.
  • Permission checks MUST exercise actual installed CLI, parent permission-mode inheritance, prompt-injected source comments, write tool denial and unexpected MCP tools. A prompt asking an agent to be read-only is not an enforceable boundary. If reliable isolation is impossible, provide read-only analysis from a truly restricted outer execution context or do not admit the agent.
  • Local machine: disk high and rust-analyzer historically expensive; run read-only reasoning/cheap targeted prepush locally, never concurrent heavy Cargo/Rust analyzer jobs, use existing hosted CI. Stop on low disk/dirty workspace/invalid base rather than creating scratch churn. No automatic hook in MVP; later hooks require independent cost-and-security admission.

I. Qualification and value metrics: distinguish scope inflation from real defects

  • Baseline and pilot: >=5 prior known-case replays (including feat(core): publish a journal phase change only under exclusive admission #1033 Codex P2-B and alias race) with a negative control, and >=2 subsequent unseen admitted PRs. Partition known-answer replay vs new blind material finding; no leakage of answers in blind prompt. Record misses, duplicates, false positives, exact-source/callpath proof, and cost.
  • Per PR/epoch measure: (a) first_push_material_review_findings by defect class and severity; (b) prepush_validated_counterexamples; (c) correction_waves_due_to_new_semantic_faults (not just total commits); (d) real_slice_files/lines and composite_PR_files/lines; (e) unplanned_scope_families, review_latency, time_to_reproducer, token budget, disk/cache growth and Github runner-minutes. Avoid arbitrary lines-as-value metrics or '75%' effectiveness promises.
  • Compare with historical similar-risk PRs (feat(core): publish a journal phase change only under exclusive admission #1033/fix(core): complete a prepared binding change only under the exclusive admission #1035 are examples, NOT fair randomized controls), annotate material confounders (stack/base changes, reviewers unavailable, review depth, risk class). The actual adoption criterion is fewer independently validated material misses and comparable or better delivery economics without privilege expansion or loss of deterministic evidence. If no improvement, simplify or switch off the optional agent.

J. Cross-owner integration, rollout, and stop conditions

Implementation remains at #1034 with the compact Linear document under QNB-194. #780 owns reviewer/governance taxonomy, #931 owns exact-head normalization, #550 owns cost measurement, QNB-183 owns broad test architecture, #359/#922 own storage semantics. Only concise cross-link updates, not duplicated charters, new Linear issues or new CI workflows.
Phase 0 now: adopt this as a voluntary working method without repository mutation; capture a short Slice Passport and run a bounded manual read-only reconnaissance for the next already admitted security invariant. Phase 1: one deliberately small agent+skill PR only when separately admitted after E2c critical path, no changes to R-15 production code therein. Phase 2/3: measured negative-test/optional integration only on new owner decisions and bounded slices.
Stop if: true read-only boundary fails; case corpus/score is contaminated by author rationale; the validator requires new secrets; resource budget breaches; slice cannot be made independently safe; an unresolved material finding would be waived; or the proposed tool increases review complexity without demonstrated benefit. Preserve pending security fixes, exact-main CI, CodeQL, Vercel per-merge protection and release/cutover gates.

Minimal self-verification output (not a new administrative form)

{PR, base_SHA, slice_start_SHA, head_SHA, reviewed_delta_SHA, invariant, cross_path_calls, counterexample, deterministic_oracle, negative_result, evidence_scope, estimated_remaining_budget, real_slice_size, composite_PR_size, unresolved_findings, owner_disposition, time_tokens_disk, next_admitted_action}.
All fields may be UNKNOWN when not verified; do not invent data or block a simple safe fix to fill an irrelevant optional field. Output should stay concise and refer to existing PR comments/issues instead of repeated full descriptions.

Activity

  1. qnbs commented on Oct 13, 2026

    @qnbs
    OwnerAuthor

    Linear plan and authority linked (2026-10-13). Detailed implementation/qualification document: https://linear.app/qnbs/document/worldscript-studio-claude-self-verification-umsetzungsplan-1034-qnb-bcced70eb0be. Canonical Linear control-plane parent: https://linear.app/qnbs/issue/QNB-194. Linear new-issue creation returned free issue limit exceeded; do not retry creating a duplicate mirror until capacity changes. GitHub #1034 remains the concrete source implementation issue; the Linear document under existing QNB-194 is the planning mirror. Phase 0 read-only may start now. The agent/skill PR is NOT source-admitted until exact bounded authorization after the higher-priority E2c recovery security work. No hooks, privileged workflows, required checks, auto-merges, release or source changes have been performed by this planning step.

  2. qnbs commented on Oct 13, 2026

    @qnbs
    OwnerAuthor

    2026-10-13 refined implementation spec published. Issue body Sections A–J now cover pre-commit read-only bypass census, two bounded adversarial passes, cohesive invariant/negative proof, semantic-slice vs composite PR vs reviewer delta SHAs, advisory correction reserve, safe split/stack decisions, verified Claude skill/subagent permission semantics, resource controls and blind-pilot metrics. The canonical Linear work package contains the corresponding operational addendum. No new anti-cascade governance PR or tightened size gate; QNB-194's explicit cancellation stands. Phase 0 is read-only; the agent/skill source is NOT ADMITTED and must not preempt the E2c critical path.

  3. qnbs commented on Oct 13, 2026

    @qnbs
    OwnerAuthor

    Phase 0 (read-only) — inventory, replay corpus and smallest MVP scope (2026-10-13). Source MVP is still NOT admitted.

    Local inventory (read only, nothing installed or changed): Claude Code 2.1.296. The repo has no .claude/ directory (no project agents, skills or settings). User settings: defaultMode=auto, 1 allow rule, 0 deny rules, hooks present. Consequence for the verifier: its read-only boundary must be tested in Phase 1 (a subagent with only Read, Grep, Glob, parent permission mode and MCP inheritance verified, then an injected-text probe that tries Write/Edit/Bash); the auto-mode classifier is a safety net (it blocked a destructive git worktree remove --force today), not a tool restriction. Phase 1 cost expectation: one small local run, no heavy Rust/Node load; hosted CI stays the oracle.

    Replay corpus (real findings of the E2b/E2c stack; answers must not be given to a blind run):

    # PR / head Finding Root-cause class Mechanical oracle that catches it
    1 #1033 89e2a468 CodeAnt: root alias retargeted between admission and commit path spelling reused after admission alias-retarget test (Unix)
    2 #1033 32636c1b Codex P1: crate-root re-export of raw commit_root bypasses the typed publisher second reachable publisher of the invariant pub surface diff / compile-fail doctest for the bypass
    3 #1033 fec4ba1d Codex P2-A: bootstrap (committed=None) accepted by the phase-transition publisher entry state not refused before I/O refusal test comparing all durable resources before/after
    4 #1033 fec4ba1d Codex P2-B: crash after anchor prepare is completed by recover_root under a shared admission recovery path is a third publisher crash-window table (C/E1/E2/F) with shared vs exclusive recovery
    5 #1035 81a7c353 Codex P1: exclusive recovery still uses the caller's alias spelling path spelling in a new entry point same alias-retarget test applied to the recovery
    C #1035 a31cd406 control: CHANGELOG-only delta, no finding expected CLEAN —

    Pattern in 4 of 5 real findings: another reachable path to the same sink (cases 2, 3, 4) or a path spelling reused after admission (cases 1, 5). The pre-commit/pre-push read-only pass therefore asks exactly three questions per slice: (a) every function that can reach the sink — public re-exports, bootstrap, recovery, retry; (b) which spelling of every path is used after admission; (c) every crash window between prepare and commit. At most 1–3 strongest counter-examples per pass, each with a deterministic test oracle or marked UNPROVEN.

    Smallest MVP proposal (not started): .claude/agents/r15-invariant-verifier.md (tools limited to Read, Grep, Glob, bounded turns) and a manual .claude/skills/verify-r15/SKILL.md (disable-model-invocation: true, no allowed-tools). Input: base/head SHAs, the one invariant, admitted scope, contract references. Output: VALID_REPRO | UNPROVEN | NO_FINDING per counter-example, with SHAs and the oracle. No hook, no CI workflow, no required check, no reviewer replacement, no PR/thread/merge action.

    Pilot measure (later): the five replays above (known answers, KNOWN_REPLAY) plus the next two admitted security slices as blind runs (NEW_BLIND_FINDING); record true positives, misses, false positives, duplicates, wall time, tokens. A historical Codex find is not a new discovery.

    Decision needed to start Phase 1: explicit source admission for the two files above as their own small PR (after the open docs PR #1036). Until then nothing is created.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions