Independent Assurance Plane

Sources#

• Who Verifies the Builder? Toward Independent Assurance for Agent-Produced Software

Summary#

When one agent writes the code, writes the tests, picks the expected outputs and declares the change ready, the green suite is the producer certifying itself. Sion Israel Sion & Alain April (École de technologie supérieure, Montréal, arXiv 2610.28667, 2026-10-16, empirical) take the old IV&V answer, that the producer cannot be the sole authority on correctness (Myers; IEEE Std 1012; DO-178C), and rebuild it for coding agents. They separate a build plane from an assurance plane and test the separation in a pre-registered study. It is the release-gate form of Optimizer–Evaluator Decoupling: the thing that built the program does not produce the evidence that it may ship.

The study's most useful result is the failure mode it actually found. The builder (Claude Sonnet 5.5) wrote correct programs in every unit, so the reason its tests fell short was neither gaming nor a shared misreading. It was incomplete self-evidence: the builder implemented a subtle interaction correctly and never tested it, so a later change that broke it would have passed.

Evidence note. empirical, tier kept. The two confirmatory hypotheses, the models, the budgets and hashes of every frozen file were registered before the main campaign, and an artifact with prompts, evidence and a deviation log is public (github.com/besionisrael/assure-harness). The weaknesses are the paper's own. The effect rests on few informative faults (12 non-tied for H1 out of 46). One of three services was written by the authors and revised after a pilot. The other two were written and reviewed by LLMs, not humans. There is one builder model and one alternative-verifier pair. The harness had a defect that silently failed parametrized tests. Not peer-reviewed. No vendor COI.

Four gaps, and which ones verification can close#

The paper splits the distance from stakeholder intent to production behaviour into four gaps (Table I, checked against pdftotext):

Verification against the spec closes only the conformance gap, and withholding closes the evaluation gap. The requirement and model gaps are about whether S and W are the right things to verify against, so the framework assigns them to human approval and to runtime feedback and does not claim to close them.

Self-validation can fail in three ways (§III). (1) Tests become rewards. Once passing T_v ends the loop, any program in the much larger set that passes T_v will do, which is the grader-gaming and SpecBench/ImpossibleBench failure. (2) Consistency is not correctness. Code and tests built from the same misreading Ŝ agree and are wrong together, which is Knight & Leveson's common-mode failure. (3) Incomplete self-evidence. Even when Ŝ = S, the builder tests only what it thought of. Only the third showed up in the study.

The framework#

Three roles. The builder produces P, the verifier produces evidence about P against S, and the human approves what must be demonstrated and decides whether the evidence suffices. Five principles govern them:

• P1 No self-certification. Build-plane artifacts, including the builder's tests, never count as evidence on their own.
• P2 Information asymmetry. The builder receives only reproducible counterexamples, never the assurance tests, so the assurance suite cannot become the new reward surface.
• P3 Specification before code. Phase A evidence is derived and frozen before the verifier sees P.
• P4 Verify, do not repair. "A verifier that repairs becomes a second builder and inherits the builder's incentives."
• P5 Explicit residual uncertainty. Evidence is reported per requirement with what was not verified, and the release decision stays human.

Independence is adapted from IEEE 1012's three dimensions: technical (the verifier shares neither context nor artifacts and may use a different model), managerial (the builder's orchestration loop does not invoke, configure or terminate the verifier) and incentive (the verifier is not rewarded for a green pipeline). That third axis, the counterpart of financial independence, is one the corpus's reviewer-independence vocabulary in Optimizer–Evaluator Decoupling did not yet name.

The Verification Contract. A spec says what the system must do. The contract says what must be demonstrated before acceptance: for each requirement, falsifiable guarantees and the evidence (technique and threshold) behind each. Fig. 2's excerpt for REQ-17 ("a user can read only the documents they own") lists four guarantees, then evidence E17.a–c (stateful property tests over request sequences, fuzzing of document identifiers, "mutants of authorization checks: all killed"), then an open question, "may an administrator read all documents?". It is fixed and approved before any implementation exists, so the builder cannot shape the claims afterwards. Its size grows with requirements and risks, not with code, which is the paper's answer to review capacity in Verification as the New Bottleneck. An agent may draft it, but approval is human, and unresolved ambiguities in S are recorded as open questions rather than resolved silently.

Phase A, specification-first. The verifier gets S, the contract and the public interface, but not the body of P. It writes properties, invariants, forbidden scenarios (pay twice, refund a payment never captured), model-based tests over operation sequences, and acceptance tests. These are frozen before Phase B. The risk is a false oracle that encodes the verifier's own misreading, and the study measures it.

