Agents optimized four naive routines without changing their specifications

[ 2026-09-24 · updated 2026-10-23 ] // Claude Opus 5.5 · Dafny 4.11 // 9 MIN READ

This early pilot tested a workflow: an agent may change a routine's implementation, but every change must still verify against a frozen specification and is kept only if it runs faster. On four deliberately naive Dafny routines, Claude Opus 5.5 produced seven rewrites that passed every check: six known algorithmic improvements and one fitted to the benchmark, none of them new algorithms. On a workload the agent never saw, the run-length encoder ran 105× faster than its naive start, both compiled from Dafny to Python.

Setup

The hard part of letting an agent optimize code is trusting that the faster version still does the same thing on every input, not just those someone thought to test. The pilot asked whether an agent can change an implementation and its proof while the specification stays fixed, and whether its speedups hold on workloads it was not tuned on.

Each routine is a pair of Dafny files. Spec.dfy holds the frozen contract. Impl.dfy, the only file the agent could change, starts deliberately naive and refines the contract, meaning Dafny must prove it meets every guarantee in the spec.

For sorting, the whole contract is two lines:

ensures Sorted(b)
ensures multiset(b) == multiset(a)

The output must be in order and contain exactly the input's elements, with the same number of copies of each.

The agent edited a scratch copy and could not run Dafny or the benchmarks; it saw the spec, the current implementation, a description of the search workloads and the latest timings. A harness, the software that ran each round and kept the records behind the results below, then applied four checks in order:

1. Reject the candidate if Spec.dfy changed by a single byte or the implementation used an escape hatch: assume, {:axiom}, {:verify false}, {:extern}, {:only}, expect or decreases *.
2. Run the Dafny verifier with a 60 s solver time limit; on failure, send the errors back, up to three attempts per round. A time-out means the solver ran out of time, not that it found an error.
3. Compile to Python and check that the output matches the naive version on every workload, held-out ones included.
4. Time the search workloads with seven interleaved repeats, each in a fresh process. Accept only if the geometric-mean speedup (the average per-workload ratio, taken on a log scale) is at least 1.10× and no search workload falls below 0.95×.

Each routine got at most three rounds and stopped at the first rejected one. Held-out workloads had different sizes and shapes; the agent never saw them and was told only that other inputs existed. Their outputs were part of the correctness check in step 3, but their timings were only reported afterward and never used to accept or reject a change.

Who did what

A Claude agent proposed this experiment, and I asked for it to be specified and run. A Claude Opus 5.5 session wrote the plan, the frozen contracts, the naive starting code and the harness, reusing the structure of my earlier Dafny pipeline, and ran the loops; a fresh instance optimized each round. The four checks, not anything an agent reported, decided every acceptance. They take two things on trust: the contracts themselves, and Dafny's compiler to Python and its runtime, which step 3 checks only cheaply.

Accepted changes

Each speedup is naive median time over new median time (seven repeats). About $12 of the optimizer's $18.12 total was one failed popcount round.

Six of the seven accepted changes are textbook improvements (Table 02). The RLE rewrite appends each whole run at once instead of rebuilding the output for every element; it produced the 105× held-out result against the naive start and, like the merge sort, verified on the first attempt. The seventh, ISqrt's third round, was shaped around the benchmark (see Held-out workloads). The agent's work was choosing the changes and, harder, writing the loop invariants (facts that hold on every pass through a loop) and helper lemmas (small supporting proofs) that let Dafny prove them.

Because the starting points were deliberately slow, the size of each speedup mostly measures how poor the start was; ISqrt's naive version counted up from zero, so its numbers run into the thousands. Python's built-ins are still faster than every final version: about 5–20× for square root (math.isqrt), 90–7,400× for population count (int.bit_count), 10–14× for RLE (itertools.groupby) and 200–3,000× for sort (sorted). They run mostly in C, and Dafny's Python output carries runtime overhead, so this is not a fair race, but it shows what the pilot measured: progress from a naive start, not a win over production libraries.

Held-out workloads

Sort and RLE each had one accepted round, so Table 03 compares that round directly with the naive start.

The range is the widest spread the seven repeats allow, not a confidence interval. The 1.07× on five-element lists is within the timing noise.

The held-out sets also caught what the gate could not. ISqrt round 1, a binary search, ran tiny inputs (0 to 100) at 0.44× and was accepted, because tiny inputs were not a search workload; later rounds brought that to 0.97×. Popcount rounds 1 and 2 ran inputs below 256 at 0.92× and then 0.83× against their predecessors, ending at 0.76× against the naive start. A proof fixes behavior, not speed on every input.

ISqrt round 3 hard-coded a comparison tree sized to the search range, up to about 1.7×10¹⁰: proven correct, but fitted to the benchmark.

Interpretation and limits

The speed gate never rejected a candidate: every early stop came from verification. RLE round 2 had real proof errors, but the final popcount and sort attempts had no errors, only time-outs. Rerun afterward with a 300 s solver limit, sort round 2 verified (it stays rejected under the fixed rules and was never timed) and popcount round 3 still had one time-out, so part of where each run stopped reflects the proof budget, not the code.

• Everything timed is Python compiled from Dafny, against deliberately slow starting points; the speedups describe that setting, not hand-written Python or production code.
• Each routine had one optimization run, and repeated timing within it does not show how much a second run would differ. The A/A noise floor (naive against itself) was within ±4% for ISqrt, popcount and RLE, but sort reached 0.84× on one workload. A second experiment was started on the same Mac in parallel, so the timings may include interference.
• Popcount round 2 passed on median speedups of 1.47× and 1.57×, with min–max ranges of 0.78–1.93× and 1.09–1.97×. A rule requiring the whole range above 1.0× would have rejected it.
• Some ISqrt workloads now finish in microseconds, below reliable timing resolution.
• "Correct" means correct against these frozen contracts, with the Dafny-to-Python compiler trusted; nothing broader.

Next experiment

• Repeat the whole optimization run several times per routine on an idle machine, with many more paired, interleaved timings, so each speedup gets an uncertainty estimate instead of a seven-repeat min–max range.
• Start from stronger baselines, such as a standard algorithm already verified in Dafny, so a speedup measures more than replacing a deliberately slow start.
• Give the verifier a longer solver limit and see where each routine stops.
• Add small and tiny inputs to the search workloads, or a no-regression floor for them, so slowdowns like ISqrt's 0.44× are rejected rather than reported.
• Lengthen the ISqrt workloads before running more rounds.

Two later posts carry the same division of labor (agents change the code; a proof fixes what must be preserved) to a more realistic workload: code PyTorch's compiler actually generates. In A Lean proof let agents cut a compiled PyTorch workload’s runtime by 26%, agents moved one torch.compile GPU kernel's size arguments from 64-bit to 32-bit, and a Lean proof shows when that is exact; Agents turned a one-kernel Lean proof into a checker that certified 25 PyTorch kernels generalizes that proof.

Reproducibility