Agentic Verified Optimization of Real‑World Software

1Speedups need a check that covers every input

Coding agents are now asked to make code faster. PIE rewrites programs for speed, KernelBench evaluates generated GPU kernels, and Jitskit synthesizes systems specialized to a workload. These systems check that the faster program still behaves correctly by running tests.

Tests can show that a program is wrong, but not that it is right . The difference matters when the tests also decide the agent's reward, because the agent can then pass the tests without preserving the behavior. Jitskit describes an apparent 6× improvement that came from regenerating test values instead of storing them, and an audit found correctness failures in 39.5% of the GPU kernels that an optimization harness had accepted .

A proof of equivalence covers every input. With a proof as the check, an agent can change algorithms and data representations freely, and the correctness requirement stays the same.

2Why now: autoformalization is the bottleneck

Proving capability has advanced quickly. Provers trained with reinforcement learning reach olympiad level , and agents now formalize research mathematics, from open Erdős problems to a complete Lean proof of Fermat's Last Theorem .

A proof establishes only the statement it proves. Translating intended meaning into a correct formal statement, or autoformalization, is now the bottleneck. Human-written formal statements contain semantic errors in 16.4% of miniF2F and 38.5% of ProofNet , strong models reach at most 9.8% correctness when formalizing graduate-level theorem statements , and in a recent formalization effort on Navier–Stokes blow-up, the Lean proof does not correspond to the natural-language proof . Programs have the same problem. Writing specifications that capture the intended behavior is difficult, even manually , and manually curated specifications contain errors .

Verified optimization does not need a new statement. The existing implementation is the specification, so the theorem f = f′ is fixed before the agent starts and needs no translation from natural language. Proving capability can therefore improve real software now, without being limited by autoformalization.

3The task: a faster program and a proof

We formulate agentic verified optimization in Lean 4 , which is both a proof assistant and a general-purpose programming language with a native compiler. The same definitions run as compiled programs and appear in proofs. Given an executable reference function f in a repository R, the agent searches for a replacement f′ with the same signature and a proof π:

minimize_{f′, π} t_B(f′) subject to π : f = f′

Here t_B is the execution time on a workload B. Lean's kernel checks the proof against the unchanged reference in a fresh copy of the repository, so the agent cannot alter the reference or add axioms, and the replacement must build with its callers.

The reference is the specification. The reference implementation is executable, so its behavior can be read and tested directly, and it can be written as the simplest correct algorithm regardless of speed. Equality to it specifies the behavior completely, and the obligation does not change as the agent explores faster algorithms. A written specification that omits part of the intended behavior would let an agent drop that behavior, the same reward hacking that weak tests invite. Equality to the reference rules this out.

Implementation and proof are searched together. Each rewrite changes the proof. Hoisting a repeated computation requires showing that its value can be reused, and a new algorithm requires relating different intermediate states. A failed proof does not tell the agent whether the rewrite is wrong or the proof is incomplete, so the agent decides when to continue the proof, when to simplify the rewrite, and when to try another one.

The task does not saturate. Correctness is fixed, and speedup is a continuous measure rather than a pass rate. Every function in an existing codebase is an instance with its specification already in place.

Two settings. In function-level optimization, the agent is given the target function. In repository-level optimization, the agent receives an application and chooses which functions to rewrite. Function-level microbenchmarks then measure each rewrite, and application-level macrobenchmarks measure whether the application becomes faster.

4Example: from 2ⁿ recursion to dynamic programming

Verina task verina_advanced_33 computes the length of the longest increasing subsequence of a list. The reference makes two recursive calls per element, one that takes the element and one that skips it, so it explores 2ⁿ branches on an increasing list of length n. The agent's rewrite fills a table from the end of the list with the length of the longest increasing subsequence that starts at each position.

The listing is the compact form shown in the paper's Figure 2, with declarations renamed. Lean checks that the displayed implementations equal the recorded ones, and the proof depends only on the standard axioms propext and Quot.sound.

The proof is the hard part. The reference recurses on the remaining list and the previously chosen element, while the table is indexed by position. The agent proved that querying the table for any suffix and any preceding element returns what the reference's helper returns. Induction on the list then handles the take branch and the skip branch together.

A one-line rewrite with a loop invariant

