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

• URL: http://arxiv.org/abs/2608.12440v2
• Date: Sat, 15 Aug 2026 11:27:55 GMT
• Title: 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 summary: This paper reports a single, fully instrumented case study of a large-scale architectural dismantling by an AI coding agent.<n>Under the protocol described here, the agent completed it successfully.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Watermarks Without Verification: AI Text Watermarking After the EU AI Act [49.51124343181601]
  Article 50 of the EU AI Act requires generative AI providers to mark the content their systems produce and ensure it can be detected as AI-generated.<n>Anthropic disclosed that every Claude model released after that date embeds a watermark based on SynthID-Text in all generated text, enabled by default with no user opt-out.<n>We argue that neither the objections nor the assurances can currently be verified and that this unverifiability, rather than watermarking itself, is the substantive governance failure.
  arXiv  Detail & Related papers  (2026-09-09T01:56:17Z)
• VeriPhy: Agentic Physical Reasoning for World Model Evaluation and Refinement [57.86962208273888]
  We present an auditable physical-verification system in which a text-only planner compiles the prompt into typed physical obligations.<n>Each action returns a provenance-carrying evidence record whose payload, when usable, is either a typed measurement or an explicitly tagged learned state.<n>We anchor evaluation in a 1,500-clip corpus of human-annotated flaw records that localize real generation failures in prompt reference, space, and time.
  arXiv  Detail & Related papers  (2026-09-02T20:36:45Z)
• From Traceability to Justifiability: Accountability Structures in Agentic Software Engineering [0.0]
  We measure, from public material only, whether AI records can express a claim and whether they hold where declared.<n>Across 188 double-graded cells we found no platform whose default record emits a content identity of a behavioral system.<n>An instrument computes realized assurance depth from a pipeline's published exhaust alone and compares it with the declared depth.
  arXiv  Detail & Related papers  (2026-08-21T16:45:00Z)
• A Reproducibility Protocol for Cross-Implementation Evaluation of Post-Quantum ACVP Test Vectors [0.0]
  This study defines a product-neutral protocol for three public implementations of NIST ML-KEM.<n> Protocol v2 freezes provider-specific capabilities, applies one validation-error symmetrically, preserves every selected case, and separates bytes, validation verdicts, unsupported operations, and adapter errors.
  arXiv  Detail & Related papers  (2026-08-13T21:29:59Z)
• Vero: Can AI Agents Build Formally Verified Software Repositories? [45.09790101960906]
  Vero is the first benchmark to evaluate joint implementation and proof at the repository level.<n>It contains 43 multi-module instances from real-world repositories spanning Python, Dafny, Verus, and Coq.<n>To improve benchmark reliability, Vero also includes an audit mechanism where agents are allowed to formally prove unsatisfiability of provided specification.
  arXiv  Detail & Related papers  (2026-08-13T17:41:27Z)
• Converted, Not Equivalent: Benchmarking Codebase Conversion via Observational Equivalence [56.25095230687242]
  Coding agents often over-trust their own local validation routines and declare success on artifacts that satisfy surface checks.<n>This problem is especially acute in conversion, where prior evaluation is outcome-driven.<n>Across blind conversion attempts, the best system reaches 26.7--28.9% overall pass rate despite Spec pass rates up to 91.1%.<n>This suggests that failures stem more from contract-misaligned self-validation than from limited budget or backbone strength.
  arXiv  Detail & Related papers  (2026-05-27T19:57:15Z)
• Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols [1.5229705287183657]
  SPECA is an audit framework that derives explicit, categorized security properties from natural-language specifications and reuses them across implementations.<n>On the RepoAudit benchmark, SPECA reaches 88.9% precision at 100% recall (F1=0.94) and surfaces 12 author-validated bugs beyond ground truth.<n>On the Sherlock Fusaka Audit Contest (10 targets, 366 submissions), SPECA recovers all 15 vulnerabilities expert-augmented and surfaces 4 fix-confirmed bugs.
  arXiv  Detail & Related papers  (2026-04-29T09:57:07Z)
• Scaling Human-AI Coding Collaboration Requires a Governable Consensus Layer [22.42181408084751]
  Vibe coding produces correct, executable code at speed, but leaves no record of the structural commitments, dependencies, or evidence behind it.<n>We propose Agentic Consensus: a paradigm in which the consensus layer C, an operable world model, replaces code as the primary artifact of engineering.<n>We propose benchmark task families designed to measure whether consensus-based reduce human intervention compared to chat-driven baselines.
  arXiv  Detail & Related papers  (2026-04-20T06:53:32Z)
• The Specification as Quality Gate: Three Hypotheses on AI-Assisted Code Review [0.0]
  The dominant industry response to AI-generated code quality problems is to deploy AI reviewers.<n>This paper argues that this response is structurally circular when executable specifications are absent.
  arXiv  Detail & Related papers  (2026-03-26T11:59:05Z)
• SlopCodeBench: Benchmarking How Coding Agents Degrade Over Long-Horizon Iterative Tasks [55.76734816061826]
  We introduce SlopCodeBench, a language-agnostic benchmark comprising 20 problems and 93 checkpoints.<n>We track two trajectory-level quality signals: verbosity, the fraction of redundant or duplicated code, and structural erosion.<n>No agent solves any problem end-to-end across 11 models; the highest checkpoint solve rate is 17.2%.
  arXiv  Detail & Related papers  (2026-03-25T19:26:44Z)
• When the Specification Emerges: Benchmarking Faithfulness Loss in Long-Horizon Coding Agents [15.65681557926802]
  Real research coding often does not: the intended system is progressively disclosed through in- teraction.<n>We introduce a benchmark for this setting and study faithfulne Ss Loss U nder eM ergent s Pecification (SLUMP)
  arXiv  Detail & Related papers  (2026-03-17T19:53:35Z)
• AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
  Existing benchmarks test only individual languages/tools, so the performance numbers are not directly comparable.<n>We address this gap with AlgoVeri, a benchmark that evaluates vericoding of $77$ classical algorithms in Dafny, Verus, and Lean.
  arXiv  Detail & Related papers  (2026-02-10T06:58:26Z)
• Probing Pre-trained Language Models on Code Changes: Insights from ReDef, a High-Confidence Just-in-Time Defect Prediction Dataset [0.0]
  We present ReDef, a high-confidence benchmark of function-level modifications curated from 22 large-scale C/C++ projects.<n>Defective cases are anchored by revert commits, while clean cases are validated through post-hoc history checks.<n>This pipeline yields 3,164 defective and 10,268 clean modifications, offering substantially more reliable labels than prior existing resources.
  arXiv  Detail & Related papers  (2025-09-11T07:07:11Z)
• Decompiling Smart Contracts with a Large Language Model [51.49197239479266]
  Despite Etherscan's 78,047,845 smart contracts deployed on (as of May 26, 2025), a mere 767,520 ( 1%) are open source.<n>This opacity necessitates the automated semantic analysis of on-chain smart contract bytecode.<n>We introduce a pioneering decompilation pipeline that transforms bytecode into human-readable and semantically faithful Solidity code.
  arXiv  Detail & Related papers  (2025-06-24T13:42:59Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.