Quint is an open-source, executable specification language and toolchain based on TLA+ that enables engineers to model, simulate, and verify system behaviors using an intuitive, programmer-friendly syntax.
Ryan Donovan: Hello, everyone, and welcome to the Stack Overflow podcast, a place to talk all things software and technology. I’m your host, Ryan Donovan, and today we’re talking about formal verification for agentic coding using TLA+. My guest for that is Gabriela Moreira, the CEO at Quint. So welcome to the show, Gabriela.
Gabriela Moreira: Thank you, Ryan. Thank you for having me.
RD: My pleasure. Before we get into the formal verification topic, can you give us a little background? How did you get into software and technology?
GM: I started a bachelor in computer science in 2015. I think I had like two ways into software. One of them was because I was customizing my Tumblr themes and I liked changing the code and seeing how things switched in the screen. I thought it was really magical. And then I was a bit into gaming. My computer was not the best, so I had to troubleshoot a lot, and I enjoyed doing that. I was considering either doing mathematics or doing computer science, and I ended up doing computer science, but it was a really hard decision. The parts that I like the most about mathematics are the parts that we see in computer science, like discrete mathematics and graph theory. So that was nice. And then inside computer science, I liked compilers and computer theory. Eventually I was presented with formal methods towards the end of the course and really, really liked TLA+. And then I started working with it right away. It never stopped.
RD: I ran across TLA+ briefly while researching an article about time travel and programming. Formal methods and proof programming seem very strict and sort of intimidating to outsiders. Do you feel that reputation is deserved?
GM: People make it deserve that often. It’s very strong in academia, and when academics present it to industry, they often fail to present it in an accessible way or talk about the actual pain points it solves. People hear things like, “Oh, you have to prove your code correct.” So I think the way it’s presented is kind of what makes it seem intimidating. But in reality, it’s actually way more useful for day-to-day engineers if you know what you’re doing. I don’t think it should deserve that reputation, but in the current shape of things, it often does.
RD: What is TLA+? How does it work?
GM: TLA+ is a formal specification language. We probably know what a specification is — you’re specifying what your software should do and what it should not do. But in TLA+, you do that formally. And formally means there is no room for ambiguity, no room for interpretation. You’re specifying it in a precise way, and the lack of ambiguity is achieved by establishing a formal semantics to the syntax. Whatever you write there has one precise meaning, going all the way back to mathematics. That’s how it was born — to be a precise language for defining algorithms and protocols, especially in the distributed systems area.
TLA+ was created by Leslie Lamport, the father of distributed systems and also the creator of TeX for LaTeX. Lamport was writing papers on distributed systems algorithms and realized he was not being precise — he found imprecision in his own papers. He thought, if someone like me is making these mistakes, others certainly are too, and that’s a problem. So he came up with a shared language everyone could use. It started as a language used in papers, and then people realized they could add tooling for it. You can use machines to check what was written, not only as a precise way of writing things, but actually checking properties. So they implemented a model checker — the TLC model checker. TLC is an acronym that doesn’t officially stand for anything. You can think of a model checker as like the compiler for a language. Specification languages don’t produce executable code the way compilers do; instead, a model checker verifies the specification. It takes your TLA+ specification and checks that it is correct.
RD: If I have it correctly, the formal specification isn’t something you build a piece of software directly from. You write the specification first and then write the software later. It would verify that what you’ve written meets the specification, right?
GM: There is a big challenge with formal methods, which is that we don’t really have great tools for verifying that the actual code itself is correct. There are some tools for that, but they are often quite limited because the range of things you can write in code is very large. It’s hard to write a model checker for a language like Rust. Some exist, but they are often quite limited in how much they can check. In TLA+, you can check much more — essentially everything you write in the language — because it’s a language purpose-built for verification.
The main pitch for TLA+ is that you first write your TLA+ model, and then you go and write your code. Leslie Lamport talks about this as: who would construct a building before drawing a blueprint? You first need your blueprint, and with a blueprint you can do calculations, check if the walls match in size, and if you notice something is off, it’s much easier to fix a blueprint than a building. That’s true for code as well. It’s expensive to write code, and changing it can introduce bugs. So if you’re thinking about a design, you might want to check it on an abstract level in a formal specification language first, then go implement it.
I think one reason the industry struggles to see the value in formal methods is that people pitch it as something you must do before writing code. When you already have code written, people think it no longer applies. But it’s still valuable after the fact. You can find design issues even after the code exists. You can model potential fixes in TLA+ and quickly find out whether a proposed fix actually holds — maybe there’s one edge case where it doesn’t, and you need to think harder before touching the code. There are different moments in a project lifecycle where formal specifications add value.
RD: There are edge cases that don’t surface until you hit production volume. Formal specification would be able to catch the faulty logic before it has to reach production, right?
GM: I want to talk about a recent example of exactly that, and it actually uses Quint, which is a good way to introduce it. Quint is a surface syntax on top of TLA+. TLA+‘s syntax is quite mathematical and hard for people to onboard. Quint starts with a different, more programmer-friendly syntax and adds more tooling on top of TLA+ to make it easier for industry applications. It’s the same philosophy underneath.
We had a use case recently — we have a blog post about it if you want to read more — involving a bug with an external team from OpenHands. OpenHands was running a Kubernetes deployment that was causing problems, triggering alerts constantly due to a race condition. They had Quint tooling set up and wanted to apply a fix, but between applying a fix and seeing whether the problem recurred, it would take weeks because of the nature of the deployment. So they used Quint to check whether their proposed fix was sufficient. Quint said no — this case is not covered by your fix, and it’s still going to cause a problem. They went ahead with the deployment anyway, and the exact problem Quint had reported appeared in production. They then experimented with different fixes until Quint could verify one, shipped that fix, and the problem went away.
That’s the case where the tool tells you you’re wrong. We actually posted a meme about this recently: Claude and ChatGPT and other AI tools will tell you you’re absolutely right. Formal method tools will tell you you’re absolutely wrong.
RD: That information is probably better for engineers. Engineers want to know what’s wrong with a thing — what’s right with it can take care of itself.
GM: Exactly. And it’s also helpful when you’re trying to make optimizations, not just fixes. You can apply an optimization, verify in Quint that it preserves the correctness of your system, and ship with much greater confidence that you haven’t broken anything in the process.
