I used formal verification and agents to make an algorithm 105× faster and prove it behaves the same

[ 2026-09-24 ] // Claude Opus 5.5 · Dafny 4.11 // 7 MIN READ

Across four deliberately slow Dafny routines, Claude Opus 5.5 produced seven faster implementations, each verified against a frozen specification it could not edit. On a held-out run-length encoding workload it never saw, the accepted version ran 105× faster. Held-out workloads also caught small-input slowdowns the acceptance gate could not see, and failed proofs, not the speed gate, ended three of the four runs.

Setup

Each routine is a pair of Dafny files. Dafny is a programming language with a built-in program verifier: you write code plus statements about what it must guarantee, and a solver checks them for every possible input. Spec.dfy holds the contract and is frozen. Impl.dfy refines it and starts deliberately naive. It is the only file the agent could change.

For sorting, the whole contract is two lines:

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

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

Claude ran through the claude -p CLI with read and edit tools on a scratch copy. It 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 then applied four checks in order:

1. Reject the candidate if Spec.dfy changed by a single byte, or if 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 limit. On failure, send the errors back, for up to three attempts per round.
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 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. Each routine also had held-out workloads with different sizes and shapes. Their outputs were checked in step 3, but their timings were only reported afterward, never used for acceptance.

Accepted changes

Each speedup is the naive median time over the new median time, from seven repeats. About $12 of the $18.12 total was one failed popcount round.

On sort, the agent replaced insertion sort with a top-down merge sort and wrote the loop invariants Dafny needed to accept it. The first proof attempt passed. On RLE, the naive version rebuilt its output for every element. The accepted version finds where each run ends and appends the whole run at once, and it also verified on the first attempt.

Held-out workloads

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

Range runs from slowest-before over fastest-after to fastest-before over slowest-after. The five-element-list result at 1.07× is not a difference the timing noise can resolve.

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, which ends at 0.76× against the naive start. A proof fixes behavior. It does not fix speed on every input.

ISqrt round 3 hard-coded a comparison tree sized to the search range, up to about 1.7×10¹⁰. It is still proven correct, but it is shaped around the benchmark.

Interpretation and limits

No accepted change broke its contract: each one verified against the unchanged spec and matched the naive output on every workload. The speed gate never rejected a candidate. Every early stop came from verification. RLE round 2 had real proof errors, but the final attempts for popcount and sort had no errors, only time-outs. Rerun afterward with a 300 s solver limit, sort round 2 verified and popcount round 3 still had one time-out. Sort round 2 stays rejected under the fixed rules and was never timed. So part of where each run stopped reflects the harness's proof budget, not the code.

Limits that affect the estimates above:

• Everything timed is Python compiled from Dafny, which adds runtime overhead. The final versions are still about 5× to 7000× slower than Python's built-ins (math.isqrt, int.bit_count, sorted) and, for RLE, itertools.groupby. Those run in C and show scale only.
• The baselines were deliberately slow, so large speedups against them say little about real code.
• One run per routine, with Claude Opus 5.5, the CLI's default model. The A/A noise floor (naive against itself) was within ±4% for ISqrt, popcount and RLE, but sort reached 0.84× on one workload, and another experiment may have been running on the same Mac.
• 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, nothing broader.

Next experiment

• Give the verifier a longer solver limit, such as the 300 s that let sort round 2 verify, and see where each routine stops.
• Add small and tiny inputs to the search workloads, or a no-regression floor for them to the gate, so slowdowns like ISqrt's 0.44× are rejected rather than reported.
• Require the whole min–max range above 1.0×, not just the median.
• Lengthen the ISqrt workloads before running more rounds.
• Repeat each routine several times, on an otherwise idle machine.

Reproducibility