Bounded Loops: Pre-Run Spend Bounds, Proved Termination, and Verified Completion for Agent Harnesses

2.2 The nearest formal treatment, and the boundary it draws

• Graph Harness (Wei, 2026) proves termination and conditional soundness for a static DAG but excludes repair edges and assumes validation accuracy; this paper crosses that boundary and measures gate performance.Graph orchestration and durable execution make control flow explicit and survive process death, but do not specify who may declare that work ended well.Source: §1 · p. 2, §2.2 · pp. 5–6, §2.1 · p. 5

1.1 Contributions

• A bounded loop combines a worker, an independent gate, and a declared budget; its verdict boundary classifies failures using anti-tamper declarations rather than worker claims or run history.The resulting three-way classification is total, disjoint, and decidable; absence of something to check is a property of the work, not an admission by the harness.Source: §1.1 · pp. 2–3
• Termination under repair requires three stated conditions, including a global repair budget; the worst-case attempt bound is a pre-run closed form costing a factor of (R + 1).The proof uses a lexicographic measure on (R − ρ, remaining budget); a per-node repair budget can let two nodes repair each other indefinitely while both retain credit.Source: §1.1 · p. 3
• A graph cannot report done unless every node has a gate verdict in its append-only ledger, and a third party can check this from the run directory.The control-flow proof excludes any execution path where an agent’s claim about itself influences the outcome.Source: §1.1 · p. 3
• The instrument pairs mechanically generated Tier 1 mutants with Tier 2 semantic mutants and fixes ground-truth labels before gates are run.For model judges, conjunction with a deterministic gate cannot increase false accepts; the engine enforces that composition. The two mutation tiers are complementary, and labels do not depend on gate behavior.Source: §1.1 · pp. 3–4
• 47 of 57 shipped, reviewed loops in the catalogue had vacuous gates, checks that pass when the artifact they should check is absent.The instrument is offered so readers can measure their own gates; one example missed fabricated legal citations in unknown reporters because the search pattern came from the same reference set being checked.Source: §1.1 · p. 4
• Three self-attestation cases were found in separate subsystems, but neither mutant tier can detect this defect because it resides in machinery reading worker-owned artifacts.Self-attestation occurs when the subject supplies the value a check evaluates; unlike vacuity, it is remedied by consulting a value the subject cannot control.Source: §1.1 · p. 4

2 Related Work

• The passages distinguish declaration provenance from artifact verification; they report that intrinsic self-correction without external feedback may not reliably improve reasoning and can degrade it, motivating a checker the worker cannot write to.The evaluator-driven loop is part of the agent runtime, and no documented pre-emptive token or wall-clock ceiling was found. The other system records spend as deferred and has an append-only log that supports replay, not third-party tamper-evidence.Source: §2.3.2 · p. 7, §2.3.1 · p. 7, §2.5 · p. 8

2.6 Mutation testing

• Mutation labels fixed by the operation avoid selection bias without excluding equivalent mutants, but specification checking remains only partially discharged.The authors report one mutant labelled defective where the gate was right and no sampled specification review of Tier-1 labels. Their operators target artifacts beyond programs, with a second tier for requirements relating multiple artifacts.Source: §2.6 · pp. 8–9

2.7 Vacuity, which is not our term

• The paper adapts vacuity—the established notion that a check can pass without exercising its interesting condition—to hand-written harness gates, where analogous detection is absent.It proposes automatic checks for whether a gate constrains anything as a promising transfer from formal methods, but does not implement them.Source: §2.7 · p. 9

2.8 Workflow verification

• For repair-bearing graphs, the paper proves decidable termination rather than workflow soundness, and requires a computable pre-run bound for operators.Repair edges act like reset arcs: termination remains decidable for this class, while workflow soundness is undecidable; the bound must be computable from the manifest.Source: §2.8 · pp. 9–10

2.9 Runtime verification, and contracts

• A gate is a runtime monitor of a particular execution, but unlike conventional runtime verification, it checks hand-written code over arbitrary artifacts rather than formal properties over defined traces.Because the worker is nondeterministic and assumed to meet nothing, the contract must be an independent postcondition the worker cannot reach; the monitor itself therefore needs measurement.Source: §2.9 · p. 10

2.10 Anytime-valid inference

• Betting-based confidence sequences provide inference valid at every sample size, while the reported quantity is the log’s mean over attempts—not a population forecast.The paper notes that an earlier internal write-up confused these quantities and reports that error in Section 12.Source: §2.10 · p. 10

3.1 Workspaces, artifacts, and ownership

• A workspace is the worker-visible mutable state; artifacts are gate-read subsets, while a declared forbid set separates worker-owned files from loop-shipped anchors.The forbid set is fixed in the manifest before a run, rather than inferred from behavior.Source: §3.1 · p. 11

3.2 Workers, gates, and the independence requirement

