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
Abstract
This paper reports a single, fully instrumented case study of a large-scale architectural refactoring by an AI coding agent under a specification-first protocol, with no human review of the generated code and no pre-existing oracle to validate the target behaviour. The task, dismantling a central invariant across a large interdependent codebase, was assessed by the author as effectively infeasible through incremental refactoring, the kind of change that conventionally calls for a rewrite instead. Under the protocol described here, the agent completed it successfully. The system is a 717,725-line production TypeScript application across 3,648 files. The task required dismantling a core lifetime invariant: the guarantee that a UI panel remains open for the duration of an AI request. The target behaviour was that a streaming generation survives the closing of its panel and can be reattached, on reopening, to the same live stream with no loss or duplication. The protocol: formal specification by the agent, 14 refinement cycles auditing that specification against the source code, atomic implementation, a compile/test feedback loop, then 17 verification cycles auditing the code against the frozen specification. Across 31 audit passes, 201 defects were corrected before any human executed the program. The convergence criterion was empirical: two consecutive verification passes returning zero findings. The change touched 189 files (31 new); with the extraction phase, the two commits total 288 files, 34,770 insertions, 16,422 deletions. Across the first and roughly thirty later sessions, the software behaved as specified, no bug observed. Elapsed: three days; cost: USD 2,430. The full specification and raw session logs, 1,500+ pages in French, are published as evidence, allowing inspection of the process and submission to a language model for consistency checking.
Community
Current AI coding agents, including Claude Code, Codex, Copilot and Cursor, demonstrate high throughput on isolated, self-contained tasks. Human review of the generated code is considered necessary in most practices.
These systems are highly capable, but unreliable at scale: once a change spans hundreds of interdependent files, agents can silently violate architectural invariants that no reviewer can track across that many files. Turning that capability into a disciplined process that reliably produces production-grade systems is becoming one of the central open problems in software engineering.
This is why we present a case study of AICode, a specialized AI coding agent, correctly completing a large architectural refactor (189 files, 717k-line codebase) with no test oracle and no human code review, using a specification-first convergent protocol. Full raw session logs are published for independent verification.
No test oracle and no human review — so what was the ground truth for "converged"? Did you diff against the old behavior on a sample, or was it just "the build passes and the invariant is gone"? And the part I'd want to see most: where did the spec have enough ambiguity that the agent had to pick a direction on its own, and how did you know it picked the right one?
The spec ambiguity: The spec is not ambigous UX wise. The UX requirements are clearly stated in a 20-line prompt at the begining of the job. How it could be considered ambigous, depending on how the word is used, the prompt did not contain any hint about how the codebase is built, how to do what is asked, which invariants to respect, which race conditions are involved, etc. The agent inspected the codebase in real time, and produced autonomously a 55-page long, extremely complex specification, describing how to translate the user's intent into code.
One concrete example, section 4: on reopening there's a three-way contention between panel initialisation, replay of already-generated content, and live streaming of new tokens, and nothing in the functional description dictates the order to resolve it in, the agent had to pick one and write it into the spec.
Since there is no oracle, it's not like the bun port or the SWE benchmark, there is no way to prove mathematically that the result is correct. Because the behaviour, the tests, did not exist. It is checked by running the app manually, under stress test, and observing the result. This is described in the paper, and was done across 30 coding sessions with the agent, while testing manually that the refactor produced a working software. This is as much proof you can get on a system of that complexity and that size. And this is very close to what you have when given a real life complex ticket on an existing app.
How do I know it picked the right one? I don't. This task is way too complicated for me. Again, this is not a formal method. There is no possibility of using a formal method for a new feature, given an app of almost 4000 files and thousands of features. It looks fine, it's modular, it seems serious. I see it as a tech lead would see a task of this size, treated by a squad. He would not prove correct the code using a formal method. I guess he would check how it looks, execute it, and probably validate, given the complexity.
To show how complex it is, this is the specification generated and refined 14 times by the agent: https://aisovereignlabs.ai/docs/case-study/liveSession/logs/liveSession-logs-phase2-specification-en.pdf
Convergence: The methodology uses loops. They are not like loop engineering, which reprocess the job until it works, more or less depending what variant is used. They are correction loops. For example, the agent writes the spec, then it fixes it iteratively, like explained in table "Table 2. Specification refinement cycles". It searches mistakes in the specification, and fixes them. We do this, in this example case study, until it can't find any mistake, at iteration #14.
Then we let the agent code. Then we do the same after coding with an automatic code review loop, 17 times, until convergence = no more mistakes found during 2 iterations. In the end, after 31 total audit loops, the agent fixed 201 mistakes. This is all self evaluated by the agent itself, using different agentic sessions to remove as much bias as possible.
This is an empirical study yielding working testable software. There is no mathematical proof, if that's what you expect. No one can prove a real life original task on a complex system of 750 000 lines. It can be tested, put to the test. Even better, the agent could be used in another study, with or without an oracle, independently from me.
Why did I publish this? I created the whole application, AICode, 100% dogfooded, with thousands of features, equivalent IMHO in complexity to Claude Code and Codex, alone, in 8 months, using this exact technology. I can't prove I did, because I can't prove anything so large and instrument 30 000 agentic sessions. But i know for a fact that it works, because the app works, and it's far from trivial. However, I was able to take one of the hardest 4000 commits, tp instrument it fully, exposing 100% of the agentic sessions logs, and to explain everything in a 14 pages paper.
I hope I answered your legitimate and tough questions. I tried to.
Models citing this paper 0
No model linking this paper
Datasets citing this paper 0
No dataset linking this paper
Spaces citing this paper 0
No Space linking this paper
Collections including this paper 0
No Collection including this paper