Some rewrites are short and their proofs are not. The reference for SquareRoot (verina_basic_65) increments a candidate root until its square exceeds the input. The rewrite calls Mathlib's Nat.sqrt and runs 21.16× faster. The proof shows, by induction on the remaining bound, that the loop returns Nat.sqrt N whenever the candidate is at most the root and the root is at most the candidate plus the bound.

5Results on 189 Verina functions

We use each of the 189 reference implementations in Verina as f and ask for a faster f′ with a proof of f = f′ over the inputs that the task's precondition admits. Verina's formal specifications are not used. Each function receives an isolated optimizer invocation (Codex with GPT-5.6 Sol at the xhigh reasoning setting), and the 54 functions whose first candidates were not faster receive one fresh retry. The timing corpus contains 49,620 generated and official inputs and is fixed before optimization, and each comparison uses nine paired trials pinned to one CPU.

Agents reach a faster, provable implementation in several ways. They reuse verified library algorithms, as in the SquareRoot example. They exploit properties of the problem: the rewrite of majorityElement returns as soon as one count exceeds half the list length, and its proof shows that the counts of two distinct elements sum to at most the length (3.74×). They change the representation and keep the control flow: the rewrite of nthUglyNumber performs the same steps on an array instead of appending to a list and indexing into it (124.90×), so its proof only relates each array to the list it represents.

The 33 functions without an improvement have proved candidates, but each candidate is slower than its reference. They are small arithmetic and comparison routines with little work to remove, such as Abs and minOfThree, and sorting routines such as insertionSort and mergeSort. On these functions, the remaining challenge is finding a faster implementation, not proving it.

6Aqueduct: real applications in native Lean

Lean is a general-purpose programming language, not only a proof assistant, but few real-world applications are written in it. Repository-level optimization needs such applications, with their callers and workloads. Aqueduct is an agentic framework that migrates C, C++, Go, and Rust programs into native Lean and checks each port against its original through differential testing . The original program is an executable oracle, so a port can be compared with it on any input without a written specification. The port may not call the original through a foreign-function interface or a subprocess.

Agents do the work that requires judgment, and a controller makes every decision on the evidence. Agents write ports and tests, and the controller selects ports and accepts a fix only if it repairs a failure without breaking a passing test. Part of the evidence is withheld from the repair agents, so every fix is checked on tests its author did not see.

We apply Aqueduct to 40 repositories from ProgramBench , which supplies pinned programs with hidden end-to-end tests. They range from 258 to 1,524,580 source lines and include archivers, compression libraries, build systems, code analyzers, and geospatial tools. As a baseline, a single migration agent with the same model produces a port directly.

On nine repositories, the single agent's port passes none of the tests, while the Aqueduct port recovers between 61.10% and 100%. On the other repositories where Aqueduct improves, the single agent already reproduces the common core of the program, and the additional tests come from rare option combinations, malformed and boundary inputs, exact diagnostics and exit codes, and environment-dependent behavior.

The ports are substantial native Lean programs. They include the Ninja build system, which passes 1,696 of its 1,750 hidden tests, the pigz compressor (827 of 857), and the Doxygen documentation generator (89 of 89). The 7zip port, from 252,968 source lines, handles ZIP, TAR, 7z, bzip2, Zstandard, LZMA, CPIO, RPM, ISO-9660, and CAB archives, among others, and recovers 554 of its 883 hidden tests.

7Results on applications: faster functions, smaller end-to-end gains

The repository-level study covers 17 Aqueduct ports, from command-line utilities to a build system and a documentation generator, with three application scenarios each. A separate agent builds the function-level and application-level workloads from the public entry points before optimization, and these workloads are withheld from the optimizer. The optimizer inspects the source and call structure, selects total functions without I/O effects, and proves each rewrite equal to the Lean reference it replaces.

The rewrites follow three patterns. The examples below are from the paper's case studies.

The function-level gains survive integration but shrink. The optimized applications are faster in 47 of 51 scenarios and in all 17 repositories by their per-repository geometric mean, but the 1.120× application-level gain is far below the 1.864× function-level gain. An application speedup is bounded by the share of scenario time spent in the rewritten functions, and the rest of each scenario, including its I/O, runs unchanged. Because each integrated rewrite is proved equal to the declaration it replaces, the optimized applications compute the same results as the migrated ones. Choosing which functions to optimize, and when to rewrite a shared data representation instead of a single function, is therefore a central part of repository-level optimization.

Faster than the original programs

