Spec-First Verification: What Zero-Finding Passes Prove

In Brief

A self-reported but fully instrumented case study describes an agent dismantling a core invariant across 189 files of a 717,725-line codebase with no human code review, declaring convergence at two consecutive zero-finding audit passes against a frozen specification — a criterion that establishes agreement with the spec, not correctness of the spec.
The case’s own data cautions against reading a zero-finding pass as absence of defects: verification cycle 15 surfaced ten findings after five near-quiet cycles, so a zero measures one probabilistic auditor’s recall on one pass.
SpecPath finds that agents handed contract-equivalent specifications through different revision histories keep nearly identical aggregate accuracy while 35 of 100 direct-success blocks fail on at least one equivalent history — a result from a five-task diagnostic suite, not a prevalence estimate.
RETRACE’s full reconstruct-and-reconcile pipeline gains 3.6–7.0 Pass@1 points and beats plain self-review on both scaffolds tested — but plain self-review itself loses 1.4–1.8 points on one scaffold while gaining on the other, and the ablation shows the issue-visible and issue-withheld passes contributing equally, so the claim that verification independence comes from withholding the referent is asserted by these papers, not isolated.
Three risk channels sit outside every spec-referenced audit — spec-versus-intent defects, behavior the spec never constrains, and weak agent-authored test oracles — and those channels, not diff reading, are where human attention still has no substitute.

Why This Matters

The argument for spec-driven development has always had a strongest form: a sufficiently precise specification can replace human review of generated code. Through mid-2026 that form was argued, not run: the production-scale executions the case study surveys shipped anchored to pre-existing test oracles, and its author reports no directly comparable case — an absence he explicitly scopes to his own knowledge (arXiv 2608.12440). Now there is a documented execution with no such oracle — three days, $2,430, 189 files, no human ever reading the diff — and two research results, both unrefereed August 2026 preprints, that mark exactly where its verification logic is thinner than it looks. Teams deciding how much review to delete are making an epistemics call whether they name it or not: every check in the spec-first stack proves agreement with a constructed referent, and the failure modes that remain live are the ones no agreement check can reach. Sorting covered risk from uncovered risk is now possible with actual numbers attached.

Key Findings

Number	What it measures	Source
≈201	Defects, ambiguities, and deviations corrected across 31 audit passes before any human ran the code	arXiv 2608.12440
110 → 160 → 189	Files in spec scope at first draft → at freeze → files the change actually touched	arXiv 2608.12440
$2,430 / 3 days	Inference cost and elapsed time for the full protocol	arXiv 2608.12440
78.8% vs 78.7%	Final-contract realization, direct condition vs mean of four contract-equivalent histories	arXiv 2608.09799
35 / 100	Direct-success blocks that fail on at least one contract-equivalent history	arXiv 2608.09799
18.3%	Conditional path violation under duplicate — inert repetition, the largest observed estimate (the authors mark condition rankings exploratory)	arXiv 2608.09799
+7.0 vs −1.4	Pass@1 change from RETRACE vs Self-Refine on the mini-SWE-agent scaffold, GPT-5-mini (Self-Refine gains on the OpenHands scaffold)	arXiv 2608.08950
80.2%	Agent-authored test patches carrying weak or no explicit oracle signals	arXiv 2606.18168

A 189-file migration converged on spec agreement alone — and the paper scopes its own claim

Joël Abenhaïm’s case study documents one execution of a specification-first protocol on his own 717,725-line TypeScript application: removing the guarantee that a UI panel stays open for the duration of an AI request, so a streaming generation survives its panel closing and reattaches on reopen (arXiv 2608.12440). The protocol ran five phases, each in a separate session: ideate, specify, refine, code, verify.

