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

From Reading Code to Reading Spec: A Verified Layer for LLM-Driven Codebase Maintenance Xinhao Zhang1 , Jingjie Lu1 , Kunpeng Liu2 , and Fei Xie1 * 1

Portland State University, USA 2 Clemson University, USA {xinhaoz, jingjie, xie}@pdx.edu, kunpenl@clemson.edu

10

2.0B -> 27.1B files

0.8

0.4

21.2M -> 28.6M engineers 2018

2020

0.67

0.6

otal Software Engineers otal Code (olume

5 0

Maintenance Burden per Engineer

After LLMs

15

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.

1

Before LLMs

Code volume )er engineer (thousand files)

Relative growth (normalized)

arXiv:2609.06383v1 [cs.SE] 6 Sep 2026

Abstract

2022 2024 Introduction of GP -3.5

2026

0.2

0.23

Before LLMs After LLMs

Figure 1: Trends in total code volume versus the software engineering workforce, and the corresponding average maintenance burden per engineer (20162026).

tlenecks: context window constraints, which preclude processing repositories simultaneously (Liu et al., 2024a), and global dependencies that span multiple files (Jimenez et al., 2024). Together, these limitations induce context degradation, leading to code hallucination and logical inconsistencies. To bypass these direct-processing limitations, a viable strategy is to manage repositories indirectly through an intermediate representation (IR) (Lattner and Adve, 2004; Iyer et al., 2016), allowing models to reason over structural abstractions rather than raw, unbounded source code (Hejderup et al., 2018). To ensure reliability, this IR should satisfy three properties: (1) granularity adaptation, partitioning the repository into localized chunks that fit within context limits; (2) topology preservation, retaining the global dependency structures; and (3) verifiability, ensuring the representation is provably equivalent to the original code behavior rather than an unverified generative approximation. To realize this paradigm, we apply the standard software specification (Spec) as a structured intermediate representation. At the micro-level, it encapsulates objects and functions as minimal closure units, utilizing modular natural language to

Introduction

Software systems are experiencing continuous growth in scale and structural complexity, a trend accelerated by the proliferation of Large Language Models (LLMs) (Hatton et al., 2017; Ouyang et al., 2025). Consequently, code generation rates outpace the cognitive capacities of engineering teams. As Figure 1 illustrates, this widening disparity elevates the maintenance burden per engineer, resulting in mounting technical debt as machinegenerated code is integrated without adequate human review or long-term maintenance. A potential approach to mitigating this maintenance burden is to utilize LLMs not only as generators but also as automated maintainers (Liu et al., 2024b). However, applying LLMs to repositorylevel code management is impeded by two bot* Corresponding author.

1

capture essential semantics. At the macro-level, these units are structurally linked via the repository’s native call graph. This dual-level architecture adapts to LLM context limits while preserving global topology, establishing an explicit, human-readable abstraction layer that facilitates code comprehension and editing without requiring developers to navigate the underlying syntax directly. Furthermore, the effectiveness of this representation depends entirely on its rigorous verifiability. To prove that a Spec objectively reflects the source code rather than LLM hallucinations, we introduce a strict round-trip equivalence verification framework. By extracting a Spec from the original code and reconstructing the code relying exclusively on this Spec without source reference, we can objectively validate that the representation captures all critical functionality without omission, rendering it trustworthy for downstream operations. We decompose the realization of this representation into three lifecycle questions. Generation: how can this structured Spec be completely and systematically constructed for large-scale repositories? Verification: how can its precise consistency with the original codebase be objectively validated to prevent generative hallucinations? Update: how can a verified Spec drive code modifications, and how can bi-directional synchronization be maintained across sustained maintenance cycles to prevent semantic drift? To systematically address these questions, we developed a closed-loop system, the Provable Representation Of Original Functionality (PROOF), which enables developers to manage code strictly by managing Spec.

while synchronously updating the Spec, enabling developers to manage code exclusively through Spec without semantic drift.

2 Related Work Large codebases increase the burden on LLMs attempting to modify code directly, elevating the risk of broken dependencies and context-window overflow. To mitigate these bottlenecks, IR are constructed to indirectly constrain codebase updates. The evolution of these representations spans natural language abstraction, graph-based structural modeling, and round-trip verification, establishing the theoretical foundation for our methodology. 2.1 Natural Language Representations Code summarization was framed as sequence transduction, translating code into natural language descriptions (Iyer et al., 2016). Bimodal pre-training introduced identifier-aware objectives for bidirectional language-code mapping (Wang et al., 2021). This extended to repository-level evolution: natural language outlines synchronized with code (Shi et al., 2025), RepoAgent’s incremental updates from call relations (Luo et al., 2024), and DocAgent’s multi-agent, dependencyorder generation (Yang et al., 2025) drive changes through natural language. These methods read well, but free text lacks structural constraints and verifiable semantics, producing ambiguity on complex logic and limiting safe modification. 2.2 Graph-Based Structural Models Graph structures represent code dependencies, data flow, and call logic: variable-level data-flow graphs capture a function’s internal logic during pre-training (Guo et al., 2020), repository-level definition-reference graphs support issue localization and repair (Ouyang et al., 2025), a repository planning graph guides step-by-step module generation (Luo et al., 2026b), RPG-Encoder (Luo et al., 2026a) and LocAgent (Chen et al., 2025) reversemodel codebases into a persistent graph for representation and localization, and CoSIL (Jiang et al., 2025) constructs call graphs during search. These methods preserve macro-level dependencies but encode nodes as high-level intent or vectors, lacking detail for fine-grained modification.