• Independence requires a distinct gate that cannot write its code into the worker-owned region and whose input excludes the worker’s transcript.A same-repository validation step may be reachable by the worker and receive its account of the work.Source: §3.2 · pp. 11–12

3.3 The verdict set

• The verdicts are pass, reject, and incapacity; an empty, vacuous, or malformed worker-owned artifact is not a permitted reason for incapacity.Incapacity means the gate could not form an opinion, not that there was nothing to check.Source: §3.3 · p. 12

3.4 Bounded loops

• A bounded loop repeatedly runs a worker and gate until the first pass or budget exhaustion, with outcomes distinguishing done from halt, pause, killed, and error.Budgets include finite attempt and no-progress ceilings; halt concerns unsuccessful work, while error means the harness could not tell.Source: §3.4 · p. 12

3.5 Receipts

• Each attempt’s receipt records its verdict, decision, consumed budget, and predecessor hash; receipts form the append-only ledger and hash-chaining makes silent edits detectable on replay.The hash chain provides tamper-evidence, not a signature.Source: §3.5 · p. 13

3.6 Bounded-loop graphs

• A bounded-loop graph keeps dataflow acyclic and models repair as a bounded new pass that re-admits an ancestor and its descendants after a node halts.Repair restarts per-pass progress, so the proof uses a two-variable induction rather than an ordering of nodes.Source: §3.6 · p. 13

4 The Verdict Contract

• The verdict boundary uses pre-run ownership declarations to make failure classification explicit, total, and disjoint.The classification is derived from the loop’s declared forbid set rather than guessed from the failure.Source: §4 · p. 14, §4.2 · p. 14

4.1 Two verdicts are not enough

• The same malformed file can require opposite responses depending on whether it is worker-owned output or protected ground-truth data.A binary pass/fail contract cannot distinguish a recoverable worker error from a checker-side problem in this case.Source: §4.1 · p. 14

4.2 The trichotomy

• The trichotomy classifies each gate run as pass, reject, or incapacity using only the workspace and declared forbid set.The classification does not consult the worker, its transcript, or run history.Source: §4.2 · pp. 14–15

4.3 Why ownership, and not severity

• Ownership, not failure severity, supplies the boundary because the loop author records worker responsibility in the anti-tamper forbid set before the run.The same parse error can fall on either side of the boundary depending on whose file it is.Source: §4.3 · p. 16

4.4 What it costs to get this wrong

• Twenty-four catalogue checkers returned incapacity for empty, vacuous, or malformed worker artifacts, ending retries and corrupting measurement.A worker that emitted broken JSON could be stopped instead of receiving actionable feedback to try again.Source: §4.4 · p. 16
• 84 of 233 held-out mutants were marked not judged and excluded, while seven loops produced only incapacity and the surviving rate looked perfect.A misfiled verdict can silently remove hard cases from the evidence base.Source: §4.4 · p. 17

5.2 A single loop

• A single loop terminates within m attempts when each worker and gate invocation terminates; its no-progress window can tighten the ceiling to min{m, w + j*}.Here j* is the last attempt on which the artifact changed; the bound is an upper bound, and the section later tests whether it is attained.Source: §5.2 · pp. 17–18

5.3 The graph procedure

• Figure 8 opens repair only after the ready set empties, reads rounds spent from ledger receipts, and resets the repair target and its descendants.These guards prevent repair from pre-empting ordinary progress, preserve the round count across crashes, and implement suffix locality.Source: §5.3 · p. 19, Figure 8 · p. 20
• Termination is conditional: an outstanding human approval suspends the graph, so a run waiting on a person does not terminate under the theorem.The procedure returns without sealing the run while approval is outstanding.Source: §5.3 · p. 20

5.4 A graph of loops

• (R + 1)Σ_v m_v bounds total graph attempts under Assumption 5.1, terminating worker and gate invocations, and no node terminating in pause.The bound charges every node its full attempt budget in each of at most R + 1 rounds; the quantities are declared in the manifest before execution.Source: §5.4 · pp. 21–22
• The graph proof uses a decreasing pair: attempts reduce remaining per-round budget, while each repair reduces the globally bounded round budget.Admissions may leave the pair unchanged, but at most |V| admissions occur per round.Source: §5.4 · pp. 21–22
• The graph bound is deliberately loose: it charges every node its full budget each round, making it computable from the manifest without reachability calculations.A generous ceiling makes the run stop earlier than the budgeted count, never later.Source: §5.4 · p. 22
• A single global repair counter makes the graph bound provable; per-node counters can allow two nodes to repair each other indefinitely while each retains local credit.The global round count is read from the ledger, so a crash and resume cannot reset the repair limit.Source: Figure 8 · p. 20, §5.4 · p. 21, Figure 9 · p. 23

6 The bound is tight, not merely valid

