以規格優先方式與 AI 編碼代理達成收斂：一項拆除核心架構不變量的案例研究——橫跨 189 個檔案、71.7 萬行的程式碼庫，且無測試預言機與人為程式碼審查

摘要

本文報告了一個在規範優先協議下由AI編碼代理執行的大規模架構重構之單一、完整儀器化案例研究，其中生成之程式碼未經人工審查，亦無預先存在的測試基準（oracle）可用以驗證目標行為。該任務為拆除一個跨越大型相互依賴程式碼庫的核心不變式，作者評估其透過漸進式重構實際上不可行，此類變更傳統上需要改寫（rewrite）而非重構。在本文所述協議下，該代理成功完成了此任務。該系統為一個由3,648個檔案組成、共717,725行程式碼的生產環境TypeScript應用程式。此任務需要拆除一個核心生命週期不變式：即保證UI面板在AI請求期間保持開啟。目標行為是串流生成在面板關閉後仍能持續，並可在重新開啟時重新連接至同一個即時串流，且無遺失或重複。該協議包括：由代理進行正式規範制定、14輪針對原始碼審核該規範之精化循環、原子性實作、編譯/測試回饋循環，以及隨後17輪針對凍結規範審核程式碼之驗證循環。在31次審核通過中，共修正了201個缺陷，全程無任何人類執行該程式。收斂標準為經驗性的：連續兩次驗證通過且回報零發現。此變更涉及189個檔案（其中31個為新增）；加上提取階段，兩次提交共計288個檔案、34,770行新增、16,422行刪除。在首次及後續約三十次的會話中，該軟體均按規範運作，未觀察到任何錯誤。耗時：三天；成本：2,430美元。完整的規範與原始會話日誌（超過1,500頁，法文）已作為證據公開，可供檢視整個流程，並可提交至語言模型進行一致性檢查。

English

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.