Formal proofs have been fashionable in the recent months, after being at best an afterthought of the programming community for half a century. By formal proofs I mean writing mathematical statements and their proofs in a computer readable language such that a program (often called a proof assistant) can check that the proof indeed proves the theorem.

Formal proofs belong to the family of formal methods. A loose term describing all the computer-assisted methods to gain assurance about programs beyond mere types and tests. Formal methods have garnered quite a lot of interest of late because many want to generate more code with LLMs, and without constraint it’s really difficult to guarantee that the code does what you set out to do. Formal methods can, at least in principle, provide such guarantees.

Formal methods sit on a spectrum. On one end you have fully automated methods (such as abstract interpretation, model checking,…), which take a program and prove properties about the program on their own. Fully automated methods are necessarily limited both in the kind of properties they can prove, and on the programs they can prove it on. On the other end of the spectrum, you have formal proofs, which lets you prove any property you want, in the entirety of maths, you just have to do it all by yourself (and believe me, convincing a computer of a proof is quite an ordeal compared to convincing a human).

All formal methods incur a cost, until recently, most software projects came to the conclusion (rightly or wrongly) that they can’t recoup that cost. This sentiment is changing. Not only that, but there’s a sentiment that LLMs can be used to generate formal proofs, making formal proofs themselves much cheaper, giving you access to mostly arbitrary properties¹. Hence the interest.

As a certified formal-proof nerd (I have a true, bona fide, government-backed nerdiness certification called a PhD), I’m certainly curious to find out how grounded these hopes would turn out to be. So I got myself a company LLM account, and set out on a little project to form an opinion of my own. I don’t know if it’s entirely fair to make a pronouncement about the entire discipline based on a single small-scale experiment, but I have to be honest: this is what this blog post is.

TL;DR While I find the capability of LLMs to generate formal proofs very promising, I’m not convinced that code generation constrained by tight specification is a very good or efficient way to program (at least not in its absolutist sense where most of the code is generated by an LLM).

What I did

Specifically, I wanted to test the maximalist proposition of me writing only specifications, and let the LLM generate all the code (I allow myself to write a tiny amount of code, mostly types), and to write all the proofs itself. There are, of course, a lot of potentially less maximalistic ways to use this combination of technologies (see for instance this successful attempt at optimisation). But the maximalist approach seemed like the fastest way to get an overview of a variety of scenarios.

To that effect I decided to build a tiny SAT solver. Because it’s small enough while being non-trivial. And because I mostly knew what I wanted to get, but it’s also not something I’m seasoned at building. I thought it was a realistic middle ground. And it has decently clear specification, which gave the project a good chance of success.

I wrote all of this in a single proof assistant² (Lean is quite popular these days, but I picked Rocq since it’s been my tool of choice since long before Lean was even an idea). I assume that a more realistic situation if we ever use proof assistant for code generation is to have the program in one language and the specifications and proofs in another. But there aren’t really any mature system to program this way today. So I didn’t want to get into this particular can of worms. To simulate the more realistic situation, though, I tried as much as possible to separate implementation and specifications in different files.

What I found most remarkable

I’d like to start with what I feel worked best, because I truly learnt something. Well, I suppose I already knew it somewhere deep down; but it was unconscious and I couldn’t voice it.

Here’s the thing, LLMs appear to be pretty good at writing formal proofs, and one of the tools that they use and in which they differ significantly from traditional automation methods is that they act non-locally. An LLM seeing an error message will often realise that a lemma is missing somewhere else, and they will go and add them, including behind an abstraction barrier. Traditional automation just gives you the error message, and you have to go and create the additional lemma on your own.

Before doing this little exercise, I had never consciously realised the mental tax caused by having to jump to another file to add a trivial lemma. Whether it’s via LLMs or via dedicated tools, this non-local automation is something that formal proof workflow desperately needed. So I was impressed.

Admittedly, the same is true of regular programming, to some degree. Having to switch file and add an extra function to an abstract data type is rather costly, and non-local code generation is certainly a contribution of LLM-backed coding agents. It’s just a bigger burden, and so a bigger relief, in formal proofs.

Speaking of, one of the biggest costs of formal proofs is proof maintenance. When a program changes a little, proofs about its correctness need to change. A small change, say, in a data type, can ripple through many proofs. And since proofs are traditionally much more expensive than implementation, the cost of change is that much bigger. It’s quite time consuming, and often painful to us humans to go through the proofs one by one and fix them. This is something else LLMs are rather effective at. You change a bit of code, they will propagate that change and fix your proofs. It really relieves the tension between writing the program you want and keeping your correctness proofs.

And, on the other hand, when an LLM convinces itself that something can’t be proved, it will cook up some counterexamples for you to figure out what you got wrong. The explanations have been quite good in this project. Plus, these are interactive, you can prod further if you need more. This is a form of realisation of the long dream of having interactive compiler errors (especially useful here because figuring out why you can’t prove something is often just as hard as understanding why you can). I’ve been rather impressed honestly.

What I found most amusing

Ok, so, this is only a side note, but LLMs have a very unusual way of writing proofs. First they guess an entire proof, and only then they will run the compiler. The first guess will almost always be quite far from an actual proof. And only in the second step will it start mutating to converge to an actual proof. Mutations are sometimes fairly local, and sometimes involve more guesses about future goals.

There’s nothing necessarily wrong about this approach. It’s just very alien to us humans. And I admit that I’m quite easily amused.