• The section asks whether the declared attempt bound is the number actually consumed, not merely whether termination occurs.It defines utilisation as a/m and treats attainment of the effective soft ceiling as an empirical question.Source: §6 · p. 23

6.1 Design

• The test varies seeded defective-record workload and productive attempts, using the shipped gate, bounds, manifest, and ledger with only record count and worker quota edited.The worker is deterministic; the experiment measures controller arithmetic and is not a benchmark of agent capability.Source: §6.1 · pp. 23–24

6.2 Utilisation

• 9 of 9 cases had predicted attempts equal observed attempts, and bound utilisation U reached exactly 1.0 when workloads exceeded m = 10.The table describes a run that halts at the ceiling rather than taking an eleventh attempt.Source: Table 1 · p. 24, §6.2 · p. 24

6.3 Soft-bound yield

• 4 of 4 cases attained the effective soft bound exactly; stalled loops stopped after w = 3 wasted attempts, saving three to seven attempts against m = 10.On a provider with a median measured turn of 48.3 s, seven saved attempts correspond to about six minutes and seven billed turns per stalled run.Source: Table 2 · p. 24, §6.3 · pp. 24–25

6.4 Positive control

• The positive control requires both convergence and stalling before results are reported, guarding against meaningless agreement from a harness that ran zero attempts.The controls reported convergence at attempt 2 and a stall at the window of 3.Source: §6.4 · p. 25

7.1 The invariant

• A graph terminating in done is ledger-supported: every node has a gate pass receipt, and no worker assertion determines that outcome.The guarantee concerns receipt provenance, not whether the gate’s pass was deserved.Source: §7.1 · p. 25, §7 · p. 25
• A third party can verify ledger support from the run directory without rerunning the work or trusting the engine that produced it.The verifier checks ledger support and the hash chain using the directory’s receipts and node set.Source: §7.1 · p. 26

7.1.1 The verifier, and the three things it reports separately

• The verifier reports chain integrity, an external head anchor, and completeness separately; a well-formed truncated prefix needs independent expected-length evidence to detect truncation.It distinguishes verified, broken, torn-tail, unchained, and mixed chain outcomes rather than collapsing missing evidence into a pass.Source: §7.1.1 · p. 26

7.2 What the invariant does not say

• The guarantee is relative to gate quality and structural independence: a gate can wrongly accept defective work, and disjoint write authority does not ensure uncorrelated errors.A checker written earlier by the same model that wrote the artifact can satisfy the structural definition while lacking the intuition of independent review.Source: §7.2 · p. 27

7.3 Tamper evidence

• A hash chain detects modification of earlier rows if the adversary cannot recompute the suffix; detecting truncation additionally assumes an unmodifiable manifest.The final row has no successor to carry its hash, and rewriting the whole file remains possible without an independently held digest.Source: §7.3 · pp. 27–28
• The ledger records independent checker verdicts, whereas an execution history records orchestrator actions such as scheduling, returns, and retries.The section frames the ledger as evidence for whether completion was earned, rather than a reconstruction of the execution.Source: §7.3 · p. 28

8 Vacuity: a Gate Satisfied by Nothing at All

• 47 shipped-catalogue defects and 14 test-suite defects were vacuous.The 14 test-suite defects included three security guards that still passed when tool registration was stubbed to a no-op.Source: §8 · p. 28, §8.3 · p. 30

8.1 Definition and the basic result

• A gate is vacuous when its predicate holds for absent or empty artifacts, allowing a worker that deletes the artifact to reach done in one attempt.The theorem establishes that a vacuous gate permits a worker to satisfy none of the loop’s purpose and still finish.Source: §8.1 · p. 28
• An empty ledger can satisfy balance and categorisation checks, while a citation gate can miss fabricated reporters absent from its reference file.The citation scanner derives its search pattern from the same reference file it validates against, so the invented citation is never matched.Source: §8.1 · p. 29

8.2 Why review does not catch it

• Line-by-line review can miss vacuity because individually correct universal assertions pass on empty collections, and prompt-only prohibitions are not enforced by a gate.Reviewers may see correct assertions without noticing their quantifier structure; a requirement stated only in the prompt remains a request to the worker.Source: §8.2 · p. 29, §8.1 · p. 29

8.3 Two shapes, and a guard that missed one

• Vacuous checks occur inside loops and in accumulated-error checks, and the first scanner detected only one of these two shapes.An assertion outside a loop can still be vacuous when it checks that an error list is empty after processing empty input.Source: §8.3 · p. 30

8.4 The remedy, and its limits

• Existence obligations can prevent empty-artifact passes, but setting a required floor too high risks rejecting legitimate work.Pinning expected transaction identifiers catches partial as well as total deletion; reference data should act as a floor, not a ceiling.Source: §8.4 · p. 30

8.5 Vacuity at the harness level