The Lean ports are mostly slower than the native programs they came from. The optimized functions run at a geometric mean of 0.235× the speed of the matched operation in the original program. Yet 15 of the 92 optimized functions run faster than the original, compared with 12 before optimization (Figure 9). The original programs perform some of the same avoidable work that the agent removed. Cheat's Go code builds a complete consolidated list before searching it for one title, and the proved Lean rewrite, which searches directly, runs 20.36× faster than the matched Go operation. Hoisting the tag normalization in filterSheets takes the Lean function from 0.37× to 2.01× the speed of the Go original, the rewrite of Gron's validIdentifier runs 2.10× faster than Go, and Code Minimap's pow10 fast path runs 1.37× faster than the Rust original.

Widely used open-source programs therefore still leave room for optimization, and each rewrite above comes with a proof that it preserves the behavior of the code it replaces. Bringing the same guarantee to code that runs in its original language needs a Lean model of that language. For Rust, Aeneas translates programs into pure Lean functions, so an optimized Rust function could be proved equal to its original through their Lean models.

8What comes next

• Dividing effort between implementation and proof. Compare optimizing before proving, proving after each change, and interleaving the two under matched time and token budgets.
• Reusing proofs. The Gron proof above reused lemmas from an earlier rewrite. Comparing fresh proof search with access to earlier lemmas, within and across repositories and as applications change, would measure the value of such reuse.
• Selecting targets. Compare selection from source inspection with selection from profiles, and single-function rewrites with module-level rewrites of shared representations.
• Opaque effects. File and network I/O are outside the current task. Modeling them behind an interface of primitive operations would bring the I/O paths of applications into scope.
• Optimizing below the source level. The equality obligation does not depend on the level at which f′ is written, so a rewrite could target explicit memory layouts or vector instructions, with a proof that the compiled artifact implements f.

✎Citation

@misc{ye2026agentic,
  title  = {Agentic Verified Optimization of Real-World Software},
  author = {Ye, Zhe and Ghai, Udaya and Qin, Zhizhen and Song, Dawn and Kong, Soonho},
  year   = {2026}
}

References

1. A. Shypula et al. Learning Performance-Improving Code Edits. ICLR 2024.
2. A. Ouyang et al. KernelBench: Can LLMs Write Efficient GPU Kernels? ICML 2025.
3. S. Liu et al. The Time is Here for Just-in-Time Systems: Challenges and Opportunities. arXiv:2605.24096, 2026.
4. E. W. Dijkstra. The Humble Programmer. Communications of the ACM 15(10), 1972.
5. R. Shah and R. Shrestha. A Contract-Grade Verifier for LLM-Generated GPU Kernels, and a Native Blackwell Backward for the Gated-Linear-Recurrence Family. arXiv:2608.12700, 2026.
6. T. Hubert et al. Olympiad-Level Formal Mathematical Reasoning with Reinforcement Learning. Nature 651, 2026.
7. Z. Z. Ren et al. DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition. arXiv:2504.21801, 2025.
8. Y. Lin et al. Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction. ICLR 2026.
9. G. Tsoukalas et al. Advancing Mathematics Research with AI-Driven Formal Proof Search. arXiv:2605.22763, 2026.
10. Anthropic. Formalizing Fermat's Last Theorem. 2026.
11. G. Chen et al. ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization. ICLR 2026.
12. N. Patel et al. MathAtlas: A Benchmark for Autoformalization in the Wild. arXiv:2605.14061, 2026.
13. A. Bastounis, F. Circelli, and A. C. Hansen. Navier-Stokes Lost in Translation: Why Lean Verification of AI Autoformalisation Does Not Guarantee Correct Natural Language Proofs. arXiv:2610.08144, 2026.
14. M. Endres et al. Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions? FSE 2024.
15. Z. Ye et al. Vero: Can AI Agents Build Formally Verified Software Repositories? arXiv:2608.13522, 2026.
16. S. Ho and J. Protzenko. Aeneas: Rust Verification by Functional Translation. ICFP 2022.
17. L. de Moura and S. Ullrich. The Lean 4 Theorem Prover and Programming Language. CADE 2021.
18. The mathlib Community. The Lean Mathematical Library. CPP 2020.
19. Z. Ye et al. VERINA: Benchmarking Verifiable Code Generation. ICLR 2026.
20. W. M. McKeeman. Differential Testing for Software. Digital Technical Journal 10(1), 1998.
21. J. Yang et al. ProgramBench: Can Language Models Rebuild Programs From Scratch? arXiv:2605.03546, 2026.