The agent wrote a formal specification, re-audited it against the source code across 14 refinement cycles, implemented atomically, then audited the code against the now-frozen specification across 17 verification cycles. Across those 31 audit passes, approximately 201 defects, ambiguities, and architectural deviations were corrected before any human executed the program. One measurement caveat travels with that count: a log-recovery gap left some refinement cycles’ correction lists unrecoverable — the paper records each such cycle “as an estimate of five” — which is why its specification-side subtotal is approximately 85, not an exact figure.

The stopping rule is the detail everything else rests on. Convergence was declared at “two consecutive verification passes returning zero findings,” met at cycles 16 and 17 — and the paper states the criterion was empirical rather than fixed in advance (arXiv 2608.12440). First manual execution came after cycle 17. The specified behavior worked, the pre-existing unit suite showed no regression, and roughly thirty subsequent sessions surfaced no bug.

Two scope corrections keep the headline honest. “No test oracle” means no oracle for the new behavior: the target behavior had not existed before, so no pre-existing suite could encode it — while the old suite still ran as a regression oracle, and the agent wrote tests under a standing instruction.

The report is also candid about its own evidentiary weight: single case, single operator, self-reported by the author of both the codebase and the agent product. The “no bug observed” claim is scoped as observed behavior — in the paper’s words, “not a proof of absence of latent defects, which no test campaign or usage window of any length establishes” (arXiv 2608.12440). The published 1,500+ pages of session logs — in French — make the process inspectable; they do not make the reporting independent.

Zero findings measures the auditor, not the code

Read as an epistemic instrument, each verification pass is a probabilistic audit: a fresh session of the same agent, comparing code against the frozen document, reporting the disagreements it can find. A zero-finding pass therefore establishes that this auditor, on this pass, detected nothing — a statement about recall, not about the code.

The case’s own finding series makes the distinction concrete. Verification corrections ran 10, 12, 9, 21, 2, 7, 8, 13, 6, 3, 3, 4, 4, 4 — and then cycle 15 surfaced ten findings after five cycles of three or four (arXiv 2608.12440). A series that quiet can still spike. Two consecutive zeros is a reasonable engineering heuristic; it is not a confidence bound, and the paper does not present it as one.

The same logic applies one layer up, where it bites harder. The specification itself was authored by the agent and refined by auditing it against the source code — the referent converged when the agent stopped disagreeing with itself, after roughly 85 corrections and a scope that grew from 110 to 160 files as unnoticed dependencies surfaced (arXiv 2608.12440). The implementation then touched 189. Refinement stopped at a single zero-finding cycle, a weaker bar than the two verification required. Whether the frozen spec matched the operator’s intent was checked by exactly one mechanism: the operator skimming the 55-page document. Every automated loop in the protocol checks agreement between the system’s own artifacts: verification compares agent-written code against the agent-authored spec, and refinement audits that spec against a pre-existing codebase whose same-methodology authorship is, per the paper’s own limitations, the author’s declaration rather than an instrumented fact.

Neither loop consults a referent from outside the system — code is audited against the agent-authored spec, and the spec against the pre-existing codebase — while spec-versus-intent fidelity, unspecified behavior, and per-pass auditor recall sit outside both — adapted from arXiv 2608.12440.

None of this makes the result hollow. Catching roughly 201 defects, ambiguities, and deviations before first execution for $2,430 is the demonstrated value (arXiv 2608.12440), and the protocol’s discipline (frozen referent, fresh sessions, atomic implementation) is the paper’s account of why repetition converged instead of drifting. The point is narrower: convergence certifies spec-agreement to the recall limit of the auditing process.

Work on quantifying exactly that limit exists. Fidelity probes score a specification against code by generated question-answer pairs, decomposing disagreement into contradiction and coverage-gap rates (arXiv 2605.17246). Nothing of the kind instruments this case: its audit trail records what was found, never what the finder could see.

The same contract, stated differently, is a different input

SpecPath attacks the referent from another side: even holding the final specification’s meaning fixed, the path by which it was stated changes what agents build. The framing question is whether agents “resolve the active specification, or merely follow the most salient path by which it was stated” (arXiv 2608.09799).