• An environment allowlist caused a loop to exhaust its budget without the worker running, showing that a recorded attempt count needs independent evidence of an attempt.The run was correctly bounded and logged, but its receipts could not distinguish four failed attempts from no attempts at all.Source: §8.5 · p. 30

9.1 Definition, and a proof that is deliberately trivial

• A check is self-attested when the subject controls the value to which the check applies, making it possible to pass while the property fails.The proposition establishes that a subject can choose a value satisfying the check’s criterion despite violating the property.Source: §9.1 · p. 31

9.2 Three instances, in three unrelated subsystems

• Examples include an empty verdict reason that reports itself non-empty, a permissive fake interpreter, and provenance a gate can write into the ledger.The launcher’s original assertion passed, while five of seven cases failed after it was rewritten to check resolution order.Source: §9.2 · pp. 31–32

9.3 Why it is not vacuity, and what the remedy is

• The remedy is to make the checked value harness-controlled, by consulting identity, calling an operation outside the object, or passing in what the harness already knows.For test stand-ins, the corresponding rule is to ensure they refuse what production refuses.Source: §9.3 · p. 32

9 Self-Attestation: a Check Answered by Its Subject

• Three self-attestation instances recurred across unrelated subsystems, though their audit provides no recall rate.The instances were in verdict validation, a packaging launcher, and a provenance record; the audit reproduced each by hand but used no held-out mutant set.Source: §9 · p. 31, §9.3 · p. 32

10 Measuring a Gate

• Both false-accept and false-reject rates matter, while defects authored with access to the gate cannot reveal failures the author did not anticipate.The section defines α as false accepts and β as false rejects; an all-rejecting gate has α = 0 but is worthless.Source: §10.1 · p. 33, §10.2 · p. 33

10.3 Blindness as a static property

• An AST check enforces syntactic routes to gate information, but does not establish information-theoretic independence; labels fixed before gate execution avoid gate-dependent selection.The gate-conditional exclusion rule can make the estimated α identically zero for a test-suite gate, regardless of its quality.Source: §10.3 · pp. 33–34, §10.4 · p. 34

10.5 Two tiers, because one is not enough

• Tier 1 applies blind mechanical operators, while Tier 2 uses independent authors shown only the loop’s purpose to test artifact relationships Tier 1 cannot express.The tiers address complementary requirement classes rather than strong and weak versions of one method.Source: §10.5 · p. 35

10.6 What the interval means

• The anytime-valid confidence sequence estimates mean false-accept propensity across attempts actually recorded, not a forecast of future attempts.Its coverage holds at every sample size, allowing inspection at any point without inflating the error rate.Source: §10.6 · p. 35

11.1 Layering, and the rule that keeps it

• The engine uses ports and adapters, with only one composition module permitted to wire concrete adapters to ports.An AST walk checks imports across every module, including function-local and dynamic imports.Source: §11.1 · p. 37, Figure 10 · p. 37
• The receipt log is the sole durable state and each surface projects it, preventing disagreements between surfaces about a run.After interruption, files needed to reconstruct a run were written too late for surfaces to open it, despite a chain-valid log.Source: §11.1 · p. 37

11.2 Gates, and why they are keyless

• The catalogue uses deterministic schema, command, and test-suite gates, while a model judge may be added only in a composition that cannot raise false accepts.The section says the predicate reductions for subjective-sounding requirements are not always faithful; one is explicitly a proxy.Source: §11.2 · pp. 37–38, Table 3 · p. 38

11.3 Anti-tamper

• A workspace tampered with during a run never reaches the gate, and provider-reported work is untrusted for completion decisions.The runner wrapper checks protected anchors, forbidden files, and test-collection configuration; usage reports serve accounting only.Source: §11.3 · p. 38, §11.4 · p. 38

12.2 E1 — Tier-1: mechanical, blind mutants

• 0 false accepts occurred on 62 conforming Tier-1 mutants; Wilson 95% upper bounds were 2.2% for Tier 1 and 9.2% for Tier 2.Tier 2 is an existence proof of an evasion class Tier 1 cannot construct, not a second confirmation of zero false accepts; its corpus has no conforming cases for measuring false rejects.Source: §12.2 · p. 39

12.3 The corpus was worth building because it found things

• 47 gate defects were pinned as regression cases, while fixing a measurement-scope bug increased Tier-1 coverage from 34 to 57 loops.The 47 comprise 20 false accepts, 2 false rejects, 14 acceptances after partial fixes, and 11 rejections misfiled as incapacity. A separate verdict-contract defect misfiled 84 of 233 mutants, excluding hard cases from the denominator.Source: §12.3 · p. 40

12.4 Authors document how their gate is permissive, not how it is strict