What it wasn’t

Here’s the thing. I don’t think that programming this way ends up being faster than programming by hand. To be specific, it’s been considerably faster than writing a program with its proof by hand, but not than writing a program alone.

There are a number of obstacles there. First, writing specifications is hard. Not everything has a clear specification, but even when it does, the specification can be quite complex.

In the case of a SAT solver, the SAT solver itself has a simple specification, the parser and CLI don’t really admit a specification, and the main invariant (which is required to prove the SAT solver’s specification) is about 50 lines long.

I got it wrong, forgot some bits. The agent takes a long time to prove, or fail to prove. We iterate. It takes time.

The other thing is that specifications are partial. Most of the time you don’t fully specify the functional behaviour of your functions, but even when you have a full functional specification, it doesn’t capture the algorithmic aspects of the function. So you still have to read the generated code quite carefully, and it’s really hard to get a good feel of what’s going on in code you didn’t write.

This is compounded by the fact that an LLM-backed agent will try to sneak every possible trick past you: it will mess up algorithmic features of a function if it helps it prove something, it will alter your specification, pierce your abstractions, assume lemmas as axioms instead of proving them. Once it even fully duplicated my program in order to avoid having to prove a refactor correct!

Generally, current coding agents have exceptionally bad taste, they will produce awful, slow code, suggest the wrongest possible fixes. Their output needs to be monitored quite carefully, and no amount of formal methods will meaningfully improve that.

A recommendation (that, admittedly, I didn’t apply to myself in this project): auditing lemma statements lost in a sea of updated proofs is very difficult, your eyes will skip past it more often than not. But you need to audit them because they will change, either because the program changed and the lemma needs to be adjusted, or because the agent is trying to be sneaky. So if you ever find yourself letting a coding agent do the proofs for you, try and make sure that the statements you truly care about are visually isolated – with at most trivial proofs – so that their changes stand out.

So in the end, I would have probably got to a finished product faster had I programmed it by hand. Even as someone who did proofs of programs for my PhD. But it’s a very different experience than writing a program by hand, so some of us might like it better. And you get the added benefit of having some formal proofs to go with it.

Automation is still relevant

LLMs, as it happens, are both quite slow and quite expensive. Formal proofs currently stress both. To give some idea, I almost always burnt through my weekly allowance of tokens in under two days’ work; once it just took until the middle of the afternoon of a single day to spend a week of credits³. I tried using a cheaper model, but the results were disastrous, formal proofs with LLMs currently still seem to require some of the most high-powered models.

Generally speaking, bespoke automation will almost always be faster and cheaper than a generic automation. The strength of coding agents is their generality: they are capable of making progress on any sort of problem. Their ability to both non-sequentially and non-locally directly affect the text of the proof gives them a flexibility that most automation doesn’t have.

But they will spend your time and money doing that. So an agent, to me, seems to be at its best when it has many tools to orchestrate. A powerful automation will let the agent skip a lot of steps; bespoke automation tools are also more robust to refactors, which can help a tonne.

What is lost

Throughout this project, I was struck by how little I understand the code or the proofs (though admittedly, I gained quite a bit of understanding of most, not all, of the implementation via the process of writing the specification, and responding to proof failures; the proofs though, I’ve long since lost track).

One way in which it manifests is that I couldn’t intervene when proofs were taking a long time. I didn’t know if it was taking time because the agent was getting lost. I didn’t know if it was taking time because the proof were badly engineered and what I could do to improve that. I didn’t get a feel for what was happening at all. So I couldn’t build automation⁴ to help proofs be more robust, or easier to deal with, because I didn’t know what took the agent effort. On a different axis, maybe with some understanding I could have avoided having a 7000+ line-of-code proof file and saved a lot of tokens, but I genuinely don’t know what’s going on in there.

When you program or prove by hand, if you’ve done something wrong, you’ll feel the pain of having to work in a badly designed setting. This pain, in turn, will both cause you to seek ways to reduce the pain and tell you what part of the systems are the problem. With coding agents, the cost remains. In fact it’s my experience that what humans need and what LLM-backed coding agents need to be effective is quite similar (small, limited-responsibility, well-isolated units).

But the pain is missing. And I don’t know what to replace it with.

Conclusion

I’m really not convinced that code generation constrained by formal proofs is the future of programming. There are too many challenges, and it’s not even that efficient. But I want to reiterate that fully generating the code isn’t the only way that you could plausibly use an agent in conjunction with formal methods.

If you already have formal proofs in your program, I think it’s rather clear that coding agents help refactoring quite significantly. A rather extreme example can be found in this blog post from Nik Swami, where an entire verified garbage collector was ported from one version of F* to another. It appears to be still quite labour intensive. But considerably less so than a manual port would have been.

But formal proofs can’t been seen as a panacea. They don’t fully specify your code (if anything because they don’t specify the algorithmics of your code). And this means yet another cost: writing specifications requires expertise, and this expertise doesn’t replace the programming expertise. Both are required (conflict of interest declaration: I obviously have services to peddle).

However, I think that the evidence is pretty strong that formal proofs are getting cheaper. Not necessarily cheap, but noticeably cheaper (see also this experiment, which is much more seriously conducted than mine). And if formal proofs really do become cheaper, it means that it will become reasonable to use them for applications where it would have been unthinkable a few years ago. Isn’t that exciting?