Contributions. Our main contributions include: • A systematic methodology for Spec generation: a hierarchical natural-language representation mirroring the repository’s structural organization, driven by an algorithm that enables LLMs to process the codebase comprehensively. • A rigorous validation framework for the generated Spec: evaluating internal quality and semantic consistency with the source code, establishing it as an objectively verifiable equivalent rather than an unverified generative assumption.

2.3 Round-Trip Verification Verifying that IR-space modifications map correctly to executable code has become an

• A methodology for Spec-driven codebase updates: PROOF modifies and validates code 2

independent direction, round-trip consistency: RTCE (Maveli et al., 2026) formalizes it as a benchmark on encoding-decoding fidelity, SimRAG (Xu et al., 2025) applies conformal prediction to filter inconsistent samples, and EPAM (Grynets et al., 2026) drives industrial code migration through a IR-mediated codetext-code architecture. These pipelines remain incomplete: verification stays soft, relying on structural similarity or self-assessment, with no continuous drift detection.

3

language-specific detail at the node level, mapping code to natural-language Spec nodes NS . The codebase update then becomes: ( ) C ′ = Φ−1 ∆(S, R) , (1) where S = Φ(C) and E(C ′ | C, R) = 1, omitting syntactic detail while holding topological complexity constant, retaining only essential code intent as a semantic representation humans can manipulate directly. We instantiate S as a naturallanguage Spec, detailed in the next section.

Problem Formulation

4 Methodology

A codebase update modifies C, with test suite T , according to change request R to produce codebase C ′ while preserving quality. Its logic parses into an abstract syntax tree AST(C); C exhibits a nested hierarchy of levels L (modules decomposing into function clusters), formalized as a directed graph DC = (NC , EC ) whose nodes distribute across L and edges reflect containment and dependency. A safe update requires C ′ to satisfy a dual equivalence constraint, E(C ′ | C, R) = 1: structural equivalence EQUIVstruct (C, C ′ ), requiring unaffected regions’ syntactic framework to remain unchanged, AST(C \ R) ∼ = AST(C ′ \ R); and behavioral equivalence EQUIVbeh (C ′ , T ), requiring identical outputs over the unchanged domain, ∀x ∈ X \ R, C ′ (x) = C(x). Existing methods solve mapping F : (C, R) → ′ C directly in code space C, tracking dependency structure while handling syntactic detail. As scale grows and LLM-generated code enters in bulk, information density in DC rises sharply, rendering direct solving of F fragile and prone to breaking E through cascading modifications. To resolve this bottleneck, an IR consistent with the code’s topological structure but easier to reason about semantically can overcome the limits of manipulating low-level code directly. We formalize this representation’s set as a surrogate space S, recasting codebase updates as a structurepreserving semantic distillation across spaces. Since DC ’s topological dependencies determine system stability, we define a mapping Φ : C → S from the code space C to a surrogate space S, keeping the graph structure unchanged. An initial code C is instantiated as a Spec graph S = Φ(C): Φ preserves the isomorphic relation DC ∼ = DS , retaining L and EC , while filtering out

To address direct code management limitations, we propose an end-to-end approach called PROOF. Built around the Spec formalized in Section 3, it enables safe codebase updates by manipulating natural language Spec. Figure 2 shows three pipeline phases: Generation, Verification, and Update. 4.1 Specification Generation Determining the update logic directly in the lowlevel code space faces high complexity: Figure 3 shows the call graph of Flask (a real-world codebase), whose structure DC = (NC , EC ) forms a dense, entangled network at the macroscopic level, making full context difficult to process directly for developers and LLMs alike, obstructing the mapping Φ into the surrogate space. Although the macroscopic network is densely entangled, Figure 3’s right panel shows that microscopic dependencies are highly localized: any given node’s local dependencies are confined to a few immediate components. Decomposing the mapping at the local dimension is thus more viable than tackling dependencies head-on: the system distills local code fragments per node, then scales these up by preserving the call edges EC , assembling a global Spec graph S = (NS , ES ) isomorphic to DC = (NC , EC ), S∼ = DC , where NS is the distilled Spec modules and ES their dependency links. The following question is how to define this decomposition’s granularity: to preserve execution logic completely, we partition the space along the codebase’s static nested hierarchy L, preserving original semantic boundaries and dependencies. We instantiate L top-down into five levels, each with a physical form and semantic function: • Project: the top-level codebase abstraction. 3

Generation

Verification

Update

PROOF Original Repo

Specification

func1

LLM

[old] [new]

Topology Extraction

Code Reconstruction

Spec Generation

…

func5 [old] [new]

Test Extraction

LLM

…

New Request Reviewed and approved!

Test Suite Spec Node

Call Graph

Software Engineer

90%

96% Verified！

LLM

100%

Specification

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.

This static decomposition, however, severs the dynamic call edges EC . To restore the code topologically, we design the core mapping nodes, Object and Function, as semantic closures with strict constraints and self-contained boundaries. Existing LLM-based summarization methods mostly use free-text descriptions, readable but blurring precise dependencies and making EC harder to track. To maintain topological isomorphism in S, we constrain the model’s free generation through a standardized, strictly constrained template. The basic carrier of the behavioral contract is the Function closure: every function node vf unc ∈ NS is a structured tuple containing its segmented control-flow pieces (Segments), sealing within its boundary the external logic and side effects it depends on, following a six-field contract, vf unc = ⟨Desc, I/O, Meta, Deps, Data, Error⟩:

Figure 3: Function-level call graph of Flask’s core module (436 nodes, 1016 edges).