• Three of four false accepts were disclosed in gate documentation, neither false reject was, and four proposed “not mechanically checkable” cases proved checkable.The six hand-found defects support no rate; a separate invoice mutant changing 50 to 50.0 was mislabelled because JSON treats the values as equal, and the corpus retains it as a correction.Source: §12.4 · p. 41, §12.6 · pp. 42–43

12.5 E2 — Tier-2: semantic mutants authored blind

• 38 Tier-2 mutants were judged, with 0 false accepts and 0 false rejects after the tier exposed 16 gate defects.Tier 2 found four defects in test-presence-per-module, which Tier 1 excludes; across three loops, deleting a violating item passed checks that lacked an existence floor.Source: §12.5 · p. 42

12.7 E3 — The confidence sequence, and which estimand it covers

• The anytime-valid bounds were α ≤0.1916 and β ≤0.2136, roughly three times wider than the fixed-n bounds of α ≤0.0664 and β ≤0.0739.The anytime-valid guarantee holds at every stopping time; the reported estimand is ¯µn, and controls show coverage falls when the interval is narrowed or its centre shifted.Source: §12.7 · p. 43, Table 7 · p. 43

12.8 E4 — Workers that try to game the gate

• Adversarial workers that claimed completion, edited checkers, or planted collection configuration never reached DONE; the gate or anti-tamper guard blocked them.Deleting an artifact instead produced rejection only where an existence obligation was declared, a coverage gap revealed by E1 and E2.Source: §12.8 · pp. 43–44

12.9 E6 — The instrument, turned on ourselves

• Scanning 2,811 test functions across 222 files found 14 vacuous tests; after repair, none remained.The first scanner missed an accumulate-then-assert pattern, so its guard was strengthened to catch both forms and include a deliberately vacuous test case.Source: §12.9 · p. 44

12.10 E5 — Cross-model convergence

• 16 of 16 cross-provider arms reached done on their first attempt across four loops, with terminal state and attempt count invariant despite differing wall times.This modest result is not a capability benchmark. A first run that appeared to show one provider halting was traced to denied file-writing permissions and a workspace mismatch; the gate correctly rejected the unchanged workspace.Source: §12.10 · pp. 44–45, Table 8 · p. 45, §12.11 · p. 46

12.11 A near-miss worth more than the result

• End-to-end runs exposed two shipped engine defects: rejected CLI flags and a missing subprocess environment variable each caused an agent to do nothing without appearing in the ledger.Both defects were fixed; the runners had not previously been driven against real binaries end to end.Source: §12.11 · p. 46

12.12 E7 — The post-freeze corpus, and what a frozen gate still admits

• 21 apparent false accepts over 67 destroying mutants became 14 after adjudication excluded seven mislabeled mutants.The seven exclusions were failures of the operators’ assumptions; the rule now fails closed when a requirement names no quantifier, losing one true positive rather than admitting an unlabelable trial.Source: §12.12 · p. 47
• Of the 14 valid false accepts, ten were vacuous checks on emptied collections, one quantified over removed records, and three completeness gates accepted hollowed content.The three gates checked required headings but not body content; the shipped operators deleted headings too, so only a hollowing operator exposed the gap. All three were fixed after this measurement.Source: §12.12 · pp. 47–48

12.13 E8 — A class the instrument cannot generate

• Three accepted findings showed self-attestation defects outside both mutant tiers, which mutate worker-owned artifacts rather than harness code that decides whether a gate’s answer is trustworthy.Examples included a verdict-reason rule consulting the verdict, an install-policy test consulting a stub written to agree, and a gate-run record reading its answer from the gate.Source: §12.13 · p. 48
• A short-circuited platform precondition let test modules pass on one host while failing collection elsewhere, a defect the type-checker found because the suite did not execute that code.Three modules gated themselves at import time; the authors’ platform made the first disjunct true, so the second was never evaluated there.Source: §12.13 · p. 48
• E8 establishes the existence of an instrument-blind defect class as a case report, not its recall or replicability.It used two auditors on one codebase and release, had no held-out set, and the authors also filtered accepted findings; the commercial tools’ versions could not be pinned.Source: §12.13 · pp. 48–49

13.1 Three ceilings and one derived bound

• A graph’s worst-case attempt total is bounded in closed form when repair uses a global budget; a loop’s effective attempt bound is min{m, w+j⋆}.A stalled loop stops after w unchanged attempts rather than necessarily consuming its full cap m.Source: §13.1 · p. 49

13.2 What the wallclock ceiling promises

• The manifest declares attempt, cumulative-token, wallclock, and no-progress ceilings; the declared wallclock bound W plus gate timeout G bounds total run time by W + G.Total worker time, including wind-down, is bounded by W; in shipped wiring G = W, giving a worst case of 2W. The proposition requires a declared W and a gate timeout G.Source: §13.2 · pp. 49–50, §13.1 · p. 49

13.3 Reserving, not extending: a bound that does not destroy what it interrupts

