PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Xinhao Zhang, Jingjie Lu, Kunpeng Liu, Fei Xie

arXiv:2609.06383v1cs.SEcs.CL

TL;DR

Code growth and structural complexity make direct repository maintenance difficult for engineers and LLMs. PROOF manages code through topology-preserving natural-language Specs and verifies them by reconstructing source code. Experiments report preserved behavior and validated Spec content across real-world repositories.

  • Problem

    Growing codebases and structural complexity strain maintenance and make direct code management difficult to reconcile with structural and behavioral equivalence.

    Source: §1 · p. 1, §3 · p. 3

  • Method

    PROOF maps codebases to natural-language Specs that preserve repository topology, verifies them through code reconstruction, and uses them to drive updates.

    Source: §1 · p. 2, §3 · p. 3, §4.1 · p. 3

  • Results

    Experiments show that Spec structure mirrors codebase organization, reconstructed code preserves original behavior, and node descriptions are validated by human and model judges.

    Source: §6 · p. 9

  • Takeaways & Limitations

    The verified Spec provides a basis for managing code through specifications, while drift calibration offers a way to detect and correct semantic drift during sustained evolution.

    Source: §6 · pp. 8–9

    Verification depends on existing test suites, so codebases with insufficient test coverage need complementary techniques such as LLM-based test generation.

    Source: Limitations · p. 10

Abstract

from arXiv · show

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 Introduction

Growing code scale and complexity strain engineers’ maintenance capacity, while context limits and cross-file dependencies make direct LLM repository management prone to hallucinations and inconsistencies. PROOF uses a structured Spec representation, validates it by reconstructing code from the Spec, and supports Spec-driven updates.

1 Introduction

  • Context-window limits and dependencies spanning multiple files impede LLM repository management and can lead to hallucinations and logical inconsistencies.The introduction frames these problems against code growth that outpaces engineering teams’ cognitive capacities and increases maintenance burden.Source: §1 · p. 1
  • PROOF represents repositories as hierarchical natural-language Specs, with modular object and function units linked through the repository’s native call graph.This combines localized units with preserved global topology to adapt to LLM context limits.Source: §1 · pp. 1–2
  • Round-trip verification reconstructs code using only the generated Spec, testing whether it captures critical functionality without omission.The authors present this as an objective check that the Spec reflects source code rather than hallucinations, making it trustworthy for downstream operations.Source: §1 · p. 2
  • PROOF is a closed-loop system for managing code through Specs, with code modifications and Spec updates synchronized to prevent semantic drift.Its contributions include Spec generation, validation, and Spec-driven code updates.Source: §1 · p. 2

2 Related Work

Prior work represents code through natural language, dependency graphs, or round-trip verification, but the cited approaches leave gaps in structural constraint, node-level detail, or continuous drift detection.

2 Related Work

  • The related-work section frames intermediate representations as a way to constrain repository updates while making code easier for LLMs to reason about.It describes a progression from natural-language abstraction through graph modeling to round-trip verification.Source: §2 · p. 2

2.1 Natural Language Representations

  • Earlier natural-language approaches support code description and repository evolution, but free text lacks structural constraints and verifiable semantics for safe modification of complex logic.The subsection traces the line from code summarization to repository-level outlines and agents.Source: §2.1 · p. 2

2.2 Graph-Based Structural Models

  • Graph-based methods preserve macro-level dependencies, but their high-level intent or vector nodes lack detail for fine-grained modification.The subsection includes data-flow, definition-reference, planning, and persistent repository graphs.Source: §2.2 · p. 2

2.3 Round-Trip Verification

  • Round-trip verification methods include encoding-decoding benchmarks, conformal filtering, and IR-mediated migration, yet the cited pipelines rely on soft verification without continuous drift detection.The subsection names RTCE, SimRAG, and EPAM.Source: §2.3 · p. 3

3 Problem Formulation

The formulation treats safe code updates as preserving unaffected structure and behavior, while recasting direct code-space updates as semantic transformations in a topology-preserving surrogate space.

