cs.SESep 6, 2026

From Reading Code to Reading Spec: A Verified Layer for LLM-Driven Codebase Maintenance

Authors: Xinhao Zhang, Jingjie Lu, Kunpeng Liu, Fei Xie

Organizations: Portland State University, USA · Clemson University, USA

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

Abstract

The rapid growth of LLM-generated code increases software complexity and the maintenance burden on engineers. While LLMs offer a potential automated alternative, this structural complexity hinders their ability to manage codebases directly. We introduce the Provable Representation Of Original Functionality (PROOF), which manages codebases indirectly via structured specifications. To enable full-lifecycle codebase management strictly through these specifications, PROOF abstracts codebase topology into a hierarchical natural-language representation. To establish absolute trust, the system proves semantic equivalence by reconstructing source code exclusively from this specification. This verified foundation drives maintenance requests, executing code modifications while synchronously updating itself to prevent semantic drift. Experiments on real-world repositories confirm the effectiveness of these specifications.

Figures & tables

Figure 1: Trends in total code volume versus the software engineering workforce, and the corresponding average maintenance burden per engineer (2016–2026).
Figure 2: Overview of PROOF’s three-phase pipeline. Generation : the codebase’s call graph is traversed node by node, and every Object and Function receives a structured natural-language Spec node, forming the Spec, an interconnected graph of Spec nodes mirroring the exact shape of the code’s dependency graph. Verification : code is reconstructed from the Spec alone and checked against the original codebase’s own test suite over repair rounds, synchronously updating both the code and the Spec until every originally-passing test passes on the reconstruction, thereby validating the Spec. Update : given a new change request, PROOF localizes the affected Spec nodes, the natural-language edit is reviewed and approved by a software engineer, and the approved edit is propagated into code by the LLM.
Figure 3: Function-level call graph of Flask’s core module (436 nodes, 1016 edges).
RepoFilesLinesNonblankTests
Flask249,5027,560491
Seaborn5429,22424,1542,381
Pytest8137,77031,4634,224
Table 1: Scale of the three evaluation repositories.
Figure 4: Test-suite pass rate across repair rounds (Pass@1 →\to Pass@2 →\to Pass@3).
Figure 5: AST structural similarity ( pycode_similar ) between each system’s reconstructed/regenerated codebase and the real source.
Figure 6: Spec Trustworthiness (Exp3): human (3-rater mean) and LLM-as-a-Judge (k=3 mean) scores across four content-quality dimensions.
Appendix figures & tables4 assets

Supplementary material from the paper’s appendix.

Appendix

Figure 8: The Spec Viewer’s interface for the same get_send_file_max_age node, laid out in three panels. Left : the codebase’s call graph unfolded into a hierarchical, collapsible tree, mirroring the Spec’s Project/Module/Object/Function levels rather than the raw file layout. Center : the selected node’s Spec content (I/O, State, Segments) rendered alongside the source it maps to, so editing the Spec and watching the corresponding code update happen together in real time. Right : the Request panel, where an open maintenance request is decomposed into a checklist of concrete edits, each targeting one function; clicking an item jumps to that node for editing, and it is checked off once resolved. The request is complete once every listed function has been fixed, at which point the change is ready for testing.
Table 9
Table 10
BackbonePass@1 (Seaborn)
Claude 5 Sonnet83.5%
Gemini 3.1 Pro72.1%
GPT-5.5 Medium55.7%
Appendix
Table 6: PROOF’s Seaborn Pass@1 under different backbone LLMs.
More in this topic

Automated Software Engineering

Automated Software Engineering uses AI, search, and verification methods to automate tasks across the software development lifecycle.

See all 82 papers

Explore similar work

CardsList

  1. Teaching Code LLMs to Reason with Intermediate Formal Specifications

    Jul 5, 2026Minh Le-Anh, Cuong Chi Le, Tien N. NguyenFormal VerificationCode Language Models

    FPT Software AI Center Hanoi Univ. of Science and Tech. Hanoi, Vietnam · University of Texas at Dallas Texas, USA

  2. Inferring Code Correctness from Specification

    May 28, 2026Tambon Florian, Papadakis MikeAutomated Software TestingCode Generation Evaluation

    University of Luxembourg Luxembourg, Luxembourg

  3. LLM-Assisted Repository-Level Generation with Structured Spec-Driven Engineering

    May 4, 2026Shuzhao Feng, Boqi Chen, Brett H Meyer +1Code GenerationRepository-Level Code Generation

    McGill University · Montreal, Quebec, Canada · University of Ottawa +1