The design holds repository, final contract, verifier, agent configuration, and budget fixed while varying only the revision history — direct statement, duplicated turns, split turns, an explicit override of an earlier rule, an explicit cancellation — across five task families derived from real merged PRs, seven models, and two scaffolds.

The aggregate looks reassuring and the pairing does not. Final-contract realization is 78.8% for the direct condition and 78.7% averaged over the four contract-equivalent histories — but 35 of the 100 complete blocks that succeed on the direct statement fail on at least one equivalent history, for a task-macro conditional-path-violation rate of 36.4% (arXiv 2608.09799). Gains and losses cancel in the mean, so condition-level accuracy hides which executions changed identity. The authors state the boundary as plainly as the result: “implementation success on a consolidated request does not guarantee specification-path invariance.”

The distribution across conditions resists a ranking. Duplicate — inert repetition, no revision semantics at all — shows the largest observed violation estimate at 18.3%, against cancellation’s 14.1%, split’s 12.2%, and override’s 10.8% (arXiv 2608.09799) — but the authors disclaim the ordering: “the ordering changes across repeats; individual operator rankings are therefore exploratory.” What the spread does support is that path sensitivity is a family of presentation effects rather than a single stale-memory bug, and the paper declines to name a mechanism. The claim is also carefully bounded: five curated families, 127 complete blocks, controls whose confidence intervals include zero. It is a diagnostic demonstration, not a prevalence estimate for software work generally.

For spec-first practice the implication runs in two directions. The convergence protocol above hands its agents what SpecPath calls the direct condition: freezing the spec consolidates it, so implementation and verification see one settled document rather than a revision trail. SpecPath’s headline caution is aimed at exactly that condition — consolidated success does not guarantee path invariance — but a workflow that only ever presents the settled document at least avoids importing the history-variance the paper measures.

But any workflow that hands an agent the living history of an evolving spec — issue threads, review comments, superseded drafts in context — inherits the measured risk that a directly-competent configuration fails on an equivalent restatement. SpecPath’s suggested fix, an explicit contract ledger tracking each requirement’s status before code is written, remains a hypothesis the paper itself flags as untested.

Reconstruct-and-reconcile beats plain self-review — but the ablation does not isolate why

The third result tests what a second check adds. RETRACE verifies a coding agent’s patch by reconstruction in both directions: a forward pass builds the repair rationale from the issue and trajectory, and a backward pass infers — from the patch and trajectory alone, with the original issue withheld — a description of the problem the patch appears to solve, then reconciles the two against the original issue (arXiv 2608.08950). On SWE-bench Verified it lifts Pass@1 from 56.2% to 63.2% with GPT-5-mini and 75.8% to 79.4% with MiniMax M2.5; on a second scaffold, OpenHands, measured on a 120-issue subset, it adds 19.2 and 7.5 points (arXiv 2608.08950).

The Self-Refine control is scaffold-dependent, and that dependence bounds what the comparison proves. Self-Refine (the same model reviewing its patch against the same issue with comparable budget) reduced Pass@1 by 1.4 and 1.8 points on the primary scaffold — yet gained 15.8 and 1.7 points on OpenHands; the paper states it plainly: “Self-Refine also improves over the OpenHands baseline on both models, unlike on mini-SWE-agent, where it slightly degrades performance” (arXiv 2608.08950). Where self-review does degrade, that echoes the older finding — stated for reasoning tasks — that “LLMs struggle to self-correct their responses without external feedback, and at times, their performance even degrades after self-correction” (arXiv 2310.01798). The durable result is narrower: RETRACE outperforms Self-Refine on both scaffolds.

What RETRACE changes is not the reviewer. The paper concedes both directions “rely on the same backbone model that generated the patch” — what changes is the structure of the check. The backward pass cannot see the issue, so its reconstruction is evidence about the patch rather than an echo of the prompt; the forward pass sees everything and re-derives the repair rationale; reconciliation compares both against the original issue.

