Agentic Verified Optimization of Real-World Software
Abstract
Program optimization aims to improve performance while preserving behavior. Coding agents can already make programs faster by changing algorithms, data structures, and execution strategies. However, existing equivalence checks mostly rely on tests, which agents have been shown to exploit, passing the tests without preserving the intended behavior. We propose agentic verified optimization, in which an agent produces a faster implementation together with a machine-checked proof of equivalence to the existing one. Because the existing implementation serves as the specification, the task avoids the specification-writing bottleneck of verified code generation, and recent advances in theorem proving make the proofs attainable. We formulate the task at the function and repository levels in Lean 4, where programs can be both executed and reasoned about. Few real-world applications are written in Lean, so we develop Aqueduct, an agentic framework that migrates C, C++, Go, and Rust programs into native Lean, validates each port by differential testing against its original. On the 189 reference implementations in Verina, agents produce faster proved rewrites for 156, including algorithmic changes such as replacing exponential recursion with dynamic programming. On 17 migrated applications, their 92 proved rewrites speed up 47 of 51 application scenarios. These application-level gains are smaller than the function-level ones, making the choice of functions to optimize an important problem. Current agents can thus already carry out verified optimization on both standalone functions and applications migrated from real programs. We discuss the remaining challenges and the steps toward verified optimization in production.
The following analysis is generated by AI and may contain errors. It is separate from the authors’ abstract and is not peer review.
Research summary
The paper proposes agentic verified optimization, where LLM agents generate faster code with machine-checked proofs of equivalence, and demonstrates its feasibility on real-world software migrated to Lean 4. By using the existing code as the specification, it avoids the specification-writing bottleneck and prevents reward hacking, showing that current agents can perform verified optimizations that are both correct and faster, albeit with modest application-level gains.
Methodology
The paper introduces "agentic verified optimization," a framework where LLM agents generate faster code implementations alongside machine-checked proofs of equivalence in Lean 4. The methodology is robust, leveraging the existing implementation as the specification to avoid the bottleneck of writing formal specs. It addresses the critical issue of reward hacking in test-based optimization by using formal proofs. The development of "Aqueduct," a framework for migrating C/C++/Go/Rust code to Lean with differential testing, is a significant technical contribution that enables the evaluation of this method on real-world software, not just toy problems.
Results & evaluation
The evaluation is extensive, covering 189 standalone functions from the Verina benchmark and 17 migrated real-world applications. The results show that agents can produce verified speedups in a majority of cases (82.5% for functions). The distinction between function-level microbenchmarks and application-level macrobenchmarks is well-handled, showing that while function-level gains are substantial, application-level gains are more modest due to I/O and unoptimized parts of the code. The comparison against a single-agent migration baseline for Aqueduct demonstrates the effectiveness of the multi-agent migration strategy.
Reproducibility
The paper provides detailed descriptions of the agent setup (Codex with GPT-5.6 Sol), the Lean version, and the timing protocols. The use of deterministic generators for workloads and the open-source nature of Lean and the benchmarks (Verina, ProgramBench) suggests high reproducibility. However, the specific prompts and agent orchestration logic for Aqueduct would need to be released to fully replicate the migration results.
Limitations
The primary limitation is the reliance on Lean 4, which has a small ecosystem of real-world applications, necessitating the migration step. The migration process itself is complex and may not capture all nuances of the original programs. Additionally, the speedups, while verified, are often modest at the application level (geometric mean 1.12x), limiting immediate practical impact for production systems where larger gains are typically expected.
Broader impact
This work bridges the gap between LLM-based code generation and formal verification, offering a path to trustworthy automated optimization. It has implications for software engineering, formal methods, and AI safety by providing a mechanism to ensure that AI-generated optimizations do not introduce subtle bugs. The framework could be extended to other proof assistants and languages, potentially transforming how performance-critical code is developed and maintained. The paper proposes agentic verified optimization, where LLM agents generate faster code with machine-checked proofs of equivalence, and demonstrates its feasibility on real-world software migrated to Lean 4. By using the existing code as the specification, it avoids the specification-writing bottleneck and prevents reward hacking, showing that current agents can perform verified optimizations that are both correct and faster, albeit with modest application-level gains.
Author of this paper? Send a correction.