In mainstream agent frameworks, a step ends when the agent's own output says it has finished. Durable-execution platforms bound retries and time, but their checker conventionally lives in the same codebase as the work: a discipline the deployment is trusted to keep, not a property the harness enforces. We state what an agent harness must guarantee, prove it, and build the instrument that measures whether a harness delivers it. A bounded loop is a worker, an independent gate the worker cannot write to, and a declared budget; a bounded-loop graph composes them with a repair relation that lets a downstream failure re-run a finished upstream node. Three guarantees follow. It finishes: termination holds under repair, with the worst-case attempt total in closed form, if the repair budget is global not per node. It does not drift: no node reaches DONE without a gate verdict in an append-only hash-chained ledger, proved from control flow, since repair leaves no topological order to induct along. It does not overspend: the ceiling is enforced inside an attempt, not between attempts. Gates are measured against a two-tier held-out mutant corpus. We characterise two classes that let a sound-looking check pass anything: vacuity, satisfied by the absence of the thing checked, and self-attestation, where the subject supplies the value the check is applied to. On a 69-loop catalogue the instrument found 47 vacuous gates in shipped, reviewed code. Against the repaired gates it reports no false accepts over 209 destroying mutants (α≤1.8%, Wilson 95%); that figure is saturation, not quality: freezing the gates and applying a fresh operator family recovers a 23.3% false-accept rate where the exhausted corpus reported none. A rate belongs to a specific gate; the apparatus, not our number, is the contribution. Engine, catalogue and corpus are Apache-2.0.
Figures & tables
Figure 1: One bounded loop. The worker writes only Ωown ; the gate reads the artifact and the anchors, never the worker’s transcript, and the worker’s write to an anchor is refused rather than merely discouraged ( Definitions 3.6 and 3.3 ). The verdict, not the worker, selects the outgoing edge. incapacity is omitted here and treated separately in Figure 4 , because the whole argument of Section 4 is about how narrow that third edge must be.
Figure 2: F1 — a bounded loop, end to end, with the trust boundary drawn. Everything above the controller is declared and readable before the run ( Corollary 5.1 ). Everything inside the dashed region is written by the party under judgement. The two solid paths into the ledger are the only ones that can produce a completion: the gate reads the workspace and records a verdict. The dotted path is the worker’s own account of itself — it is stored, and it reaches no guard in the procedure ( Lemma 7.1 ). The ledger and the receipt sit outside the untrusted region: they are written beside the loop package, not inside the workspace, so an agent cannot edit the record that judges it.
Figure 3: M3 — which facts can decide a completion. Shaded boxes are authored by the party under judgement. Solid arrows are the only inputs any guard in the procedure reads; the worker’s self-report and its transcript reach the ledger and stop there. This is the drift guarantee ( Theorem 7.1 ) as a picture: an agent cannot route to done by asserting it, because no branch consults the assertion. The adversarial test for this claim inverts it — a runner that always claims completion, paired with a gate that always refuses, must reach halt and never done .
Figure 4: The verdict trichotomy of Theorem 4.1 . The single distinguishing test is ownership, read off the loop’s own forbid set rather than inferred from the failure. Every path into incapacity passes through a file the worker was never permitted to write, which is what makes Corollary 4.1 hold.
Figure 5: F2 — one attempt, with every declared bound shown where it is actually enforced. Heavy boxes are the points that can end a run; the annotations name what each reads. Two of the five checks happen before a turn, which is why the ledger flags whether an attempt was spent — without it, a ceiling halt at m writes an (m+1) -th row and utilisation computed from the receipt reads 1.1 for a bound that held exactly ( Definition 13.1 ). The clamp on the worker turn is the one enforcement point that was added last; every other box on this diagram predates it.
Figure 6: F4 — the spend contract on a time axis. The solid box is what the manifest declares. G is dashed because it is the one term outside the declaration: a gate is never cut short, since terminating a check part-way yields no verdict and a check that could not run must never be recorded as having judged. A verdict costing a few seconds past the ceiling is worth strictly more than no verdict, so we pay it and publish it rather than buying a tidier inequality with an unusable outcome.
Figure 9: F3 — two edge kinds, one budget. Solid edges carry data and form a DAG. The dashed edge is a repair : it points backward, and on D ’s failure it returns A and everything reachable from A to pending for another pass. The data graph stays acyclic; the repair relation does not, and that is the whole difficulty ( Definition 3.16 ). On the right is the construction a per-node repair budget admits. P repairs Q , Q repairs P , each decrements only its own counter, and each sees credit remaining after every round — so the run never terminates while every declared bound is respected. One global counter, decremented across the whole graph and never reset at a boundary, is what makes Theorem 5.2 provable, and bounding repairs per node — as every other budget in this system is bounded — is precisely what breaks it. The engine now refuses a plan whose nodes disagree about the budget rather than adopting the first value it finds, because there is no correct way to choose among conflicting global bounds.
Workload
Predicted
Observed
Terminal
U
1
1
1
done
0.1
2
2
2
done
0.2
3
3
3
done
0.3
4
4
4
done
0.4
6
6
6
done
0.6
8
8
8
done
0.8
Table 1: Bound utilisation against a declared ceiling of m=10 . Predicted equals observed in 9 of 9 cases. U rises linearly with workload up to the ceiling and then caps at exactly 1.0 : past the ceiling the run halts rather than borrowing an eleventh attempt.
Productive attempts j⋆
min{m,w+j⋆}
Observed
Attempts saved
0
3
3
7
1
4
4
6
2
5
5
5
4
7
7
3
Table 2: The soft bound with w=3 , m=10 . Predicted equals observed in 4 of 4 cases, and every run halted on no-progress rather than on the hard ceiling. “Attempts saved” is the difference against spending the full declared cap.
Figure 10: Layering. Dependencies point inward and only composition may name a concrete adapter, checked by an AST walk over every module. Below the engine, the receipt log is the single durable artifact and each surface is a view over it, so two surfaces cannot disagree about a run.
Reads as a judgement call
What the gate actually computes
objective is measurable
a numeric target , a non-empty unit , and a deadline matching ˆ\d{4}-\d{2}-\d{2}$
prose is readable
mean words per sentence ≤25
runbook is complete
seven required heading strings are present, and each has content beneath it
privacy policy is complete
six required disclosure phrases occur in the normalised body
Table 3: Requirements that sound as though they need a judge, and the decidable predicate each was reduced to. The reduction is not free and it is not always faithful — the second row is a proxy and nothing more, and the third row’s “ and each has content beneath it” clause is there because the version without it passed a runbook with all seven headings and nothing under any of them ( Section 12.3 ). The claim is not that judgement is unnecessary, but that it belongs in authoring the predicate, where it is written down once and can be audited, rather than in the loop, where it is re-exercised on every attempt and recorded nowhere.
Tier 1
Tier 2
mutants
233
38
destroying (label incorrect )
171
38
preserving (label correct )
62
0
judged
233 / 233
38 / 38
gate errors ( incapacity )
0
0
false accepts α over destroying
0 / 171
0 / 38
Table 4: The held-out mutant corpus after the defects of Sections 12.3 and 12.5 were fixed. Each rate has its own denominator and they are not the same number. α can only be measured on mutants labelled defective; β only on mutants labelled conforming. Reporting both against the full 233 and 38 would imply every mutant was checked for both, and for Tier 2 would assert β=0 over an empty set ( Remark 12.1 ).
Figure 11: Tier-1 coverage by gate kind. Before the fix the corpus resolved only command gates, so every jsonschema , pytest and composite loop produced no verdict and appeared in no count — not as errors, not as exclusions, absent. The guard against unprincipled exclusion inspected only loops already outside the eligible set, and both predicates defining that set read a command gate’s argv, so it was vacuous over exactly the loops that had gone missing. The grey band is the 11 loops excluded for the stated reasons of Section 12.1 .
Direction
Defect
Disclosed?
false accept
data-processing terms: substring match inside a denial
yes
false accept
runbook: required headings present, no content under any
yes
false accept
alt-text: attribute absent, image passes
yes
false accept
citations: pattern derived from the reference set ( Example 8.2 )
dependency pinning: extras and spacing legal under the spec refused
no
Table 5: The six defects found by hand, by direction and by whether the gate’s own documentation disclosed the behaviour. Three of four false accepts were disclosed; neither false reject was. The sample is too small to carry a rate, and the pattern is nonetheless the one we would predict.
loop
how the gate was evaded
test-presence-per-module
a test with no import and no assertion; a test importing a different module; a test asserting on a standalone calculation; renaming the source so the import orphans
nda-required-clauses , gdpr-dpa-terms
the required heading kept, the obligation underneath it negated
pinned to a version that was never released; pinned below the file’s own stated floor
conventional-commits
subject substituted wholesale; a docs change typed build ; an already-conforming line rewritten
secret-scan-keyless
credential split across a concatenation; password renamed to passwd ; the config deleted rather than moved to the environment
Table 6: The 16 Tier-2 defects. Every one satisfies the requirement as literally stated and defeats it in substance — the failure mode a mechanical operator cannot construct, because constructing it requires understanding the purpose.
estimand
anytime-valid
fixed-time
μˉn — mean propensity of the attempts in the log
1.0000
0.9590
population marginal, 1 node pooled
0.8333
0.6067
population marginal, 6 nodes pooled
0.9717
0.8450
population marginal, 30 nodes pooled
0.9983
0.9783
population marginal, heterogeneous ( ρ=3.5 )
0.8267
0.6000
Table 7: Empirical coverage at nominal 95%, by estimand. The sequence is anytime-valid for μˉn ; coverage of a population marginal is a different quantity that rises with the number of independent nodes pooled and falls with their heterogeneity.
loop
gate kind
provider
terminal
attempts to done
wall (s)
citation-existence-check
command
A
done
1
26.6
B
done
1
27.5
C
done
1
54.9
D
done
1
86.6
bug-fix-red-green
pytest
A
done
1
24.3
B
done
1
36.0
Table 8: Cross-model convergence: four independent provider models, four loops, one gate each. Letters are assigned within each loop by ascending wall time and do NOT identify a provider across rows ; letters are not mapped to vendor names because sixteen observations cannot support a product comparison and a named table would invite one. Wall time is reported only to show the arms differ in something while agreeing on everything the gate decides, and must not be read as a per-provider figure. Tokens are unavailable through this path and are not estimated.
Tier 1 (saturated)
E7 (post-freeze)
loops covered
57
54
destroying mutants
171
60
preserving mutants
62
35
gate errors ( incapacity )
0
0
false accepts α
0 / 171
14 / 60 = 23.3%
Wilson 95%
≤2.2%
[14.4%,35.4%]
Table 9: The saturated corpus and the post-freeze corpus against the same frozen gates. The left column is what an exhausted operator set reports; the right is what a fresh one finds behind it. The comparison is the result, not either column. A reader should take from this that a gate suite reporting zero against the corpus that repaired it has established exhaustion and not quality and that the remedy is another operator family, which is cheap, rather than more mutants from the same one, which is free and worthless.
Appendix figures & tables5 assets
Supplementary material from the paper’s appendix.
Appendix
Pattern
n
Verdict is
Choose it when
Schema
10
a document validates against a declared schema
the requirement is about shape , and the schema is the contract a consumer already relies on
Predicate
44
a purpose-built program exits zero
the requirement is about content and reduces to a computation over one artifact
Executable spec
9
a test suite passes
the requirement is behavioural, and the artifact is code that can be exercised
Conjunction
3
every child gate passes
two independent obligations must both hold, or a model judge is being admitted ( Theorem 10.3 )
External tool
2
a third-party analyser reports clean
a mature checker already exists and re-implementing it would be worse
Appendix
Table 10: The five gate patterns the catalogue uses, with the count of loops choosing each. The distribution is itself a finding: two thirds of real requirements were served by a purpose-built predicate over a single artifact, not by a schema and not by a test suite. An author’s instinct to reach for a schema generalises less far than the catalogue suggests it should.
Failure mode
The gate passes because
Evidence
Absence
the artifact it quantifies over is gone, so every universal claim holds
47 instances; Example 8.1
Hollowing
the artifact keeps its structure and loses its content, and the gate checked structure
14 instances; Section 12.12
Self-derived scope
the checker builds its search pattern from its own reference data, so anything outside it is never examined
Example 8.2
Misfiled incapacity
a diagnosis the gate reached was returned as an inability to diagnose, so the loop stopped instead of retrying
84 of 233 mutants; Section 4
Scope blindness
the measurement resolved one gate kind and silently returned nothing for the others
24 loops; Figure 11
Prompt-only obligation
the requirement was stated to the worker and never to the gate
Example 8.1
Appendix
Table 11: Seven ways a gate passes work it should refuse. Four are properties of a gate; rows four, five and seven are properties of the machinery around gates, and we keep them in the same table deliberately, because in this project they cost more evidence than the gate defects did. The counts in the third column are not commensurable: the first five come from instrumented measurement over the catalogue, the last from a release audit whose grade is stated in Remark 9.2 .
domain
gate kind
n
representative requirement
legal / contract
command
9
required clauses present and not negated in the body ; citations resolve against shipped reference data
finance
pytest, command
8
three-way invoice match; a ledger reconciles and no seeded transaction disappeared
clinical
jsonschema
5
a note carries every required field with the stated types
security
command
7
no credential-shaped literal, including across string concatenation and renamed keys
a failing suite goes green; every module has a test that imports it and asserts on what it imported
Appendix
Table 12: Catalogue composition by domain. The count column does not sum to 69, and should not. A loop declares one or more domain tags — 28 of the 69 declare more than one, so the tags total 96 across 24 distinct labels — and the groupings above merge related tags for readability. The authoritative count of loops is 69, obtained from the manifests and pinned by a packaging test; the authoritative partition by gate kind , which is disjoint and does sum to 69, is in Section 12.1 . The requirements in the right-hand column are stated as they are after the fixes of Sections 12.3 and 12.5 .
reason
n
why, and how it is verified
unshipped SDK
4
the runner needs an agent framework the package does not vendor. Probed against the live environment in both directions — a loop claimed excludable that in fact runs fails the check, as does the converse
external tool
3
the gate invokes a security scanner not assumed present
negative requirement
1
the requirement is that an artifact must not acquire a property; a mutation that introduces the property is a conforming input, not a defect, so the operator set cannot construct a labelled defective case
Tier-1 inexpressible
3
the requirement is a relation between artifacts. A single-artifact operator has no notion of consistency across two files. Covered by Tier 2, which found four defects in one of them
Appendix
Table 13: Exclusions. This table is the denominator: every rate in the paper is over 69−12=57 loops.
result
command, and what it pins
E1, E2 — Table 4
uv run pytest tests/evaluation The corpus is a test: a regression in any gate fails the build rather than moving a number in a paper.
Blindness — Theorem 10.1
... test_generator_is_blind.py AST assertion over every generator module.
Tier-2 prompt integrity
... test_tier2_authoring_was_blind.py Recomputes each mutant’s authoring digest from the repository.
E3 — Table 7
... test_reported_interval_estimand.py Includes the three shrink/shift controls that must fail if the interval were vacuous.
Self-improving agent workflows create an audit problem when the same controller can change both its behavior and the conditions under which that behavior is judged. We present GuardrailLoop, a simulation-based testbed that makes three operational contracts jointly testable: preservation of human-defined policy, compute accounting at every recorded execution prefix, and recovery of a specified scientific state after crashes. A hash-pinned policy fixes goals, scope, evaluation identity, budget, and release conditions; machine-directed evolution is restricted to a code-owned feature catalog and bounded knobs. The contribution is an executable boundary and an evaluation protocol that separates useful adaptation, state recovery, and repeated execution. In a paired 50-seed 2 x 2 study, round-stage growth changes target attainment by +1.00 and restricted mean compute to target by -56.97 simulated GPU-hours (95% paired-bootstrap interval [-58.91,-54.70]); idle growth has zero measured utility effect. Across 240 enumerated crash injections, all runs recover the defined outcome, but only 210 preserve the normalized trace: 30 pre-commit crashes repeat a planner call. Resource-drift, kill-switch, integrity, and output-guard matrices satisfy their specified checks. These findings show why successful outcome recovery is insufficient evidence of exactly-once execution. They establish conformance within one calibrated deterministic testbed, rather than general safety or real-world self-improvement.
Qinzhen Ma, Jialin Wu
Rice University · University of California, San Diego
Generate--test--revise loops are common in coding agents, but repetition alone provides no reliability guarantee. We study the gap between finding a correct patch and retaining, verifying, and submitting it. A sealed five-seed study over 30 HumanEval repairs produces 900 three-revision trajectories. Under forced revision, current correctness with current traces falls from 0.820 after one revision to 0.673 after two, although ever-correct rises to 0.847. Two common-state studies use 2,430 branches from identical frozen programs to remove post-treatment risk-set bias. In a prespecified 14B replication, stale traces harm 34/135 correct starts versus 4/135 with current traces, a 22.2-point increase (task-cluster 95% CI [8.9,37.0], exact Holm p=0.0337). A prospective 540-rollout policy eliminates observed correct-start harm but reduces wrong-start repair and fails its joint criterion. Repository experiments over 24 bugs and four coder stacks expose floor effects and component heterogeneity without Holm-significant effects. We therefore separate admission, preservation, grounded certification, competence, and liveness. We derive an evidence-bound typed loop contract and instantiate its mechanically enforceable subset in a reference implementation that binds verifier evidence to exact code states, preserves verified checkpoints, and emits auditable admission receipts. The implementation is an executable specification and conformance artifact, not evidence of improved repair competence or calibrated verifier dependence.
How do you verify a long-horizon agent when its own state and self-reports are exactly what you cannot trust? We present an agent instrument built so that verification is structural rather than post-hoc. A deterministic Executive owns all belief; a language model may only file typed proposals, and a claim is admitted only when a prediction pre-registered before acting is matched against observation by code. Two properties make the instrument a verifier of its own science, not just of the agent: every run invalidates itself when per-organ write-error, render-size, or salted-canary-echo floors are breached (four of the first eight architecture runs were invalidated, each localizing a real defect); and a render-invisible shadow reference compiles the plan the full system would have committed in every ablation cell, so drift metrics are defined even where the mechanism under test has been removed. Using this instrument we report a clean, single-variable result on a failure every long-horizon agent suffers: ablating the commitment mechanism flips goal-abandonment from 0.00 to 1.00 while binding error stays flat at 0.00 (three seeds per cell, up to 394 reference beats per run, every run gated valid). The binding channel, by contrast, does not reappear as per-beat drift when its repair is ablated -- because binding is code-owned, the failure class is structurally absorbed, its only residue appearing one layer upstream as a collapse in hypothesis formation. We report these under full disclosure that task efficacy is null (zero level completions across 52 gated runs on ARC-AGI-3), pre-registered as a structural defeater. The contribution is a verification methodology for agent development and the drift decomposition it makes measurable.