Coding agents can now implement a specification, write and run tests, repair failures, and declare the result ready for release. When the same agentic system produces both the software and the evidence of its correctness, a passing test suite is no longer independent evidence: visible tests become an optimization target, code and tests may share one misinterpretation of the specification, and the builder's own tests may simply be incomplete. This paper argues that agent-produced software requires an assurance plane that is structurally independent of the build plane. We characterize four gaps between stakeholder intent and production (requirement, conformance, evaluation, and model gaps) and identify which of them verification can close. We propose a framework that separates building from verifying, introduces a Verification Contract stating what must be demonstrated before release, and organizes verification in a specification-first phase without access to the implementation and an implementation-aware phase based on mutation analysis, property-based testing, and fuzzing, with an assurance report that leaves the release decision to a human. We evaluate the framework in a pre-registered study on three stateful services, two of them written by third-party models, and an EvalPlus pilot. The builder's programs were correct, but its own tests missed subtle interactions: a verifier in a fresh context detected more of the 46 seeded faults than the builder's tests (Holm-corrected p = 0.006) and surfaced the ambiguities of the specification, at the price of rare false oracles. A verifier from another provider did not add detection.
Figures & tables
Gap
Between
Treatment in the framework
Requirement
R and S
Human approval of the Verification Contract; Phase A reports ambiguities and contradictions in S
Conformance
S and P
Phase A and Phase B evidence
Evaluation
Tv and S
Assurance artifacts are withheld from the builder
Model
W and production
Runtime evidence revises the contract
TABLE I: Four gaps between stakeholder intent and production behavior
Fig. 1: Overview of the framework. The build plane produces the program; the assurance plane produces evidence about it. The builder receives counterexamples but never the assurance artifacts or fixes. Gaps from Table I are shown in italics.
ID
Evidence by
S
Tv
P
Verifier model
SV
Builder
✓
✓
✓
n/a
A
Verifier, Phase A
✓
same as builder
B
Verifier, Phase B
✓
✓
same as builder
AB
Verifier, Phase A, Phase B
✓
after Phase A
same as builder
AB ′
Verifier, Phase A, Phase B
✓
after Phase A
other provider
TABLE II: Experimental conditions. S : specification; Tv : visible tests; P : implementation.
Service
Author of S , Th , faults
Req.
Faults
Th tests
Documents and payments
the authors
10
14
39
Room booking
Mistral Medium 3.5
10
17
27
Equipment loans
Qwen 3.7-Plus
10
15
27
TABLE III: Services of the main campaign
Seeded faults detected
Tests failing on the reference
Cond.
Documents
Booking
Loans
All
As measured
Genuine
Mut.
Tokens
Detected, rescored
SV
77.1
84.7
93.3
85.1
0.6
0.6
95.2
0.0k
196/230
A
84.3
94.1
93.3
90.6
11.4
1.9
96.3
67.4k
216/230
B
91.4
96.5
93.3
93.7
10.8
1.0
96.0
76.4k
219/230
AB
92.9
100.0
93.3
95.4
8.9
0.7
99.3
125.9k
221/230
AB ′
72.9
91.8
90.7
85.1
7.0
2.3
96.6
69.8k
200/230
TABLE IV: Evidence per condition. Seeded faults detected (%, mean over 5 runs) per service and pooled; invalid tests as measured and genuine false oracles (% of tests, all services); mutation score (%, median over services); tokens per unit, excluding the shared builder phase (median over services)
Software development follows an implementation-verification loop in which developers or agents iteratively revise an implementation until an evaluator, such as a test suite, accepts it. The evaluator checks the implementation against a set of requirements under a model of the deployment environment. Yet even a formal proof that the implementation satisfies the requirements under the model cannot guarantee acceptable behavior after deployment. Requirements only approximate stakeholder intent, and the model only approximates the real deployment environment. We call these together - requirement gap and model gap - the two-gap framework, which unifies the main failure modes of agentic software engineer-ing: reward hacking exploits omissions in the requirements or model, while hallucination widens the gaps by fabricating requirements or environment assumptions. Because neither gap can generally be certified closed in an open, changing world, the goal shifts from closing them to continuously narrowing them. We therefore propose an assurance-revision loop that uses deployment evidence to revise the requirements, model, or evaluator when stakeholders reject the resulting behavior. We then cast assured agentic development as a resource-allocation problem over human judgment, agent capability, and compute. The two principal bottlenecks mirror the two gaps: human judgment for the requirement gap and faithful, costly evaluation for the model gap. Reality remains the final verifier: acceptable behavior under actual deployment conditions is the ultimate test, while predeployment evaluations remain proxies for it.
Alexander Krentsel, Shubham Agarwal, Mert Cemri +5
Reusable Web-agent verification requires a rule to follow changing requirements and support subsequent execution. We introduce AgentProofBench, which connects paired tests of a frozen acceptance rule to execution from identical saved openings. The resource spans 97 tasks, 79 families, and four Web services. Experiments with DeepSeek Flash/Pro establish two linked measurements. Across 48 families, complete-panel and decision-replay tests retain 82/96 Flash and 79/96 Pro source programs; paired reuse-rebuild BA intervals are [-5.47, 1.57] and [-10.16, 0.00] percentage points. Across 22 execution families, deployment-state panel correctness separates program assignments whose two saved openings are both delivered correctly: 32/33 assignments with error-free panels, versus 1/11 with panel errors. All reference-defined program-gate regressions and withheld deliveries occur in the latter group. Neutral continuation attains the highest correct delivery under the tested generic feedback, providing a concrete baseline for measuring the value added by a gate. Released instructions, states, programs, reference rules, and trajectories connect each test failure to its execution consequences. AgentProofBench makes reusable verification assessable at both the requirement and policy levels.
Multi-step enterprise agent tasks fail in a characteristic way: single-pass inference has no checkpoint between deciding an answer and committing to it. We study one production system (Leni) whose architecture installs such checkpoints: verification loops (execute, observe, compare, correct) staffed by lightweight task-specialized post-trained models. We evaluate the unmodified production configuration on three public benchmarks stressing distinct failure modes: SpreadsheetBench Verified (silent computation error), BullshitBench v2 (premise confabulation), and the GAIA validation split (cascade error over long tool chains). The full system improves over its frontier base model by +11.0 percentage points on SpreadsheetBench (91.25% vs 80.25%, n=400, p<0.001), +7 to +10 percentage points on BullshitBench (98% vs 91%, n=100), and roughly +15 points on GAIA validation (75.2% pass@1, n=165; 83.0% best-of-k). Our central contribution is a decomposition of that uplift: most of it comes from scaffolding, routing, and specialist models rather than from the verification step itself, whose isolated contribution is small (+1.5 points) but concentrated at the top of the score distribution, where it converts otherwise-failing tasks. We instrument the loop end-to-end, yielding an empirical verifier confusion matrix (catch rate about 0.20, fix rate 0.75, no false-alarm regressions) that grounds a compounding-reliability model. Specialist-swap ablations suggest that the loop's value depends on who observes it: replacing the small trained verifier with the generating frontier model eliminates most rescues. A valid-premise control shows zero over-rejections in 100 expert-level questions.