RETRACE reconciles a forward repair rationale against a backward reconstruction made with the issue withheld; both passes run on the backbone model that wrote the patch — adapted from arXiv 2608.08950.

Three designs point at the same idea — though not independently, and not by the same mechanism. Anthropic’s loop-engineering guidance recommends a separate reviewing agent because “a reviewer with fresh context is less biased and not influenced by the main agent’s reasoning” (Anthropic). The case study cites that guidance directly and positions its protocol as applying the principle differently — same model, different anchor: “The separation this protocol relies on is in that referent, not in the identity of the reviewer” (arXiv 2608.12440).

RETRACE’s own ablation, though, does not isolate the referent as the active ingredient. On a 120-issue subset, the issue-visible forward pass and the issue-withheld backward pass score identically — 56.7% each against a 50.0% baseline — while rescuing different failures, and reconciling both reaches 60.8% (arXiv 2608.08950). The paper credits complementarity, with the gain coming “not only from additional inference but from the independent verification signal that reconciliation provides.”

What the three share is structural: each check is arranged so the checker cannot simply echo the interpretation that produced the artifact — a fresh-context reviewer, a frozen referent, a reconstruction with the issue withheld. Fresh context itself is not common ground: Anthropic’s guidance prescribes it and the case study’s separate sessions practice it, but RETRACE’s passes consume the original trajectory. Whether that structure, rather than the reconciliation of complementary passes, is what buys RETRACE’s measured gain is unisolated. Whether a heterogeneous checking model adds a further increment on top is, per RETRACE’s own limitations, a natural extension nobody in this set has measured.

The residual risk concentrates where no referent exists

Assembling the three results yields a map of what a review-free stack covers and what it cannot. Spec-agreement audits cover implementation drift from the frozen document — the 116 code corrections the verification cycles produced (arXiv 2608.12440). Deterministic gates cover what they always covered: the compiler, the type system, the pre-existing regression suite — kept in the case study as their own layers, a dedicated compile/test feedback-loop session after implementation and a regression run after the change, rather than as checks inside each audit cycle. The drift-detection machinery accumulating in the 2026 spec-driven development literature (merge gates, citation checks, regression oracles) extends that floor. What remains uncovered clusters in three places.

Spec-versus-intent defects. The specification is constructed, not given, and everything downstream certifies fidelity to it. A wrong requirement propagates through 31 clean audit passes untouched — the audits would enforce the error faithfully. In the case study this channel is guarded by one operator skim and the natural-language request; no automated pass examines it, and no automated pass can, because there is no machine-readable referent for intent.

Unspecified behavior. Conformance says nothing about behavior the spec never constrains. The spec’s scope grew from 110 to 160 files during refinement as dependencies surfaced, and the final change exceeded the frozen scope by 29 files (arXiv 2608.12440) — evidence that the coverage boundary was porous even for the system’s author. What the implementation does in the unconstrained region is checked only by the regression suite and subsequent use.

Weak constructed oracles. Where the new behavior’s tests are agent-authored, the oracle is part of the artifact under suspicion. A large-scale audit of agent-authored test code found 80.2% of test-file patches carry weak or no explicit oracle signals (arXiv 2606.18168) — assertions that smoke without alarming. An agent that writes the code, the spec, and the tests has authored every referent in the loop, which is the same trust topology that makes self-graded agent success unreliable in benchmark settings.

The pressure to accept these residuals is real and documented: telemetry across 10,000+ developers — reported secondhand through a 67-source multivocal literature review — shows 98% more pull requests against 91% longer review times with flat delivery metrics (arXiv 2605.01160). On those figures, diff-level review is not scaling with agent-era throughput regardless of what replaces it. The spec-first stack is a serious replacement for one class of failure — implementation drift — at a unit cost human review seems unlikely to match, though nobody has run that comparison: the case study reports no control condition and supplies no human-review baseline. It does not replace judgment about what the system should do, and the case study’s own limitations section, read carefully, claims nothing of the kind.