3 Problem Formulation

  • The codebase is formalized as an AST hierarchy and directed graph of containment and dependency relations.Its nodes are distributed across levels, from modules to function clusters.Source: §3 · p. 3
  • A safe update must preserve the syntactic structure of unaffected regions and maintain identical outputs over the unchanged input domain.The formulation expresses these requirements as structural and behavioral equivalence constraints.Source: §3 · p. 3
  • As code and dependency density grow, directly mapping a codebase and change request to updated code becomes fragile and risks cascading modifications that break equivalence.The formulation links this fragility to the information density of the code dependency graph.Source: §3 · p. 3
  • The surrogate space preserves the codebase’s graph structure while replacing language-specific node detail with natural-language Spec nodes.The mapping retains the hierarchy and graph edges while filtering syntactic detail, so updates can be reasoned about as structure-preserving semantic distillation.Source: §3 · p. 3

4 Methodology

PROOF represents code as a hierarchical natural-language Spec graph and operates on it through generation, round-trip verification, and localized updates. Its design preserves topology while checking reconstructed behavior and letting engineers review semantic edits.

4 Methodology

  • PROOF manages codebase updates through natural-language Specs in three phases: generation, verification, and update.The methodology manipulates the Spec rather than directly managing code in source space.Source: §4 · p. 3, Figure 2 · p. 4

4.1 Specification Generation

  • Function and Object closures capture local code semantics, while deterministic parsing assembles their declared dependencies into a Spec graph topologically isomorphic to the codebase.The function contract records control-flow segments and six fields; the object closure groups class state, invariants, and methods.Source: §4.1 · pp. 3–5

4.2 Equivalence Verification

  • Verification reconstructs code from the Spec alone and checks that it retains the tests the original code passed, without requiring reconstruction to fix pre-existing defects.The repository test suite is used as a finite sample of possible inputs, and Fidelity measures the fraction of originally passing tests that reconstruction still passes.Source: §4.2 · pp. 5–6

4.3 Codebase Update

  • For a change request, PROOF localizes affected Spec nodes and decomposes the request into independent edits, confining semantic error and leaving unaffected AST regions unchanged.The proposed edits are presented in structured natural language for engineer review; the LLM then generates and assembles the code automatically.Source: §4.3 · p. 6
  • Incremental updates can accumulate drift between the Spec and code; PROOF can regenerate a reference Spec, leaving developers to decide whether to realign them.The drift measure is a reference indicator and does not force a reset.Source: §4.3 · pp. 6–7

5 Experiments

PROOF is evaluated by reconstructing code from repository representations and assessing behavioral, structural, and interpretability outcomes. It leads the reported repair-round and structural comparisons, while human and model judges rank it first across interpretability dimensions.

5.1 Experimental Setup

  • Across three SWE-bench repositories, Claude 5 Sonnet-backed PROOF and three baselines were assessed on test behavior, AST similarity, and human- and LLM-rated interpretability.The repositories range from 9.5K–37K lines and 0.49K–4.2K tests; original test suites were isolated during generation.Source: §5.1 · p. 7

5.2 Behavioral Equivalence

  • On Seaborn, PROOF reaches 100% Pass@3 versus RepoAgent’s 51.32% and RPG-Encoder’s 38.93%; on Pytest it reaches 91.24% at Pass@2.PROOF has the highest Pass@3 across all three repositories (100%, 100%, and 96.80%).Source: Table 2 · p. 7, §5.2 · p. 7

5.3 Structural Equivalence

  • PROOF achieves the highest AST similarity overall, peaking at 96.12% on Pytest, and maintains 87.32% on Seaborn.The authors attribute precise AST alignment to strict Spec constraints, verifiable closures, and continuous validation.Source: Table 3 · p. 8, §5.3 · p. 8

5.4 Interpretability

  • PROOF ranks first across all four interpretability dimensions under both human and LLM judging.Its larger gaps in Completeness and Consistency are linked to the six-field closure template and Deps/Data fields that carry node relations.Source: Figure 6 · p. 8, §5.4 · p. 8

