Formal verification might solve AI's review bottleneck

A new software engineering paradigm – Blog

Circuit has a notion of equivalence. The optimize function is correct if the output circuit is equivalent to the input circuit. For example, the identity function would be a correct optimizer. A circuit also has a measurable size. A good optimizer reduces that size significantly.

This maps cleanly to the framework above: optimizer correctness is a hard constraint; circuit-size reduction and optimizer runtime are optimization objectives. The apc-optimizer repository implements this framework and is set up as follows:

Around 500 lines of Lean specify exactly what it means for an optimizer to be correct. The core is Spec.lean, if you want to get a feel for it. Writing the specification took around two days, plus a day of review by team members.

We check in a few relevant benchmarks. Those are real-world input circuits for which we care about optimizer performance. A benchmarking script measures both the quality of the optimizer and the runtime.

When a PR is opened, CI (1) applies a label if only a whitelisted set of files was touched (which excludes all of the specification and benchmarks), and (2) runs the benchmarks and posts the result into a comment.

In practice, “reviewing” an AI-generated implementation PR consists of checking for the label and skimming a comment like this. AI agents have written 100% of the optimizer implementation and its proofs with minimal guidance. We do not review the generated code at all. In fact, I barely know Lean.

Results: Circuit-size reduction is on par with our previous implementation; see this comparison across a suite of benchmarks. The agents were asked to optimize only a subset of these benchmarks, so the results on the others are evidence that the optimizer generalizes. Runtime is still slower than that of our Rust implementation, but it has not been a priority so far, and we are confident that it can be improved. Our slowest test case became more than three times faster in the last three days.

Integration: We have integrated this code into our main codebase as an alternative to our existing Rust implementation. Lean can be compiled to C, which is then invoked from Rust via FFI.

For more information about this specific use case, see our blog post on formally verified autoprecompiles.

What this means for software engineering

On a personal note, it has felt overwhelming to rebuild a core component of our main product in just a week or two. I think many software engineers feel both overwhelmed by what AI can do today and underwhelmed by how much faster it lets them ship. I believe the review bottleneck described above explains much of that gap. Formal verification can close it.

The key question, of course, is how widely this approach applies. That remains largely an open question, and I hope this post sparks discussion. Here are a few thoughts:

For the approach to deliver a meaningful speedup, writing and auditing the specification must be substantially cheaper than writing and maintaining the implementation.

Reusable libraries of concepts would help. For example, most web backends have some notion of user accounts, access rights, and databases. Just as we now reuse software libraries, we could reuse specification libraries.

Thanks to FFI, we can introduce AI-generated, formally verified code one module at a time without rewriting the entire codebase. Even if the approach applies only to certain components, it can still be valuable there. In our case, we used it only for the optimizer.

Ultimately, software development might no longer be about code, but about requirements. Critical properties would be specified formally; everything else could be expressed through prompts and validated through automated and manual testing. We might never see the generated code—or even know the programming language it was written in.

For various discussions around this subject, I’d like to thank Leandro Pacheco, Leo Alt, Jonathan Striebel and Arne Binder.