Practical Implications

Freeze and consolidate before implementation. Present the implementing and verifying agents one settled specification document, never the revision trail that produced it. SpecPath’s 35/100 result is measured on contract-equivalent histories, so consolidating keeps that variance out of the loop — though consolidation is the paper’s baseline condition, not its proposed mitigation, and its own proposal, the contract ledger, remains untested (arXiv 2608.09799).
Run verification in fresh sessions against the frozen referent — never as same-context review. The fresh-session prescription comes from Anthropic’s guidance and the case study’s practice, not from RETRACE, whose passes consume the original trajectory. What RETRACE adds is that structured reconstruct-and-reconcile checking beat plain self-review on both scaffolds it tested — while plain self-review itself lost points on one scaffold and gained on the other (arXiv 2608.08950), too scaffold-dependent to carry the check alone.
Treat convergence as a stopping heuristic and record its basis. Log the per-pass finding series; a spike after quiet cycles — ten findings at cycle 15 after five near-quiet cycles in the one instrumented case — argues for more consecutive zeros on higher-stakes changes, and for treating any zero as a recall statement about the auditor (arXiv 2608.12440).
Keep the deterministic floor under the probabilistic loops, and isolate it from the agent. The case study kept compiler, types, and the pre-existing regression suite as separate layers — a dedicated feedback-loop session and a post-change regression run — rather than folding them into the audit cycles; graders the agent can touch are graders the agent can game.
Add a direction-flip check on significant diffs. Reconstructing the problem from the patch with the ticket withheld rescued failures the forward pass missed (and vice versa — the two rescue different sets), and RETRACE’s per-issue cost stayed comparable to or below baseline, helped by high prompt-cache hit rates and shorter targeted output (arXiv 2608.08950) — a cheap layer that catches a failure class same-context review misses.
Price agent-authored tests as weak oracles until proven otherwise. With 80.2% of agent test patches showing weak or no explicit oracle signals (arXiv 2606.18168), require explicit assertion-strength checks before counting the new behavior’s tests as verification.
Re-spend saved review attention on the two channels no audit reaches. Human scrutiny of the specification against intent, and adversarial probing of unspecified behavior, are the relocated form of the review job — the same upstream migration visible in how engineering practices transfer into agent loops. Deleting the diff read is defensible; deleting the spec read is not.

Open Questions

What is the escape rate when the spec itself is wrong? The case study cannot observe this channel by construction — a spec defect that survives refinement is enforced, not caught. No instrumented case yet measures how often converged-but-wrong ships, and at what downstream cost.
How many consecutive zero-finding passes buy how much confidence? The non-monotone finding series suggests two may be thin for high-stakes changes, but nobody has framed the stopping rule as the sequential-statistics problem it is, with auditor recall estimated rather than assumed.
Does consolidation actually reduce path sensitivity? SpecPath’s contract-ledger proposal predicts it; the paper explicitly leaves the comparison — ledger versus token-matched summary under the same budget — unrun.
Is withholding the referent actually the active ingredient? RETRACE’s ablation cannot say — its issue-visible and issue-withheld passes gain identically and the paper credits their reconciliation — so a design that varied only referent visibility would be the first direct test of the case study’s stated separation principle.
Does a heterogeneous verifier beat a fresh session of the same model? The case study’s checker shares the writer’s model and system prompt; RETRACE’s shares the backbone. Both name the cross-model variant as an extension, and the increment it buys is unmeasured.
Does the protocol reproduce outside its author’s hands? The clearest next step is the paper’s own: an independent operator running the same protocol on a public codebase, which would remove the single-case, self-reported, and closed-source limitations at once (arXiv 2608.12440).

Scout: When the Spec Is the Oracle — What Specification-First Verification Actually Proves