Are formal methods cool again?

A look at whether LLMs can make formal methods more practical for everyday software engineering.

Certain things become more accessible when the surrounding tools and technology change (e.g aerial photography).

Formal methods are having a weird comeback

Recently I came across some very interesting articles, talks and discussions about renewed interest in using formal methods in software engineering. The core idea of a lot of them was connected to utilizing LLMs (Large Language Models) to lower the entry barrier for formal approaches in software, and also regarding the use of formal methods as an alternative approach to verify the correctness of the increasing amount of AI-generated code.

In this article, I want to explore some of these ideas and also share a bit of my experience dabbling around in this space at a very basic level.

What formal methods actually mean

Although you might already be familiar with formal methods, I think many software engineers (including me, when I first heard about them) might not have a clear idea of what they are. This is understandable because most of these methods were not widely adopted by the broader software engineering community, for reasons we will go into shortly.

Basically, formal methods are mathematical techniques used to specify, analyze or verify that systems work as intended. This is different from regular software testing, where we evaluate the system under a specific predefined set of inputs and expected outputs.

These formal techniques can roughly be broken down into three areas:

• Specification: precisely stating what the system should do by defining it as a formal model.
• Analysis and verification: checking whether a model or implementation satisfies the properties stated in its specification. Two major approaches for this are:
  1. Model checking: automatically exploring the possible states of a model to find whether a required property can be violated.
  2. Theorem proving: using mathematical logic to construct a proof that certain properties hold (spoiler alert: very complicated).
• Development and refinement: using formal models or specifications to guide the design or implementation itself.

Why they were not widely adopted

As mentioned earlier, formal methods were not widely adopted by the industry. In fast-paced agile cycles, the cost of building with regular testing, and even taking into account bug fixes and rework, can often be cheaper than the time spent learning and applying formal techniques.

For many general use cases, testing was considered good enough. And for many teams, it is questionable whether the return on investment is worth the time spent on learning, training and adopting these approaches.

There is also a cultural gap since most engineers are comfortable thinking in familiar ideas like entity relationships, APIs, services etc. Formal methods often force to think with a more abstract mindset and uses more math heavy terminology and concepts.

Tooling and ecosystem maturity also matter. Compared to mainstream development stacks, the tooling for formal methods can feel dated and less familiar to get into.

Why LLMs change the picture

The first time I noticed renewed interest around this topic was through Martin Kleppmann’s article, “Prediction:AI will make formal verification go mainstream.” Martin, the author of the famous Designing Data-Intensive Applications, argues that LLMs can make formal verification more economically viable. He also makes the point that LLM-generated code intrinsically creates more need for verification, because human review may not scale well enough if we are generating more and more code with AI.

His article mostly focuses on theorem proving based formal verification and he explained this idea further in a recent, very good interview with Gergely Orosz, including the point that the main blocker to this shift may be more cultural than purely technical.

I also came across other discussions around this. Hillel Wayne, who writes a lot about formal methods and TLA+, has written about AI being useful for TLA+ users, especially for reducing friction and helping with the more mechanical parts. Further, in a recent WSO2 Technology Conference talk, Srinath Perera discusses possible use cases for AI in formal verification in a proposed autonomous/semi-autonomous software development lifecycle (ASDLC), particularly using LLMs to generate code in formally verifiable languages.

So based on these signals, it seems experts are starting to question whether LLMs can make formal methods more practical, and also whether the rise of AI-generated code makes stronger correctness techniques more necessary.

Formal specification may be the practical starting point

For general software engineers, formal specification along with model checking may be the more immediately useful and approachable entry point than theorem-based formal verification which is powerful, but also very complex. Writing proofs and verifying implementation-level correctness is a whole different skill set, and honestly not something I know about to cover properly here. However, it may become more viable with AI, and I think it won’t hurt to keep an eye on where that goes.

On the other hand, specification combined with model checking feels like a good place to start. It lets us model a system at a higher level and reason about its behavior before getting lost in implementation details.

So when I started searching around on formal specs, one of the most talked about tools I came across was TLA+ which was created by Leslie Lamport, who is well known for his seminal work in distributed systems theory including Paxos. TLA+ is a formal specification language often used to model systems, especially distributed systems and concurrent systems. At a simple level, it lets you describe the state of a system, the actions that can change that state, and the properties that should hold. There are also notable industry use cases around TLA+. Companies such as AWS, Microsoft, MongoDB and Oracle have used TLA+ in practice with benefits, including the discovery of subtle, critical bugs in their systems.

