A new software engineering paradigm – Blog

In this post, I’d like to collect some thoughts on what I believe is a new paradigm in software engineering. It is feasible today, and my colleagues and I have used it successfully over the past two weeks. In short, the paradigm combines formal verification and AI :

Humans specify what they want the software to do in a formal language such as Lean.

AI writes the software and a formal proof that it adheres to the specification. The proof is machine-checkable, eliminating the need for human review of the generated implementation.

AI by itself suffers from the review bottleneck

I believe that this combination of formal verification and AI is much more effective than AI by itself. The reason is code review. Even if agents can write code at near-zero marginal cost, reviewing all that code becomes the new bottleneck.

So why not YOLO it and drop review altogether? In some domains, that might be fine. But for most codebases, AI would have to get a lot better first. The way I think about it, AI may now be roughly on par with a single human at writing code. A single developer can maintain quality, but cannot scale; human teams scale by distributing the work and using code review to keep quality high. AI scales the writing without scaling the reviewing, creating a bottleneck.

Note that I am not talking about airplanes here. Lots of “ordinary” software isn’t critical enough to need formal verification for its own sake, but it is critical enough that you don’t want to YOLO it either. The key point of this post is: formal verification is a means to use AI more effectively . The increase in assurance is almost a side effect.

Eliminating the review bottleneck

The formal verification + AI approach can eliminate human review of generated implementation code in two ways. First, assuming the specification captures the intended behavior, you don’t have to worry about correctness of the code. Second, if the code is entirely managed by AI, its maintainability and human readability become less important.

The general framework is as follows:

Humans define the hard constraints : These are the required properties of the software, expressed as a formal specification. Usually, they capture some notion of correctness.

Humans define the optimization objectives : Benchmarks measure what the code should optimize for. Obvious examples include runtime and resource usage, but the objectives can also include hard-to-formalize properties that can be tested experimentally.

Agents write the code and proofs : Every proposed change comes with a formal proof that the software satisfies the hard constraints. Benchmarks also run automatically for each change and measure the optimization objectives.

One special case of this framework is Andrej Karpathy’s autoresearch project, which searches for better machine learning algorithms. Its primary acceptance signal is a soft goal: model performance on a validation set. Useful model quality is difficult to specify exhaustively as a hard constraint, so empirical measurement is the natural driver in that setting.

The point of this framework is that little human effort is needed to evaluate each generated implementation change. Hard constraints are proven to be met by the agent. Optimization objectives are measured automatically. If there are several objectives, a human may still need to choose among tradeoffs—what if quality improves, but runtime also increases?—although even that could potentially be automated.

Aside: Analogies to machine learning

Before I worked in applied cryptography, I was a machine learning engineer building tools to segment 3D image data. The analogies between this approach and machine learning are striking:

Because the agents can see the benchmarks and repeatedly optimize against them, the benchmarks are essentially the training set. Each one can be labeled, i.e., come with a desired output, or unlabeled.

Overfitting is a risk of this approach. We want the resulting algorithm to also perform well on inputs outside the training set.

One way to mitigate overfitting is to give instructions like “try to write general passes” or “don’t add a new pass, generalize an existing one”. It’s a form of regularization.

Asking agents to optimize a metric resembles reinforcement learning. For example, our circuit optimizer performed poorly on one metric simply because I hadn’t told the agents to optimize it. A poor reward design!

More generally, specification gaming is a serious issue. We did catch an agent exploit a weakness in the spec.

And, of course, we no longer understand the implementation. We measure how well the software works in practice, but we also get a proof that it satisfies the formal specification. That is stronger than the usual machine-learning setting.

A Hello World example

Suppose we wanted to implement a function that returns the k-th smallest element of a list of integers. We’ll start with Lean definitions that...