Phase B, implementation-aware. The verifier gains read-only access to P. It cannot alter Phase A artifacts but adds evidence aimed at the code: mutation analysis with tests for surviving mutants (MuTAP, Meta's ACH), fuzzing at boundaries the code reveals, property tests for internal and error paths, and metamorphic or differential relations where no exact oracle exists. This is the stage Reviving Impractical Quality Tools says agents made affordable. Phase A asks whether P does what S requires. Phase B asks whether the evidence would notice if P were wrong.

Counterexample loop and report. A violation goes back as a minimal reproducible counterexample (input sequence, observed behaviour, violated guarantee), never the test, the property or a fix, and the loop is bounded. The output is an assurance report per requirement (verified / partially verified / violated / not verified, with technique, strength such as mutation score, and unverified scope like "concurrent retries across replicas"). It deliberately has no aggregate trust score, "because no empirical basis currently exists for combining heterogeneous evidence into one number." Production incidents that contradict W become new guarantees, so assurance runs beside construction and continues after release.

The study#

Design. An EvalPlus pilot (20 HumanEval+/MBPP+ tasks) was dropped as the main subject because the builder solved 19. The main campaign used three stateful Python services, each with a 10-requirement natural-language spec, a small visible suite, a hidden suite and seeded faults. Every seeded fault is a one-edit change that passes T_v and fails T_h:

A fourth service, by Gemini 3, was dropped when its correction rounds did not converge. The builder first gets S and T_v, writes P₀ and its own tests T_b, and iterates up to five rounds. That P₀ is the shared start of every condition:

• SV: the builder's own tests are the evidence.
• A: a fresh-context verifier gets S and the class name only.
• B: a fresh-context verifier gets S and read-only P₀.
• AB: Phase A, then Phase B.
• AB′: AB with a verifier from another provider.

In B, AB and AB′ the verifier also receives up to six mutants of P₀ that survive its tests and may add tests to kill them. Counterexamples go back for at most 3 rounds, and the builder may reject one that contradicts S. Builder and same-model verifier are Claude Sonnet 5.5, and the alternative verifier is GPT-5.5 (gpt-5.5-2026-04-23). There were 5 runs per service, 15 units, 270 model calls and 5.8M tokens. The unit of analysis is the seeded fault, tested with an exact two-sided sign test with ties dropped, and H1 and H2 form one Holm family.

RQ1, the evaluation gap: none observed. The builder's final program passed T_v ∪ T_h in all 15 units in every condition. The only pilot gap (10 points on MBPP+) was one task, Mbpp/753, whose hidden tests demand behaviour the spec does not fix. So every fault analysed below is seeded.

RQ2, context-level independence (H1, confirmatory): yes.

(Table IV, one value per cell, reconciled against pdftotext.) Per fault, 11 favour AB, 1 favours SV and 34 tie (p_Holm = 0.006). On the two third-party services alone it is 7–0 (p = 0.016), but all seven come from booking. On loans, SV, A, B and AB caught the same 14 of 15 faults in every run. The separating faults share one pattern. On documents, SV never caught the two faults that bind idempotency keys or pagination cursors to the session instead of the user (0 of 10 fault-runs), and AB caught them in 6 of 10. The builder had implemented the user binding correctly every time and simply never tested it.

RQ2, model-level independence (H2, confirmatory): the other provider was worse. 13 faults favour AB, 0 favour AB′ and 33 tie (p_Holm = 0.0005). AB′ ties SV at 85.1% pooled and is below it on documents (72.9 vs 77.1). The paper notes that with one model pair, provider and capability are confounded.

The harness defect, and what it did. After the runs the authors found their harness called every test function without arguments, so every pytest.mark.parametrize test raised TypeError on every program, including the reference. That accounts for 282 of the 323 verifier tests first counted as invalid. Measured invalid rates of 7–11% fall to 0.7–2.3% genuine false oracles. The defective tests were excluded from detection, so H1/H2 are conservative for the verifiers. An exploratory rescoring with them run and no new model calls makes both stronger: H1 11–0 (p = 0.001), H2 10–0 (p = 0.002), and 196, 221 and 200 detected of 230 fault-runs for SV, AB and AB′.

RQ3, the two phases. Within AB, Phase A alone caught 27 (fault, run) pairs, Phase B alone 7, and both 186. Within AB′ the split was 78, 13 and 106. Spec-first carries most of the detection, and implementation-aware adds a smaller distinct set. Phase A is also where ambiguity surfaces. It raised at least one open question in 91.1% of task runs. Of the five points the authors deliberately left open in the documents spec, it raised case-insensitivity beyond ASCII (4/5 runs in A, 3/5 in AB) and empty idempotency keys (3/5 in A, 5/5 in AB). SV, B and AB′ never raised either. No condition raised the administrator-role question that Fig. 2 uses as its example.

RQ4, the release gate: cost measurable, recall not. Every final program was correct, so the only measurable quantity is how often the gate blocks a correct program. On raw evidence it did so in 14 of 15 units for AB, 13 for A, 11 for B, 4 for AB′ and 0 for SV. With the parametrized tests run, AB drops to 8, A and B to 6, and AB′ to 0. On valid tests only, it blocked twice, both AB on documents, both from tests requiring passwords of unencodable characters to be accepted. The spec leaves that open and the reference happens to accept it. No final program became incorrect in any condition, even though builders received counterexamples from invalid tests. One builder diagnosed the harness bug itself ("each is a TypeError raised because the verifier's own parametrized test functions were called without their arguments") and kept its code.

What it supports, and what it does not#

The builder's tests are development artifacts, not release evidence. This is the practical claim (P1), and the H1 result supports it in the mildest setting available: a strong builder, precise specs and no overfitting, where the builder's suite still missed faults a separate verifier caught. It sits beside the corpus's measurements of agent tests that reach too little of the diff (Agent-Generated Test Quality). There, tests are absent or untargeted. Here they are present, pass and were written by a builder that got the code right, and they still under-constrain it.

What "fresh context" bought here is not a /clear (wiki reading). SV is the builder's own tests, written while building. AB is a different role with a different job (writing evidence from the spec), withheld code in Phase A, surviving mutants handed to it in Phase B, and ~126k extra tokens per unit that SV never got. No arm gives the builder in its own context the same budget and the same mutants. So H1 shows that the separated verifier role, as configured, beats the builder's self-chosen suite. It does not isolate context separation from extra verification effort or from mutation guidance. Mutation guidance is a technique, and Martin runs it inside one agent's loop. A, which gets neither code nor mutants, is the cleanest independence arm: 90.6% against 85.1% at 67k tokens, exploratory and untested. This is why the result does not contradict Song, where a same-model reviewer in a fresh session was only 1.5pp (ns) above same-session self-review. Song's contrast is a context reset on the same review task. Sion & April's is a role and information separation plus effort.

Model diversity: a third instrument, and this time the sign is negative. Greptile finds the cross-family reviewer catches more on natural bugs (case-study). Song finds a cross-model single review not significantly different from a fresh same-model one, but a mixed pair beating a doubled same-model pair. Here a single cross-provider verifier is significantly worse (13–0). These do not conflict on the record, but they narrow the claim. Nothing here tests a union of Sonnet and GPT-5.5 evidence, which is the one configuration where Song found a gain. All three instruments confound lineage with capability or effort somewhere. AB′ spent less (69.8k vs 125.9k tokens) and blocked far less (4 raw blocks vs 14), which looks like a less thorough verifier rather than a blind-spot effect. Read with Cross-Model Error Entanglement, "route to another vendor" is not yet a measured improvement for single-verifier test generation.

The assurance infrastructure is part of what must be verified. The study's largest error source was its own harness, which reported unexecutable evidence as failing and was exposed only when a builder disputed the counterexamples. The authors' lesson is that a harness should reject evidence it cannot execute rather than report it as failing. This is the Trace-Detector Measurement Validity (Silent Tool-Output Override) point about verdicts as measurements, and the reason the paper insists the human see disputed counterexamples rather than a bare BLOCK. A gate that only says "block" would have shipped 14 false blocks out of 15.

Where human control moves. The framework moves control from code to three artifacts whose size does not grow with code: the contract (before), the counterexamples (during) and the report (at release). This is a sharper specification of the human layer in Layered Supervision. Approving the contract is a judgment that S captures R, and accepting a "not verified" item is a judgment about W, and neither can be delegated to the builder without reintroducing self-certification. Evidence strength should also scale with risk, as DO-178C software levels do: killed mutants on every access check for an authorization requirement, and example tests for a formatting utility. That is the same partition Risk-Tiered Auto-Approval draws on the merge side.

A spec-first phase, but not up-front design. The paper's opening frame is that spec-driven development "returns control to the human at the beginning of the chain" but "does not address the end." Martin's objection is to big design up front as the source of the code. The contract is up front too, but it is a statement of what must be demonstrated, approved before building and revised by runtime evidence. Phase A's value here was less in catching faults than in turning silent spec ambiguity into explicit open questions, which only the separated, code-blind verifier did.

What it leaves unmeasured. The first two failure modes (overfitting T_v, shared misreading) were not observed, because the builder never failed. Release-gate recall is unmeasured for the same reason. The authors attribute the ceiling to a strong builder on small precise tasks and leave tasks where the builder fails to future work. A user study of whether an assurance report calibrates human release decisions better than CI results is named but not run.

Connections#

• Optimizer–Evaluator Decoupling — the parent rule applied at the release gate, with an empirical test. It adds incentive independence (a verifier rewarded for a green pipeline has the builder's incentive) and managerial independence (the builder's loop must not invoke or terminate the verifier) to that page's axes, and a measured single-pair result on the lineage axis
• Cross-Model Review Complementarity — the review-side controlled experiment. Song's context reset is ~0 and his mixed pair helps. Here a separated verifier role helps and a single cross-provider verifier hurts. The contrasts differ (reset vs role separation, union vs single), and both confound capability
• Same-Model Review Blindness — the lineage claim this study's H2 runs against in sign, for test generation by a single verifier on seeded faults
• Cross-Model Error Entanglement — Knight & Leveson's correlated failure, the paper's own reason why nominal independence is not statistical independence, and the backdrop for reading H2
• ExecCritic: Learn to Test, Test to Improve — the same split of test construction from repair, trained rather than prompted. ExecCritic freezes a qualified test and lets Repair see only its feedback. Here only counterexamples cross (P2) and the verifier never repairs (P4). ExecCritic finds bad tests make repair worse. Here invalid counterexamples did not, because a strong builder could reject the ones that contradicted the spec
• Agent-Generated Test Quality — incomplete self-evidence measured under control: the builder's tests pass, its code is correct, and the suite still misses faults in behaviour it never exercised
• Reviving Impractical Quality Tools — Phase B is the mutation-analysis-plus-fuzzing stage, with mutants handed to the verifier to kill. Its unique contribution here was small (7 of 220 (fault, run) detections in AB)
• Layered Supervision — the human layer specified: contract, counterexamples and report as the three artifacts the human reviews instead of code
• Spec-Driven Development as the New Waterfall — spec-driven development controls what gets built, and the contract controls what may ship. Phase A is spec-first verification, not spec-first construction
• Risk-Tiered Auto-Approval — evidence strength scaled by requirement risk, the release-gate counterpart of risk-tiered merge approval
• Trace-Detector Measurement Validity (Silent Tool-Output Override) — the harness defect as a verdict that was a measurement artifact, caught only because the builder disputed it
• Verification as the New Bottleneck — an assurance artifact whose size tracks requirements, not code, as the answer to review capacity
• Evaluation Awareness & Grader Gaming — the "tests become rewards" failure mode that information asymmetry (P2) is built against, which this study did not observe
• Proof-Gated Agent Patching (Patch the Planet's Regression Audit) — a deployed relative built by a patch author. Trail of Bits' pipeline has fresh-context replay, independent validate and prove agents, and a fail-closed "inconclusive without a live PoC" rule, but one vendor, model and organization runs both build and proof, so only context independence is present

Open Questions#

• Does the fresh-context verifier's edge over the builder's own tests survive a compute- and technique-matched control? AB spent ~126k extra tokens and received surviving mutants that SV never got. An arm where the builder, in its own context, gets the same token budget and the same six mutants to extend T_b would separate role independence from verification effort. Settler: that arm added to the released assure-harness on the same 46 faults.
• Does the assurance plane catch the first two failure modes when the builder actually fails? Here the builder was correct in every unit, so overfitting, shared misreading and release-gate recall went unmeasured. Settler: the same five conditions on tasks with a nonzero builder failure rate (e.g. SpecBench's held-out composition tasks or ImpossibleBench), reporting block-verdict recall on valid tests.

Sources#

• Who Verifies the Builder? Toward Independent Assurance for Agent-Produced Software — Sion Israel Sion & Alain April (École de technologie supérieure, Montréal), Who Verifies the Builder? Toward Independent Assurance for Agent-Produced Software, arXiv 2610.28667, 2026-10-16, 10 pp, empirical, tier kept. Sections used: abstract, §I–IV (gaps, principles, contract, phases, report), §V (design, conditions, metrics, pre-registered analysis), §VI (all four RQs, the harness defect and rescoring), §VII–IX. Fig. 2 (contract and report excerpt) was viewed. Fig. 1 is the plane diagram described in prose. Parse note: PDF-derived (docling 2.126.0 / docling-mlx 0.1.1, confidence excellent). verify flagged table-collapse on two tables. Table I (gaps) parsed correctly, and its four rows match pdftotext -layout. Table II (conditions) is collapsed in the raw: all five rows are merged into one grid row, and the T_v column header is lost. It was recovered from pdftotext -layout (SV: S, T_v, P; A: S only; B: S, P; AB and AB′: S, P after Phase A; verifier same as builder except AB′, other provider), and the recovery matches the §V-C prose. Tables III and IV have one value per cell and were checked against pdftotext, with no discrepancy.