Dabbling around

Before getting too much into the AI aspect, it is useful to first have a very basic idea of what a TLA+ spec is. A TLA+ spec is not like normal application code. Instead, we are writing a model of how the system is allowed to behave.

A simple way to think about it is as a state machine. We define the important variables in the system, the initial state, the possible actions that can change that state, and the properties or invariants that should always hold. Once we have that model, the TLA+ model checker can explore the possible states and check whether any of those defined properties can be broken (i.e indicating a bug/problem in our defined model).

This is also different from normal testing, where we usually test some predefined flows, inputs, and conditions (test cases). With model checking, we define the rules of the system and let the tool explore the different states and possible orders that can happen from those rules, which is where some surprising cases can appear.

I started playing around with TLA+ using AI as a supporting tool to teach myself the basics, in addition to the usual docs and other resources. These days, chatting with an AI assistant has become one of my go-to learning methods whenever I want to get familiar with a new topic.

I wrote mostly very basic specs for simple cases. But even in these cases it was harder deciding the states, what actions can change them, what should be abstracted away, and what should always be true than the actual syntax. LLMs were most useful here by reducing the boilerplate and syntax overload, especially as TLA+ uses mathematical notation and first principle concepts, and not the programming language primitives we are most familiar with. That gave me more time to think about the model than fighting with syntax.

I also tried generating specs using natural language problem statements or descriptions, but it was not as smooth as regular code generation (for now). With general coding, for example a web app, LLMs are often very fluent because the patterns are common. With TLA+, I had to refine prompts more, provide docs as context, ask it to do background research and review the output carefully.

So my current feeling is that LLMs can reduce the friction a lot, especially when learning and drafting. But thinking about the problem, choosing the right abstraction, coming up with the right states and transitions, and identifying subtle invariants still requires human judgement.

Why bother?

Lamport says we should think before we code (today this might be better worded as ‘think before you prompt’ :)). That sounds obvious at first glance, since in most engineering work we already do planning and design in some form. But even with design documents, diagrams and discussions it is easy to miss things when the problems and solutions get larger and more complex. Even if we keep the AI angle aside for a moment and even if we do not actually write formal specs, writing some kind of specs informally for a system seems like a great exercise. It forces a switch from our usual procedural-oriented thinking into reasoning about states.

For example, think about something like a payment processing and order dispatch flow. In code, this might be spread across API endpoints, payment provider callbacks, database updates, background jobs, and dispatch workers. But at the specification level, we can step back and ask what the possible states are. Is the order placed, payment confirmed, ready to dispatch, order cancelled, or refunded? What transitions are actually allowed between those states? Can an order be dispatched before payment is confirmed? Can duplicate callbacks or retry jobs cause duplicate dispatches? What happens if dispatch fails after the payment is confirmed?

This kind of declarative writing makes you think about edge cases that are easy to miss when jumping directly into implementation. You improve the ability to abstract away the details and reason about the core variables and properties of the system at the level you are interested in. Similar to zooming in and out of a picture.

So what’s the catch?

However it is important to keep in mind that this is not a silver bullet. For many tasks, normal design practices, testing, code review, and observability are enough. But there are areas where formal specification can be very useful: any sort of distributed systems, concurrent workflows, flows with locking, retries, idempotency, scheduling, resource allocation and more, basically when the number of moving pieces becomes hard to reason about manually.

AI is not always good at some aspects of specs and model checking. In a counter-argument article for his earlier article mentioned above ,“LLMs are bad at vibing specifications,” Hillel Wayne points out that LLM-generated specs can look convincing but still miss important nuances. At the same time, he correctly warns it may still be too early to make final judgments due to the rapid improvement of models.

Some final thoughts

It is clear that LLMs do not suddenly make formal techniques a piece of cake, and not all problems we tackle daily will benefit from them. But I do think formal specification deserves more attention from the general software engineering community, especially now that AI can reduce the barriers to entry.

Catching problems upfront will not be the only advantage. It also changes the way we think about systems and problems. I think that mindset shift will come in handy in a lot of places, even if one never goes very deep into or actually implements formal methods.

Also for anyone curious to explore further, TLA+ itself seems like a good starting point, especially if you are interested in specification and model checking based approaches, particularly relating to distributed systems.