Agentic Verified Optimization of Real‑World Software

Speedups 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. Verified compilers such as CompCert and superoptimizers such as STOKE already optimize with this guarantee, but only through passes proved correct in advance or over short instruction sequences, so they find only what those transformations can express. Coding agents are not limited to a fixed set of transformations: they can propose new algorithms and data representations. With a proof as the check, an agent can change both freely, and the correctness requirement stays the same.

Why 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: specifications are hard to write correctly , and even curated ones contain errors . In a recent large-scale verification effort, an example specification taken from a fuzz test checks only the length of the decompressed output, not its bytes .

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.

The 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.

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.

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.

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.

Example: 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, so it does quadratic work. On its 261 timing inputs, the rewrite runs 4,468× faster.

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.

Results on 189 Verina functions

We use each of the 189 reference implementations in Verina as f and ask the agent for a faster f′ with a proof of f = f′. Verina's formal specifications are not needed.

Agents reach a faster, provable implementation in several ways. They reuse verified library algorithms: the rewrite of SquareRoot calls Mathlib's Nat.sqrt instead of counting up to the root (21.16×). 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.

Aqueduct: 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.

Agents do the work that requires judgment, and a controller makes every decision on the evidence.

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. Aqueduct's ports pass 87.68% of the hidden tests that the original programs pass, compared with 68.17% for a single migration agent.

The ports are substantial native Lean programs, including the Ninja build system, the pigz compressor, the Doxygen documentation generator, and a port of 7zip from 252,968 source lines that handles ZIP, TAR, 7z, bzip2, Zstandard, LZMA, and other archive formats.

Results 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. The agent inspects each application, chooses which functions to rewrite, and proves each rewrite equal to the Lean function it replaces.

The rewrites follow three patterns.

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. Lean code runs on a reference-counted runtime in which many values are boxed and allocated on the heap, and the source language gives no control over memory layout, unboxed representations, or vector instructions, which native C, C++, Go, and Rust code uses directly. This gap can narrow as Lean's compiler and runtime evolve, and optimizing below the source level (What comes next) targets it directly. Even so, in 15 of the 92 functions, the optimized Lean code already runs faster than the matched operation in the original program, compared with 12 before optimization (Figure 8). 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.

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.

What comes next

• Dividing effort between implementation and proof. When to optimize before proving, when to prove after each change, and when to interleave the two.
• Reusing proofs. The Gron proof above reused lemmas from an earlier rewrite. Carrying lemmas across rewrites, repositories, and versions could make each new rewrite cheaper to prove.
• Selecting targets. Choosing functions from profiles, and rewriting shared data representations instead of single functions.
• Opaque effects. Modeling file and network I/O 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.
• Optimizing code in its original language. Aeneas translates Rust programs into pure Lean functions, so an optimized Rust function could be proved equal to its original through their Lean models.

Cite this work

@article{ye2026agentic,
  title={Agentic Verified Optimization of Real-World Software},
  author={Ye, Zhe and Ghai, Udaya and Qin, Zhizhen and Song, Dawn and Kong, Soonho},
  journal={arXiv preprint arXiv:2610.30188},
  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. X. Leroy. Formal Verification of a Realistic Compiler. Communications of the ACM 52(7), 2009.
17. E. Schkufza, R. Sharma, and A. Aiken. Stochastic Superoptimization. ASPLOS 2013.
18. J. Garvin. On the LZO fuzz-test example in a formal-verification report. Post on X, October 2026.
19. S. Ho and J. Protzenko. Aeneas: Rust Verification by Functional Translation. ICFP 2022.
20. L. de Moura and S. Ullrich. The Lean 4 Theorem Prover and Programming Language. CADE 2021.
21. The mathlib Community. The Lean Mathematical Library. CPP 2020.
22. Z. Ye et al. VERINA: Benchmarking Verifiable Code Generation. ICLR 2026.
23. W. M. McKeeman. Differential Testing for Software. Digital Technical Journal 10(1), 1998.
24. J. Yang et al. ProgramBench: Can Language Models Rebuild Programs From Scratch? arXiv:2605.03546, 2026.