• A reserve r partitions W into work time and a bounded handoff, so a wind-down turn does not extend the ceiling or change the termination and spend guarantees.The wind-down occurs at most once and is bounded by r; an external kill switch receives no wind-down, and the handoff cannot change the terminal state.Source: §13.3 · p. 51

13.4 Auditing consumption from the receipt

• The append-only receipt records whether a worker was invoked and names the handoff file, allowing a third party to recompute consumption without counting pre-attempt halts as spent work.Bound utilisation is U = a/m, where a is attempts spent and m is the declared cap; U > 1 would indict the instrument, not the run.Source: §13.4 · p. 51

14.1 The defect

• A loop declaring a 120-second wallclock ceiling ran one attempt for over 300 seconds, because enforcement occurred only between attempts and a runner default stopped it.The declared limit was exceeded by 180 seconds before the unrelated 300-second runner default terminated the attempt.Source: §14.1 · p. 52

14.2 The second defect, which the first was concealing

• 65 of 69 loops allowed six seconds per attempt, while 31 real turns had a 48.3-second median and reached 270.6 seconds.All catalogue tests passed because the demonstration worker completed an attempt in roughly 0.4 seconds.Source: §14.2 · p. 52

14.3 Repair, and how the numbers were chosen

• 90 seconds is the rounded-up measured 75th-percentile turn; choosing that percentile rather than the maximum kept the ceiling capable of binding and stable at 72.5 seconds across runs.The observed maximum moved from 177.6 to 270.6 seconds, while the 75th percentile remained 72.5 seconds in both runs.Source: §14.3 · p. 53

14.4 Why we publish this, and why the class is not ours alone

• The authors publish the defect because outside inspection could not detect it; the same declared-without-enforcement pattern appears in recorded production incidents.The paper notes that the reported defect cost nothing because its workload was a demonstration, not because the defect differed in kind.Source: §14.4 · p. 53

14.5 Why this generalises past our system

• For each declared limit, ask what test fails if enforcement is deleted; reverting the shared clamp now fails source-level tests across all seven runners.The end-to-end test reports 60.1 seconds against a declared two-second ceiling when the clamp is reverted.Source: §14.5 · pp. 53–54

14.6 Two further instances of the same shape

• Six copied change detectors used a stale snapshot, preventing the no-progress bound from firing after earlier writes; two prompt builders omitted forbidden actions from worker instructions.The change detector is now one content-addressed function; the omitted prompt rules led to rejected work on rules the worker had not been given.Source: §14.6 · p. 54

14.7 The instance we produced while writing this section

• The reserve adapter used W/2 for even ceilings despite the strict r < W/2 hypothesis, leaving that proposition’s condition unestablished on 90 of 180 tested ceilings.The stated remedy is ⌊(W −1)/2⌋ and a test that sweeps the inequality rather than restating a value.Source: §14.7 · p. 54

15.1 One defect class, found seven times

• Across seven layers, a recurring defect was a locally correct answer that the caller misread, with the failure silent and flattering.Examples include vacuous gates, excluded mutants, missing loops in measurement, tests that never proved collections non-empty, and runner or workspace mismatches.Source: §15.1 · p. 55
• The same defect class also appeared in 14 tests, the scanner, runner arguments, and provider workspaces, including checks that let empty collections pass.The listed cases include 14 tests that asserted over collections without proving they were non-empty, a scanner that missed one vacuity shape, and runners that did nothing or wrote outside the gate’s workspace.Source: §15.1 · p. 55

15.2 A second axis, found by parties who did not write the code

• Three release-audit checks were self-attested: verdict-reason, install-policy, and gate-identity checks asked the party under scrutiny for the answer.This differs from misreading a return: the authority of the answer, rather than its interpretation, is the issue.Source: §15.2 · p. 55
• Two implementations of agent-CLI driving each had tests but no agreement test, and the same capability was present in one and missing in the other four times, in both directions.Source: §15.2 · p. 56

15.3 Threats to validity

• The gates and mutation operators share a project, so an unimagined defect class may be absent from both; independent auditors found one harness-level class but could not bound what remains.The filter that accepted the auditors’ findings was still the authors’ own.Source: §15.3 · p. 56
• Zero false accepts across 209 destroying mutants gives a 1.8% Wilson upper bound at 95%, supporting only that this corpus found no remaining defects in these gates.The per-tier upper bounds are 2.2% and 9.2%; zero follows 47 fixes and does not establish that the gates have no defects.Source: §15.3 · p. 56
• Transfer beyond the authors’ 69-loop catalogue is untested; E5 has 16 observations and no shell-path token data, and no benchmark against another framework is provided.E5 supports only that the gate decided the same way regardless of which model wrote the artifact on those loops, not a quantitative provider conclusion.Source: §15.3 · p. 56

