Specification-first convergence with an AI coding agent: a case study of dismantling a core architectural invariant across 189 files in a 717k-line codebase with no test oracle and no human code review

(authored by agents unless marked 🧑) Tag: abenhaim2026specification, paper

case and protocol

This is one instrumented case study of an AI agent removing a lifetime invariant from a VS Code extension. The paper says the task had “no human review of the generated code and no pre-existing oracle to validate the target behaviour” (Abstract, p. 1). The target was making a session panel closable while the AI orchestrator continued. The five-phase protocol is ideate, specify, refine, code, verify (Sec. 5, p. 8). The paper’s evidence is process logs and an outcome, not a formal proof of the extension.

technique 1: write a frozen behavioral specification

Use this when no existing test oracle defines the desired behavior. Start from a natural-language request, scope it, and have the agent produce a document describing user-visible behavior, interfaces, data flow, atomicity, and affected modules. The agent’s specification was then frozen before implementation. The paper states: “The intent is audited before generation, in the form of a written specification that is repeatedly challenged against the real source code, frozen, and audited again against that same reference” (Sec. 1, p. 2). Inference: for VL, the analogous artifact is a human-reviewed contract describing Rust state invariants and Verus pre/postconditions before code generation; prose alone is not a Verus assertion.

Run a fresh session that re-analyzes the specification against the actual repository, reports omissions or contradictions, and rewrites it. Repeat until a pass finds no corrections. Fourteen cycles averaged 35 minutes and produced approximately 85 corrections; cycle 14 returned zero findings and cycle 13 was frozen (Secs. 5.2 and Table 2, pp. 10–12). The method is summarized as: “Refinement is the process of having the agent re-analyse the specification against the real source code, report defects in the specification, and rewrite it” (Sec. 5.2, p. 10). Inference: a Verus workflow can perform the same audit over types, call sites, and existing contracts before adding proofs; each correction should identify whether the intended invariant or the code is wrong. The paper does not claim the resulting specification is complete.

technique 3: atomic implementation with compiler feedback

Ask the agent to implement the frozen specification in small accepted steps. In this case the agent initially proposed ten steps; three were accepted, and implementation took 2 hours 21 minutes 44 seconds (Sec. 5.3, p. 12). A separate feedback loop repeatedly compiles and runs available tests, correcting type, compilation, and unit-test failures. The paper explicitly distinguishes this from architectural verification: “The agent does not automatically correct compilation, typing or unit-test failures in its own output; this is the responsibility of the feedback loop” (Sec. 5.4, p. 13). Inference: for Verus, run cargo and Verus after each atomic patch, preserve failing diagnostics, and do not treat compiler success as proof of behavioral adequacy.

technique 4: verification against the frozen reference

After implementation, launch fresh sessions to compare code to the frozen specification, find residual architectural deviations, and correct them. Seventeen cycles were run; cycles 16 and 17 found zero defects, so the stopping rule was two consecutive zero-finding passes (Sec. 5.5, pp. 13–15). The paper says: “Verification is the process of having the agent analyse the current state of the source code against the frozen specification, report residual architectural defects and subtle deviations, and correct them” (Sec. 5.5, p. 13). Across 31 refinement and verification passes, 201 defects were corrected before a human executed the program: approximately 85 in the specification and 116 in generated code (Sec. 6, p. 16). Inference: this can complement Verus by auditing whether the contract still matches architecture, but repeated LLM audits are not a soundness argument; only checked Verus obligations establish the encoded properties.

evidence and what remains trusted

The operation touched 189 files (31 new), while the frozen specification tracked 160 files; the two commits and extraction touched 288 files (Abstract; Sec. 6, p. 16). The author reports success on the described UI behavior and publishes 1,500+ pages of logs (Abstract, p. 1). There was no control condition, no independent operator, and no characterization with weaker models (Sec. 7, pp. 18–19). The paper states: “The stopping rule was empirical rather than fixed in advance” (Sec. 5.5, p. 15), so convergence means two clean audits, not mathematical convergence. Tests remained available but were not an oracle for the new behavior. Inference: the trusted base includes the specification authoring process, the agent’s source inspection, compiler/tests, and the author’s judgment that the UI result is correct. The case demonstrates a useful governance loop, not formal verification.

implications for VL

Inference: the protocol is a moderate threat to a product that relies on agent self-review without proof because it shows large refactors can appear coherent while defects are found only through repeated audits. VL should use the frozen-specification and independent-session ideas before asking an agent to write Rust, then require Verus contracts, loop invariants, and decreases proofs for safety properties. Existing compiler/test feedback and architectural audit loops should not be presented as new formal techniques. The paper’s single case and self-reported result cannot establish reliability across repositories or models.

techniques for the catalog

frozen specification — create and freeze a behavioral reference before implementation when no oracle exists
refinement audit loop — repeatedly compare the specification with source until a defined clean-pass rule
atomic implementation feedback — implement in small steps and compile/test after each step
frozen-reference verification — audit generated code against the unchanged specification until two clean passes

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numerical/section/page references, technique descriptions, catalog entries, and overlap; corrected none.

Last edited: 2026-10-15

Steven Hé (Sīchàng)