• Module: a physical directory or file grouping classes and functions by business domain. • Object: the union of a data structure (state) and Functions (behavior), its Spec aggregated from its functions. • Function: smallest, self-contained execution unit with defined inputs, outputs, and logic, serving as Φ’s semantic distillation entry point. • Segment: the code lines forming a single Function (a loop, or branch), needed since functions are often too long for a model to digest at once and must be split for processing.

• Description: the execution intent; • I/O Definition: constraints on parameter types and return values; • Meta: programming language, purity (side effects), and atomicity (multi-threaded safety); 4

• Dependencies & External Calls: every call to another node; • Data & Mutations: which global state or mutable arguments are read or modified; • Error Handling: the boundaries of exceptions thrown and caught.

field, a deterministic parsing algorithm reads these fields and extracts corresponding edges, without the LLM inferring the macroscopic structure. This avoids the structural bias free-form connection generation could introduce, aggregating related nodes locally into Modules and composing them upward, scaling from the smallest nodes to a global specification graph S = Φ(C) that remains topologically isomorphic to C.

Through the Deps and Data fields, the system records every function’s interaction with its external environment, specifically detailing which nodes it calls and which global state it reads or modifies, thereby converting dependencies previously hidden in the code into static, structured declarations. In the object-oriented paradigm, a class encapsulates its variables and data structures, so we define the Object closure as a nested tuple vobj ∈ NS : a class-level state definition enclosing methods Mobj operating on that state, vobj = ⟨ClassDesc, DataState, Invariants, Mobj ⟩. The three outer fields are:

4.2 Equivalence Verification The previous section defined the mapping Φ from C to S. During generation, structured closures and deterministic parsing guarantee that the resulting Spec graph S = Φ(C) is isomorphic in topology to the original codebase, DC ∼ = DS . Topological isomorphism only guarantees correct calls and dependencies between nodes. Each node’s natural-language description is written by the language model, and if it omits or misdescribes information while carrying out Φ, S will not accurately reflect the behavior of C even when the structure is correct. Structural isomorphism is therefore not sufficient on its own. Since S is the only object later localization and editing act on, we must show that Φ preserves the information needed to reproduce the code’s behavior, capturing everything that determines how the code behaves when run rather than mere syntactic details or formatting. Only once this is checked, confirming S accurately represents C’s behavior, are the later editing procedures justified. S and executable code C are different representations that cannot be compared directly. To check whether S contains enough behavioral information, we use a zero-edit roundtrip: reconstruct code from S via the inverse mapping, Ĉ = Φ−1 (S), turning whether S is correct into whether C and Ĉ behave the same way. We write Ĉ to distinguish this from C ′ , reserved for code produced by an actual change request R in Section 4.3. Two pieces of code are behaviorally equivalent if they produce the same output on every input, matching the definition of EQUIVbeh in Section 3: in the zero-edit case (R = ∅), Ĉ should produce the same output as C for every x ∈ X :

• ClassDesc: the object’s design intent and responsibility; • DataState: the class’s internal instance variables and their type constraints; • Invariants: the logical constraints that must hold throughout an instance’s lifecycle. An object’s internal behavior aggregates from Mobj : each method vm ∈ Mobj reuses the function tuple structure above (vm = ⟨Desc, I/O, . . . ⟩), except its Data field extends to and is constrained by the parent’s DataState (the class’s self variable). These definitions provide the foundation for scaling through the hierarchy: since every node encapsulates both its internal logic and an interface declaration, discrete code entities are stitched back together via these cues, aggregating locally into Modules and composing upward into a network reflecting the project’s global dependency relations. Relying on these interface declarations, the system splits Φ into two phases: local node instantiation, and global topology extraction and assembly. In the local instantiation phase, the system traverses the codebase along its static hierarchy; for each node the LLM reads its code, splits it into ordered control-flow segments, and fills the six contract fields per the template, keeping context small and reducing drift from long-range dependencies. In the global assembly phase, the system reconstructs the dependency network among nodes: since every closure declares its call intentions through the Dependencies & External Calls

∀x ∈ X , Ĉ(x) = C(x)

(2)

If so, S preserves behavior-determining information in C, and Φ loses no information that matters. 5

Checking this equality requires examining every input in X , which is not possible in practice; we therefore use the repository’s existing test suite T as a finite sample of X to approximate it. Requiring Ĉ to pass every test in T runs into a practical problem: real code C often has existing defects or flaky tests and does not itself pass every test in T , so this would require the model to fix pre-existing defects during reconstruction, which this check is not meant to verify. To resolve this, we relax the equivalence condition. Let Pass(C) = {t ∈ T : exec(C, t) = pass} be the tests C passes, using the same exec from Section 3; we replace exact equivalence with directed inclusion: Pass(C) ⊆ Pass(Ĉ)

meaning the macro-level requirement is concretely translated into separate updates to specific text fields within a function or object tuple. Because the number of affected nodes is far smaller than the total number of nodes in the Spec graph (i.e., |NR | ≪ |NS |), this design of decomposing the request into node-level operations mechanically confines the semantic error a single change may introduce to a local region. At the same time, when the ( system )applies the ′ −1 inverse mapping C = Φ ∆(S, R) to reconstruct the code, because the modification is confined to specific nodes, the syntactic structure of unaffected regions remains unchanged. This satisfies the equivalence constraint defined earlier, AST(C \R) ∼ = AST(C ′ \R). This mechanism not only narrows the scope of subsequent testing and verification but also effectively limits the system state’s drift within a single change. In this process, the focus of code review and editing shifts to the semantic level. Because the modification proposal for the affected nodes NR is presented as structured natural language, a developer need only read the text and confirm whether its business logic matches the change request. Once the modification proposal has passed review within the surrogate space, the generation and assembly of the underlying code (i.e., applying the inverse mapping Φ−1 ) is carried out automatically by the large language model. This mechanism establishes a division of labor in which the developer manages the Spec and the model modifies the code, so that the developer does not need to directly handle low-level syntactic detail. Although local mapping can effectively control the error of a single modification, after i successive incremental updates, some semantic drift be(i) tween the current Spec graph NS and the underlying code remains difficult to avoid. To measure this drift, the system provides an intuitive calibration method. When necessary, the system can regenerate a fully accurate reference (i)∗ Spec graph NS from the current underlying code, and quantify the error by computing the difference in Fidelity between the two:

(3)

This states the minimum requirement, no regression: it does not penalize Ĉ for defects already in C, verifying only that logic C already implements correctly is not lost after the roundtrip. This set-inclusion condition is binary; to quantify and compare it across experiments, we turn it into a continuous score, Fidelity: the fraction of C’s originally passing tests that Ĉ still passes. Fidelity(NS ) =

|Pass(C) ∩ Pass(Ĉ)| |Pass(C)|

(4)

where Ĉ = Φ−1 (NS ). If C already passes the entire test suite (Pass(C) = T ), the denominator becomes |T |, and Fidelity reduces to the ordinary test pass rate. This continuous score avoids treating the mapping as a failure over a few failing tests while keeping the check strict: a high score, whether reported as Fidelity on real code with pre-existing defects or as the pass rate on a clean benchmark, is evidence that S preserves the behavior-determining information in C. Passing this check is the precondition for the localization and editing procedures described in the following sections. 4.3

Codebase Update

When the system receives a change request R, the large language model maps it onto the specification graph S in the surrogate space S and locates the affected subset of nodes NR . Through this process, the global modification operation ∆(S, R) is decomposed into a set of mutually independent local changes (i.e., an independent modification ∆v is performed for each affected node v ∈ NR ),

( (i)∗ ) ( (i) ) ∆i = Fidelity NS − Fidelity NS

(5)

Here, ∆i serves only as a reference indicator; the system does not force any reset based on it. Depending on the situation, when a developer judges the drift to be too large, they may choose to over6

PROOF

EPAM

RepoAgen%

RPG-Encoder

100

100

100

80

80

80

60

60

60

40

40

40

20

20

20

0

0

Test suite pass rate (%)

write the current state with the reference graph, thereby realigning the code and the Spec. This design both preserves the flexibility of day-to-day updates and provides a means of removing long-term accumulated error, ensuring the codebase remains stable and reliable over long-term evolution. Appendix A walks through a concrete case study of how a Spec node is structured in practice and how a change request R is decomposed into node-level edits kept in sync with code.

Pass@1 Pass@2 Pass@3 Flask

Pass@1 Pass@2 Pass@3 Seaborn

0

Pass@1 Pass@2 Pass@3 Py%es%

Figure 4: Test-suite pass rate across repair rounds (Pass@1 → Pass@2 → Pass@3).

5.2 Behavioral Equivalence

5

Experiments

5.1

Experimental Setup

We evaluate on three SWE-bench (Jimenez et al., 2024) repositories (9.5K–37K lines, 0.49K–4.2K tests; Table 1). Original test suites are isolated during generation to prevent leakage. In our primary experiments, we apply Claude 5 Sonnet as the underlying language model. We provide a detailed ablation study regarding token efficiency and backbone sensitivity in Appendix B. Repo

Files

Lines

Nonblank

Tests

Flask Seaborn Pytest

24 54 81

9,502 29,224 37,770

7,560 24,154 31,463

491 2,381 4,224

Repo

Method

Pass@1

Pass@2

Pass@3

Flask

PROOF EPAM RepoAgent RPG-Encoder

84.9% 31.77% 4.28% 57.8%

97.6% 94.30% 67.5% 94.0%

100% 98.57% 94.6% 99.2%

Seaborn

PROOF EPAM RepoAgent RPG-Encoder

83.5% 0.00% 29.95% 3.49%

98.1% 35.78% 46.96% 26.84%

100% 59.64% 51.32% 38.93%

Pytest

PROOF EPAM RepoAgent RPG-Encoder

0% 0.00% 0.09% 0.38%

91.24% 0.00% 74.48% 86.60%

96.80% 8.07% 89.75% 90.46%

Table 2: Test-suite pass rate across repair rounds.

As shown in Table 2, PROOF yields the highest Pass@3 across all three repositories (100%, 100%, and 96.80%). For Flask and Seaborn, PROOF demonstrates higher Pass@1 and reaches 100% within three rounds. The variance among methods is most prominent on Seaborn: PROOF reaches 100% at Pass@3, whereas RepoAgent and RPGEncoder record 51.32% and 38.93%, respectively. The results on Pytest warrant further analysis. As the largest repository, Pytest exhibits the highest code volume, test count, and structural coupling. All evaluated methods record a Pass@1 of approximately 0%. This occurs because high-level integration errors in a tightly coupled architecture propagate extensively, leading to widespread test failures rather than indicating that all reconstructed functions are incorrect. However, by preserving call graph topologies and explicit node boundaries, PROOF facilitates structural error localization during the repair phase, bringing the pass rate to 91.24% at Pass@2. Similarly, RPGEncoder, which also incorporates graph structures, improves to 86.60% at Pass@2. In contrast, EPAM, which operates without strict boundary definitions, records a 0.00% pass rate at Pass@2.

Table 1: Scale of the three evaluation repositories.