• Theorem 5.2 covers repair that re-runs a finished upstream node, excluded by the Graph Harness framework (Wei, 2026), using an outer induction and sufficient conditions for restored budgets.Because budget restoration creates reset arcs and the general soundness question is undecidable, the result gives sufficient conditions rather than a general procedure.Source: §16 · p. 57
• The completion invariant is stated as a formal property and proved, rather than left as a design intention about verifier independence.The paper identifies this as a theorem-level statement of an agent harness’s completion invariant.Source: §16 · p. 57
• The verdict boundary is derived from anti-tamper configuration, distinguishing a wrong artifact from a broken checker; the corollary was worth 84 of 233 mutants.Source: §16 · p. 57
• The paper reports 47 vacuous gates in a reviewed shipped catalogue and 14 in its test suite, measuring a verification defect class in production agent code.The concept of vacuity is borrowed; the contribution is measuring its incidence in this setting.Source: §16 · p. 57
• Because the subject is a verifier, the mutation methodology is inverted; the paper also gives a model-judge composition result requiring no calibration or accuracy premise.The composition is enforced in the engine, with its cost assigned to β and measured.Source: §16 · pp. 57–58
• The paper reports its own scanner, coverage, defect-category, and product-configuration errors rather than presenting its evidence as curated beyond scrutiny.Source: §16 · p. 58

17.1 Gate independence under shared authorship

• Shared model authorship may align worker and gate errors even when their write authority is disjoint, a risk structural independence does not rule out.The paper identifies measuring this worker–gate relationship as a key open problem.Source: §17.1 · p. 58, §18 · p. 61
• A proposed experiment compares escape rates for model-A mutants against gates written by A versus B, with loops and budgets fixed.A measured gap would support recording checker provenance and flagging shared authorship.Source: §17.1 · p. 58

17.2 Does α compose across a graph?

• Whether node-level false-accept rates compound across a graph remains unmeasured; shared inputs and shared gate idioms challenge the independence assumption.A proposed two-node experiment seeds a defect missed upstream and measures how often the downstream gate catches it.Source: §17.2 · p. 58

17.3 The retry budget is an unreported confounder

• Retry count affects the chance of a defective artifact passing, but reported reliability figures omit that parameter; α may also change as workers adapt to rejection.The proposed experiment measures α by attempt index; if it rises, the stated anytime-valid guarantee no longer holds.Source: §17.3 · p. 59

17.4 What is genuinely not mechanically checkable?

• All four requirements previously filed as beyond mechanical checking proved checkable; the category’s real boundary remains unknown.The paper argues that an entry should be treated as a claim that no implementation exists only after trying to write one.Source: §17.4 · p. 59

17.5 An automated prober for both defect classes

• Vacuity has a syntactic scanner, but self-attestation was found by manual review and fix reversion; this release has no automated prober for either class.A proposed self-attestation prober would substitute a hostile subject and test whether the check still discriminates.Source: §17.5 · p. 59

17.6 Gate decay and continuous recertification

• The proposed longitudinal experiment replays a fixed corpus at successive commits to track gate decay, which can hollow out a check while it still executes.The conclusion frames the instrument—not its reported rate—as the contribution, while noting that generalization beyond the authors’ catalogue remains unestablished.Source: §17.6 · p. 60, §18 · pp. 60–61

18 Conclusion

• 23.3% of defects were falsely accepted by frozen gates under a fresh operator family, despite zero false accepts on the exhausted corpus.The fresh family probed a defect class the first family could not express.Source: §18 · p. 60

A.1 Termination, without the no-progress window

• A no-progress window can only halt earlier, so even a useless progress function cannot extend a run beyond the attempt ceiling.Its failure mode is wasted budget, not non-termination.Source: §A.1 · p. 61

A.2 Why the graph induction needs two variables

• Graph termination uses the lexicographic measure (R −ρ, Σ), because repairs can reset the attempt count while the repair-round count alone cannot bound attempts within a round.A repair edge acts like an outer loop around DAG traversal.Source: §A.2 · p. 61

A.3 Soundness under partial failure

• Only a run ending in done makes a claim about artifacts; surviving ledger prefixes remain chain-valid after a crash, though a valid prefix must also be readable.An early implementation wrote reconstruction metadata only at run end, leaving a valid prefix that could not be opened.Source: §A.3 · pp. 61–62

A.4 Blindness: what the AST check covers, and what it does not

• The AST check blocks specified imports, checker-source access, loop-name comparisons, and subprocesses, but cannot reject imports whose targets are computed dynamically.It guards against ordinary maintainer drift, not a determined generator author.Source: §A.4 · p. 62

A.5 Unbiasedness, stated more carefully

• The estimator’s denominator is independent of the gate, but that does not prevent a systematically narrow operator set from making α optimistic.Tier 2 exists to probe failures the fixed operator set cannot express.Source: §A.5 · p. 62

