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.
Figures & tables
Figure 1: Agentic verified optimization in a repository. An agent selects a function f from a Lean repository and jointly searches for a replacement f′ and an equivalence proof π . Keeping f fixed, it uses Lean’s errors and proof goals to revise both artifacts. The search returns the replacement with a checked proof that it preserves the reference’s behavior. Microbenchmarks measure function-level speedup, and macrobenchmarks measure the effect on the application.
Figure 2: From recursive search to dynamic programming. A simplified example from Verina task verina \ _advanced \ _33 , showing (a) the reference implementation, (b) the agent’s rewrite, and (c) their equivalence theorem, proved in Appendix D.1 . The rewrite runs 4,467.871× faster on the 261-input corpus.
Figure 3: The Aqueduct migration workflow. Three porting strategies produce candidate implementations. Test-design agents inspect the frozen candidates and build a shared corpus T , using differential execution, coverage, fuzzing, and mutation testing. The controller selects a port by agreement with the original across behavioral families. Repair agents revise the selected port, and rerunning the tests checks each revision as the corpus grows. The controller audits the resulting port for calls to the original and hardcoded answers before a single hidden evaluation.
Figure 4: Function-level optimization on the 189 Verina references. (a) The fraction of functions with a faster verified implementation, with counts shown inside the bars. (b) vfastp , the fraction with a verified speedup greater than threshold p (Equation 2 ), using a logarithmic horizontal axis. Each curve covers every function in its suite.
Suite
Targets
Improved
Geom. mean
Median
Basic
108
93
1.959×
1.109×
Advanced
81
63
1.716×
1.163×
All
189
156
1.851×
1.117×
Table 1: Verified optimization on the 189 Verina functions by suite. Aggregate speedups use the fastest verified implementation for each target, including its reference.
Function level (92 rewrites)
Application level (51 scenarios)
Comparison
Faster
Geom. mean
Median
Faster
Geom. mean
Median
Optimized Lean vs. migrated Lean
92/92
1.864×
1.402×
47/51
1.120×
1.077×
Optimized Lean vs. original
15/92
0.235×
0.217×
3/51
0.148×
0.160×
Migrated Lean vs. original
12/92
0.126×
0.120×
3/51
0.132×
0.158×
Table 2: Performance of migrated and optimized applications at both scales. Speedup is baseline runtime divided by evaluated runtime, and values above one favor the evaluated implementation. Faster counts the kernel-checked rewrites or application scenarios whose speedup exceeds one.
Figure 5: Repository-level optimization measured at two scales. (a) Each row is one of the 92 accepted rewrites, ranked by its speedup over the migrated Lean reference, with the migrated and optimized implementations placed by throughput relative to the original source-language operation. The dashed line marks the original. (b) The speedup of each rewrite over its migrated reference, on the same rows. (c) Application speedup of optimized over migrated Lean for the 51 scenarios, grouped by repository, with diamonds marking each repository’s three-scenario geometric mean.
Appendix figures & tables3 assets
Supplementary material from the paper’s appendix.
Appendix
Outcome
Mutants
Killed by both suites
16
Killed by generated tests only
12
Killed by ProgramBench tests only
1
Killed by neither
7
Total scored
36
Appendix
Table 3: Mutants killed by the generated tests and by the hidden ProgramBench tests on the same 36 compiled mutants across 9 repositories.
Repositories
Compiled mutants
Killed
Score
Median per repository
95% interval
25
190
101
53.2%
50.0%
39.1% to 67.0%
Appendix
Table 4: Mutation audit of the generated suite on the full audit population.
Figure 6: Contribution of migration components. Recovery under component ablations and two pipeline baselines. Removing candidate diversity produces the largest decrease among the four component ablations.