We compare against three baselines (Section 2): RepoAgent (Luo et al., 2024), RPGEncoder (Luo et al., 2026a), and EPAM (Grynets et al., 2026). Because comparing heterogeneous IRs directly is difficult, we assess information retention by reconstructing codebases strictly from IR (without source access) across three dimensions: Behavioral equivalence: Fidelity (Equation 4) measures the reconstruction’s pass rate, calibrated against the original suite’s perfect pass rate. Pass@1 is the initial reconstruction’s pass rate. Iterative failure-driven repairs yield Pass@k, strictly maintaining test suite isolation. In our experiments, we set k = 3, recording the progressive success rates from Pass@1 through Pass@3. Structural equivalence: We compute Abstract Syntax Tree (AST) similarity between the original codebase and the unmodified Pass@1 reconstruction using pycode_similar (fyrestone, 2017). Interpretability: We average scores across four dimensions evaluated by 3 independent human raters and 3 LLM-as-a-judge trials. 7

EPAM

RepoAgent

Flask

RPG-Encoder

Seaborn

PROOF

P%test

EPAM

Fai(hf)lness

100

Me(hod RepoAgen(

Verifiabili(y

RPG-Encoder

Comple(eness

H)man

Ra(er LLM-as-a-J)dge

Consis(ency

Score (1-5 Li er()

AST structural similarity (%)

PROOF

5 4 3 2 1

80 60 40

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.

5.3

(match to code’s real behavior), Verifiability (specific, checkable claims), Completeness (I/O, side effects, error conditions, dependencies covered), and Consistency (agreement with parent/sibling nodes). Together, these criteria provide a sufficient framework to ensure both local node accuracy and global structural coherence, verifying the representation is rigorous enough to safely drive automated modifications. An LLM-as-a-Judge scores the same items with the identical rubric, repeated three times per item; we take the mean, with runto-run variance as a stability check. PROOF ranks first on all four dimensions under both scoring sources, though the margin varies. Faithfulness and Verifiability gaps are small (0.3 and 0.5 points), since even free-text baselines mostly state a function’s behavior clearly. Completeness and Consistency gaps are larger: on Completeness, PROOF exceeds RepoAgent (3.3) by 1.1 points and EPAM (1.9) by 2.5, tracking to the six-field closure template that forces every node to state I/O, side effects, error conditions, and dependencies explicitly. On Consistency, PROOF exceeds RepoAgent (2.9) by 1.7 and RPG-Encoder (3.9) by 0.7, since PROOF carries a node’s relation to its parent and siblings through the Deps and Data fields at generation, whereas isolated generation cannot guarantee consistency. The same margins appear in the LLM-asa-Judge’s scoring.

Structural Equivalence Method PROOF EPAM RepoAgent RPG-Encoder

Flask

Seaborn

Pytest

90.45% 83.22% 82.43% 89.67%

87.32% 71.91% 80.25% 40.36%

96.12% 80.90% 86.52% 86.10%

Table 3: Structural similarity to the original codebase.

To evaluate architectural preservation, we measure Abstract Syntax Tree (AST) similarity between reconstructed and ground-truth codebases. As Table 3 shows, PROOF achieves the highest similarity globally, peaking at 96.12% on Pytest. This highlights the necessity of combining macrolevel topology with fine-grained closures. While RPG-Encoder performs competitively on Flask (89.67%), its abstraction of node intents causes structural collapse on Seaborn (40.36%). Conversely, PROOF maintains 87.32% fidelity by explicitly defining boundaries for every node. Baselines also reveal the limitations of pure natural language and soft verification. Lacking rigid constraints, RepoAgent suffers generative deviations capping at 86.52%. Similarly, EPAM’s soft verification permits continuous drift, yielding 80.90% on Pytest. PROOF resolves these issues by enforcing the Spec as a strict constraint. By isolating functions into verifiable closures and utilizing continuous validation, our approach eliminates ambiguity and ensures precise AST alignment. 5.4

6 Conclusion

Interpretability

Software now grows faster than engineers can maintain it at the code level, and applying large language models to repository-scale code is limited by context windows and complex dependency topologies, producing hallucinations and inconsistencies. We introduce a verified intermediate representation, the Spec, which lets developers locate, review, and drive code evolution through three

We sample 7 functions each from Flask, Seaborn, and Pytest (21 total), including 2 dependencylinked groups per repository so Consistency has real cross-node context to check. Three raters independently score the four anonymized descriptions (PROOF and baselines EPAM, RepoAgent, RPG-Encoder) on four dimensions: Faithfulness 8

stages: generation, verification, and update. Experiments show the Spec is accurate in structural topology, behavioral equivalence, and node-level content: its skeleton mirrors the codebase’s organization, reconstructed code preserves original behavior, and node descriptions are validated as reliable by both human and model judges. The drift calibration mechanism (∆i ) further offers a way to detect and correct semantic drift during sustained evolution.

9

Limitations

40th International Conference on Software Engineering: New Ideas and Emerging Results, pages 101–104.

The applicability of PROOF depends on existing engineering infrastructure and underlying model capabilities. Verification relies on existing test suites to ensure objective behavioral equivalence. For codebases lacking sufficient test coverage, our method needs to incorporate complementary techniques like LLM-based test generation to complete the verification loop. Furthermore, PROOF’s practical effectiveness varies with the underlying LLM’s semantic understanding of the target language. For low-resource languages or unseen private domain-specific languages (DSLs), our approach requires utilizing retrieval-augmented generation (RAG) or model fine-tuning to enhance the LLM’s syntax comprehension. Finally, our current evaluation focuses on resolving static call graphs within individual repositories. Extending this framework to distributed architectures, such as systems relying on RPCs or message queues rather than static graphs, remains one of several potential directions for future research.

Srinivasan Iyer, Ioannis Konstas, Alvin Cheung, and Luke Zettlemoyer. 2016. Summarizing source code using a neural attention model. In Proceedings of the 54th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 2073–2083. Zhonghao Jiang, Xiaoxue Ren, Meng Yan, Wei Jiang, Yong Li, and Zhongxin Liu. 2025. Issue localization via llm-driven iterative code graph searching, 2025. URL https://arxiv. org/abs/2503.22424. Carlos E Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, and Karthik Narasimhan. 2024. Swe-bench: Can language models resolve real-world github issues? In International Conference on Learning Representations, volume 2024, pages 54107–54157. Chris Lattner and Vikram Adve. 2004. Llvm: A compilation framework for lifelong program analysis & transformation. In International symposium on code generation and optimization, 2004. CGO 2004., pages 75–86. IEEE. Nelson F Liu, Kevin Lin, John Hewitt, Ashwin Paranjape, Michele Bevilacqua, Fabio Petroni, and Percy Liang. 2024a. Lost in the middle: How language models use long contexts. Transactions of the association for computational linguistics, 12:157–173.

References Zhaoling Chen, Robert Tang, Gangda Deng, Fang Wu, Jialong Wu, Zhiwei Jiang, Viktor Prasanna, Arman Cohan, and Xingyao Wang. 2025. Locagent: Graphguided llm agents for code localization. In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 8697–8727. fyrestone. 2017. pycode_similar: A simple plagiarism detection tool for Python code. https://github. com/fyrestone/pycode_similar. Version 1.4. Oleg Grynets, Vasyl Lyashkevych, Arsen Dolichnyi, Roman Piznak, Taras Zelenyy, and Volodymyr Morozov. 2026. Specification-based code-text-code reengineering for llm-mediated software evolution. arXiv preprint arXiv:2605.25232.

Tianyang Liu, Canwen Xu, and Julian McAuley. 2024b. Repobench: Benchmarking repository-level code auto-completion systems. In International Conference on Learning Representations, volume 2024, pages 47832–47850. Jane Luo, Chengyu Yin, Xin Zhang, Qingtao Li, Steven Liu, Yiming Huang, Jie Wu, Hao Liu, Yangyu Huang, Yu Kang, et al. 2026a. Closing the loop: Universal repository representation with rpgencoder. arXiv preprint arXiv:2602.02084. Jane Luo, Xin Zhang, Steven Liu, Jie Wu, Jianfeng Liu, Yiming Huang, Yangyu Huang, Chengyu Yin, Ying Xin, Yuefeng Zhan, et al. 2026b. Rpg: A repository planning graph for unified and scalable codebase generation. In International Conference on Learning Representations, volume 2026, pages 91932–91985.

Daya Guo, Shuo Ren, Shuai Lu, Zhangyin Feng, Duyu Tang, Shujie Liu, Long Zhou, Nan Duan, Alexey Svyatkovskiy, Shengyu Fu, et al. 2020. Graphcodebert: Pre-training code representations with data flow. arXiv preprint arXiv:2009.08366. Les Hatton, Diomidis Spinellis, and Michiel van Genuchten. 2017. The long-term growth rate of evolving software: Empirical results and implications. Journal of Software: Evolution and Process, 29(5):e1847.

Qinyu Luo, Yining Ye, Shihao Liang, Zhong Zhang, Yujia Qin, Yaxi Lu, Yesai Wu, Xin Cong, Yankai Lin, Yingli Zhang, et al. 2024. Repoagent: An llm-powered open-source framework for repositorylevel code documentation generation. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing: System Demonstrations, pages 436–464.

Joseph Hejderup, Arie Van Deursen, and Georgios Gousios. 2018. Software ecosystem call graph for dependency management. In Proceedings of the

10

Figure 7 situates this triple within the full call graph of the Flask repository: the Flask object is one node among hundreds, and its closure content, along with that of its method and the standalone function that depends on it, is exactly what a developer or an LLM reads instead of the underlying source when working through PROOF. Figure 8 shows the same get_send_file_max_age node in the interactive Spec Viewer, which renders every Function/Object closure as a navigable page and is laid out in three panels. The left panel exposes the codebase’s full symbol hierarchy as a collapsible tree, folded module by module rather than by raw file path, mirroring the Spec’s own Project/Module/Object/Function levels (Section 4.1). The center panel renders the selected node’s closure (I/O, State, Segments) alongside the source it was generated from; a developer driving the edit through any LLM coding console (e.g., Claude Code, Antigravity, Codex) can update the Spec text and watch the corresponding code update beside it in real time, verifying the two stay consistent without leaving the page. The right panel resolves that node’s Called-By/Calls/SharesState-With edges, which correspond to the dependency edges shown in Figure 7, and lists the maintenance request currently open against it as a checklist of per-node TODO items. We illustrate this checklist with the concrete request shown in the figure: adding a per-request unique identifier for distributed tracing. The request decomposes into three node-level edits, each recording both a Spec-level change and its corresponding source change: (1) App’s default_config gains a REQUEST_ID_HEADER constant defaulting to None, so the feature is opt-in; (2) Flask.preprocess_request reads that header from the incoming request and stores it as g.request_id, marking the first point in the request lifecycle where both g and request are available; (3) _default_template_ctx_processor exposes g.request_id to templates under the key request_id, following the pattern already used for g, request, and config. The first two edits are marked high priority, since the header name must exist in config before it can be read, and must be read before it can be exposed; the third, marked medium, is a usability addition layered on top once the first two hold. As shown in the figure’s checklist, the developer checks off each edit on completion, giving a running view of how

Nickil Maveli, Antonio Vergari, and Shay B Cohen. 2026. Can llms compress (and decompress)? evaluating code understanding and execution via invertibility. In Findings of the Association for Computational Linguistics: ACL 2026, pages 25625–25660. Siru Ouyang, Wenhao Yu, Kaixin Ma, Zilin Xiao, Zhihan Zhang, Mengzhao Jia, Jiawei Han, Hongming Zhang, and Dong Yu. 2025. Repograph: Enhancing ai software engineering with repository-level code graph. In International Conference on Learning Representations, volume 2025, pages 30098–30121. Kensen Shi, Deniz Altınbüken, Saswat Anand, Mihai Christodorescu, Katja Grünwedel, Alexa Koenings, Sai Naidu, Anurag Pathak, Marc Rasi, Fredde Ribeiro, et al. 2025. Natural language outlines for code: Literate programming in the llm era. In Proceedings of the 33rd ACM International Conference on the Foundations of Software Engineering, pages 150–161. Yue Wang, Weishi Wang, Shafiq Joty, and Steven CH Hoi. 2021. Codet5: Identifier-aware unified pretrained encoder-decoder models for code understanding and generation. In Proceedings of the 2021 conference on empirical methods in natural language processing, pages 8696–8708. Ran Xu, Hui Liu, Sreyashi Nag, Zhenwei Dai, Yaochen Xie, Xianfeng Tang, Chen Luo, Yang Li, Joyce C Ho, Carl Yang, et al. 2025. Simrag: Self-improving retrieval-augmented generation for adapting large language models to specialized domains. In Proceedings of the 2025 Conference of the Nations of the Americas Chapter of the Association for Computational Linguistics: Human Language Technologies (Volume 1: Long Papers), pages 11534–11550. Dayu Yang, Antoine Simoulin, Xin Qian, Xiaoyi Liu, Yuwei Cao, Zhaopu Teng, and Grey Yang. 2025. Docagent: A multi-agent system for automated code documentation generation. In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 3: System Demonstrations), pages 460–471.

A

Spec Example

Section 4.1 defines the Object closure vobj = ⟨ClassDesc, DataState, Invariants, Mobj ⟩ and the Function closure vf unc = ⟨Desc, I/O, Meta, Deps, Data, Error⟩. We illustrate both using three nodes actually generated by PROOF for Flask: the Flask class as an Object closure, its method get_send_file_max_age (vm ∈ Mobj ), and _prepare_send_file_kwargs, a module-level function declared outside any object whose Data field reads ctx.app.get_send_file_max_age, thereby connecting the two nodes across the object boundary within the same call graph. 11

much of the request remains.

B

tions. Building on this, we further measure consumption at the reconstruction stage. Table 5 reports the total token consumption for reconstructing Seaborn’s codebase from each system’s representation, across all three rounds (Round 1 is the zerorepair, full-codebase generation; Rounds 2–3 are test-failure-driven repair rounds).

Ablation Study

To examine the efficiency and performance of our method, we measure token consumption on Seaborn. Seaborn is the middle-scale repository among the three benchmark repositories used throughout the paper, covering the four systems compared in the main experiments: PROOF, RepoAgent, RPG-Encoder, and EPAM. We report consumption separately for the two stages of the pipeline: (1) IR construction (Code → intermediate representation) and (2) reconstruction (IR → Code), the latter broken down across three rounds (k = 3) under the same repair protocol as Experiment 1 (Section 5.2): Round 1 is the zero-repair, full-codebase generation, and Rounds 2–3 are testfailure-driven repair rounds. Table 4 reports the size of each system’s generated intermediate representation on Seaborn, along with the total token consumption for constructing this representation across the whole repository. System

IR words

Tokens

RPG-Encoder PROOF RepoAgent EPAM

18,206 126,743 549,948 237,889

3.32M 4.32M 6.03M 9.61M

System

Round 1

Total

RPG-Encoder PROOF RepoAgent EPAM

3.65M 5.29M 4.75M 12.01M

6.12M 5.49M 6.59M 14.20M

Table 5: Reconstruction-stage token consumption on Seaborn, k = 3.

Reconstruction tokens (M)

PROOF

EPAM

RepoAgent

RPG-Encoder

Round 1

Tot l

EPAM

RepoAgent

15.0 12.5 10.0 7.5 5.0 2.5 0.0

PROOF

RPG-Encoder

Figure 10: Round 1 (hatched) versus total (solid) reconstruction tokens per system on Seaborn, k = 3.

Table 4: Size of each system’s generated IR on Seaborn and IR construction token consumption.

IR construction tokens

IR words

PROOF requires a substantial initial investment in Round 1 (5.29M tokens), exceeding both RPGPROOF EPA RepoAgent RPG-Encoder Encoder (3.65M) and RepoAgent (4.75M), though remaining more efficient than EPAM. We attribute 600000 10 this to the structured six-field contract, which pro500000 8 400000 duces the most information-dense representation 6 300000 per node but also carries the highest per-token 4 200000 cost when consumed as generation input. This up2 100000 front cost, however, is fully offset during the repair 0 0 (a1) IR size (a2) IR construction cost phase. Because PROOF converges rapidly, its subFigure 9: IR words (a1) and IR construction tokens (a2) sequent repair rounds require minimal additional per system on Seaborn, drawn as two small-multiple pan- tokens, bringing its total consumption (5.49M) beels rather than one dual-axis chart since the two measures low RPG-Encoder’s (6.12M). In contrast, RepoAare different units at very different magnitudes. gent (6.59M) and EPAM (14.20M) both struggle to achieve full convergence, continuing to incur PROOF’s IR construction consumes 4.32M to- substantial repair costs in subsequent rounds withkens on Seaborn, 1.30× RPG-Encoder’s 3.32M. out fully resolving. PROOF’s advantage in total reRepoAgent, which generates free-form per- construction cost is therefore conditional: because entity documentation without batching, con- it converges faster, spending more tokens in the sumes 6.03M tokens. EPAM, lacking a tightly- first round pays off. Beyond evaluating the token efficiency of IR constrained topological structure, likely consumes more tokens navigating complex dependency rela- construction and reconstruction, it is crucial to de12

Figure 7: The Flask object located within the full call graph of the Flask repository (436 nodes, 1,016 edges), with its Object closure, the get_send_file_max_age method closure, and the _prepare_send_file_kwargs function closure that depends on it shown alongside the node they were generated from.

Backbone Claude 5 Sonnet Gemini 3.1 Pro GPT-5.5 Medium

pabilities (dropping from 83.5% to 72.1% and finally to 55.7%). This variance confirms that the framework still benefits significantly from advanced base models, as reconstruction is not entirely backbone-independent. However, the most critical finding emerges when comparing across methods rather than across models: even when powered by the weakest backbone in our test suite (GPT-5.5 Medium at 55.7%), PROOF still substantially exceeds the highest-performing baseline powered by the most capable model (RepoAgent using Claude 5 Sonnet, which achieved only 29.95% as shown in Table 2). This absolute margin of over 25 percentage points isolates the impact of the framework’s core design. It provides strong empirical evidence that PROOF’s advantage over existing baselines is fundamentally attributable to the method itself, specifically the hierarchical, dependency-aware Spec generation process and the rigorous constraints of the structured six-field contract, rather than merely piggybacking on the raw computational power or context window of any single backbone model.

Pass@1 (Seaborn) 83.5% 72.1% 55.7%

Table 6: PROOF’s Seaborn Pass@1 under different backbone LLMs.

termine whether PROOF’s performance is overly reliant on the reasoning capabilities of a specific backbone model. Large language models exhibit varying degrees of proficiency in instruction following, context management, and zero-shot code synthesis. To ensure our framework’s robustness and demonstrate that the observed advantage is not merely an artifact of a single powerful LLM, we re-run the Generation and Verification pipeline on the Seaborn repository using three distinct backbone models and report the resulting Pass@1 metrics. For this ablation study, we interface with each model through its native environment to maximize expected performance: Claude Console for Claude 5 Sonnet, Codex for GPT-5.5 Medium, and Antigravity for Gemini 3.1 Pro.

C Human Evaluation Instructions

As detailed in Table 6, the choice of backbone LLM undeniably influences the final reconstruction quality, with Pass@1 scores scaling predictably with the underlying model’s general ca-

This is the rating form used by human raters for the Interpretability experiment (Section 5.4): a 1– 5 Likert scale with anchors, scored per node de13

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.

scription. Rater instructions. • Each rating covers one node’s description. Raters do not know which system produced it (PROOF / RepoAgent / RPG-Encoder / EPAM, order shuffled and labels hidden, randomly numbered as Description A/B/C/D). • Each node is rated alongside its source code (for Faithfulness / Verifiability / Completeness) and its parent/sibling node descriptions (for Consistency). • The four dimensions are scored independently, 1–5, half-points allowed (e.g., 3.5).

14

Dimension

1

2

3

4

5

Faithfulness

Description seriously diverges from or fabricates the code’s behavior

Broadly correct, but multiple inaccurate or misleading statements

Mostly accurate, with one or two detail-level deviations

Accurate, with only minor flaws that do not affect understanding

Verifiability

Entirely generic phrasing (e.g., “processes data”, “executes logic”), no claims checkable against the code Covers almost none of I/O, side effects, error handling, dependencies

Mostly generic, only a few specific, checkable statements

About half the content is specific and checkable, still many vague statements

Most statements are specific and clearly pointed, individually verifiable

Fully accurate, matches the code’s actual behavior exactly, no fabrication Every statement is specific and checkable, traceable line-by-line to the code

Covers only a small fraction of key information, omitting content critical to understanding/modifying the function Multiple noticeable inconsistencies or awkward transitions

Covers most key information, but one or two items are clearly missing

Key information is mostly complete, only minor (atypical edgecase) information missing

I/O, side effects, error conditions, dependencies, and all key information fully covered

Broadly self-consistent, with one or two minor wording/granularity mismatches

Basically consistent with context, only very minor phrasing differences

Fully self-consistent with parent/sibling nodes, uniform terminology, granularity, and boundary description

Completeness

Consistency

Clearly contradicts the parent or sibling node (e.g., inconsistent interface/data-flow description)

Table 7: Human evaluation rubric: 1–5 Likert scale with anchors, one form filled per node per anonymized description.

15

Related documents

• FeatX: Editing Software by Editing Features for Repository-Level Code Evolution#324970
• CHISEL-ing Back Source Code with AI-enabled Iterative Recovery#784756
• CHISEL-ing Back Source Code with AI-enabled Iterative Recovery#783166
• AI-Powered Debugging: Exploring Machine Learning Techniques for Identifying and Resolving Software Errors#70785
• Continuous Autonomous Refactoring: A Research Roadmap for AI-Driven Code Quality Maintenance#821191