6 Conclusion

The conclusion presents PROOF as a Spec-centered process for code evolution through generation, verification, and update. Experiments support the Spec’s structural, behavioral, and node-content accuracy, while drift calibration offers a way to detect and correct semantic drift over sustained evolution.

6 Conclusion

  • PROOF organizes code evolution through Spec generation, verification, and update.The Spec lets developers locate, review, and drive code evolution.Source: §6 · pp. 8–9
  • Experiments support the Spec’s accuracy in structural topology, behavioral equivalence, and node-level content.The conclusion says its skeleton mirrors codebase organization, reconstructed code preserves original behavior, and human and model judges find node descriptions reliable.Source: §6 · p. 9
  • Drift calibration (∆i) offers a way to detect and correct semantic drift during sustained evolution.Source: §6 · p. 9

Limitations

PROOF’s applicability is bounded by test infrastructure, underlying model capabilities, and the static call-graph setting used in the current evaluation.

Limitations

  • Behavioral verification relies on existing test suites; codebases without sufficient test coverage need complementary techniques such as LLM-based test generation.Source: Limitations · p. 10
  • Effectiveness varies with the underlying LLM’s language understanding; low-resource languages and unseen private DSLs may require RAG or fine-tuning.Source: Limitations · p. 10
  • The evaluation covers static call graphs within individual repositories, leaving distributed architectures using RPCs or message queues for future work.Source: Limitations · p. 10

A Spec Example

The example shows how PROOF represents repository elements as structured closures and presents them for navigation and editing. A tracing-identifier request is decomposed into ordered, node-level Spec and source changes.

A Spec Example

  • The example defines Object closures with ClassDesc, DataState, Invariants, and Mobj, and Function closures with Desc, I/O, Meta, Deps, Data, and Error.A module-level function’s Data field links to a method on the Flask object across the object boundary.Source: A Spec Example · p. 11
  • The Spec Viewer presents a symbol hierarchy, a selected node’s closure and source, and its dependency edges alongside the open maintenance checklist.The hierarchy mirrors Project/Module/Object/Function levels, and the center panel shows corresponding code updates in real time.Source: A Spec Example · p. 11
  • The tracing-identifier request becomes three node-level edits: configure an opt-in header, store its value on the request, then expose it to templates.The first two edits are high priority because the header must be configured before reading, and read before exposure; the template edit is a medium-priority usability addition.Source: A Spec Example · p. 11

B Ablation Study

The ablation measures Seaborn token use for IR construction and three-round reconstruction, then tests PROOF’s Pass@1 across backbone models.

B Ablation Study

  • PROOF’s IR construction consumes 4.32M tokens on Seaborn, 1.30× RPG-Encoder’s 3.32M; RepoAgent consumes 6.03M.The comparison covers four systems on Seaborn, the middle-scale repository, and reports construction separately from reconstruction.Source: Table 4 · p. 12, B Ablation Study · p. 12
  • Across three rounds, PROOF totals 5.49M reconstruction tokens, below RPG-Encoder’s 6.12M, RepoAgent’s 6.59M, and EPAM’s 14.20M.PROOF spends 5.29M tokens in Round 1, but its subsequent repair rounds add little as it converges rapidly; the total-cost advantage is conditional on that faster convergence.Source: Table 5 · p. 12, B Ablation Study · p. 12
  • Even with GPT-5.5 Medium, PROOF reaches 55.7% Pass@1, above RepoAgent with Claude 5 Sonnet at 29.95%.PROOF’s Pass@1 varies across backbones, with reported values dropping from 83.5% to 55.7%; the pipeline was rerun on Seaborn using three backbone models.Source: Table 6 · p. 13, B Ablation Study · p. 13

C Human Evaluation Instructions

The instructions specify blinded, per-node human ratings and the information raters use to assess each description.

C Human Evaluation Instructions

Loading 2609.06383v1…