A.6 The interval reported with zero failures

• At 95% confidence over this corpus, the supported bounds are α ≤1.8% and β ≤5.8%; α is not zero, and pooled figures summarize two structurally different sampling processes.Per-tier bounds are the primary figures; the pooled rate is a convenience.Source: §A.6 · p. 63

A.7 Bounded elapsed spend, proved

• The elapsed-spend proof admits attempts only before the work ceiling, clamps their remaining time, and bounds total worker time by W and total run time by W + G.The reserve condition r < W/2 makes work exceed courtesy; gate calls are not clamped because an incomplete check has issued no verdict.Source: §A.7 · pp. 63–64

B A Pattern Catalogue for Gate Design

• The catalogue is a measured design space, not a proposed methodology, and includes failure modes that can make gates silently stop working.It covers 69 loops and was measured by instruments that found 61 defects between them.Source: B A Pattern Catalogue for Gate Design · p. 64

B.1 What a gate can be

• A schema defines correctness by what it admits, a test suite can pass over an empty collection, and a predicate is expressive but prone to author error.Two apparent false accepts were judged correct under their schemas’ contracts.Source: §B.1 · pp. 64–65

B.2 Reducing a requirement to a predicate

• Requirements that seem to need judgement can often be recast as obligations about observable witnesses; where no witness exists, a model judge must be conjoined with a deterministic gate.The engine refuses other model-judge compositions.Source: §B.2 · p. 65

B.3 How gates fail, in the order they were found

• Existence checks guard against absence, while substance checks require content beneath a required element to guard against hollowing.Applying a remedy to the instance that revealed a defect class does not ensure the class itself is covered.Source: §B.3 · p. 65

B.4 What we would tell an author, and what we cannot

• Gate authors should encode every requirement, default to refusal when a requirement cannot be checked, and test against defects they did not write.They should also avoid asking the subject for values the checker can determine itself.Source: §B.4 · pp. 65–66
• The catalogue’s pattern frequencies and defect rates cannot be assumed to generalize beyond its 69 selected loops, domains, gates, and operators.The authors say external generalization requires applying the instrument to gates they did not write.Source: §B.4 · p. 66

C.2 Two catalogue entries the paper does not round away

• The catalogue retains a known mislabelled invoice mutant because JSON treats 50 and 50.0 as equivalent, and its category for mechanically undecidable requirements remains empty after four entries proved checkable.The authors do not know the category’s true boundary.Source: §C.2 · pp. 66–67

D.1 Setup; D.2 What regenerates what; D.3 Why the corpus is a test rather than a script

• Rates use 57 of the 69 catalogue loops, and the corpus is part of the test suite so regressions that reintroduce any of 47 defects fail at the relevant commit.Table 14 is identified as a reproduction map; the exclusions table supplies the rate denominator.Source: Table 13 · p. 68, Table 14 · p. 68, §D.3 · p. 68

D.4 Section 12.10, and what will not reproduce

• E5 reproductions should match terminal state and attempts-to-done, but wall-clock times may differ and token counts are absent.The path does not parse provider usage envelopes, and a fifth profile was held out for budget reasons.Source: §D.4 · p. 69

D.5 Verifying a run without trusting us

• Replay detects modified ledger entries and torn tails, but a party able to rewrite the whole file can rewrite the chain; external signatures are needed to prevent that.This is tamper-evidence, not authentication.Source: §D.5 · p. 69

E.1 An auditor is an agent, and an agent writes

• An auditor changed three source files during another auditor’s review, invalidating both auditors’ findings for the interval; separate detached worktrees prevent this shared-tree hazard.Auditors’ proposed fixes should be treated as findings and reproduced independently, not accepted as patches.Source: §E.1 · p. 69

E.2 Four guards that could not report

• Four audit guards could not reliably report failure: an empty output passed, a type-check step never ran, an excluded filename caused a permanently red test, and an environment-specific assertion could not pass on the runner.The release test now fails against a deliberately broken subject.Source: §E.2 · p. 70

E.3 A mechanical probe, and its one gap

• Reverting 12 repairs made 11 guards fail as expected, while one uncovered call site stayed green; another revert caused a loop that never finished.The release has no mechanical prober, and a future one needs a per-mutant deadline with timeout as a third outcome.Source: §E.3 · p. 70

Availability and Licensing

• The engine, catalogue, reference graphs, mutation harness, scripts, and figures are released under Apache-2.0.The figures and Section 12 numbers are emitted from receipt logs by repository scripts.Source: Availability and Licensing · p. 70

Conflicts of Interest

• Tier 1 and Tier 2 corpus construction and released analysis scripts are presented as mitigations for authors’ conflict of interest in measuring their own gates.The authors also report unflattering findings, including a mislabelled mutant and defects in their own tests.Source: Conflicts of Interest · p. 71