AI says you’re right, formal methods say you’re wrong

extract

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. Connect with Gabriela on LinkedIn and X. Congrats to Populist badge winner Alex K. for winning the badge on their answer to SQL Server: Select Top 0?. TRANSCRIPT [intro music] 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 like a bit into gaming. My computer was not the best, so I had to like, 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. And I ended up, like, the parts that I like the most about mathematics is the parts that we see about mathematics in computer science, like discrete mathematics, graph theory. So that was nice. And then inside formal, inside software, computer science, I liked like compilers, computer theory. And 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 like right away. It never stopped. RD: Yeah, I think I ran across TLA+, briefly in researching a sort of jokeyish article about time travel and programming. It's a very, you know, any sort of formal methods proof programming, it seems very strict and sort of intimidating to outsiders. Do you feel that it deserves this sort of intimidating reputation? GM: People make it deserve that often. It's very strong in academia, right? Formal methods of different shapes. And when the academics present that to the industry, they often fail to present it in an accessible way, talk about actual pain points it solves. People talk about like, oh, you have to prove your code correct. What are you doing? You're guilty. So I think the way it's presented is kind of like what makes it deserve that. But in reality, it's actually way more useful for day-to-day people if you know what you're doing. So yeah, I don't think it should deserve that. But I think the current shape of things, it often does. RD: What is TLA+? How does it work? GM: So TLA+ is a formal specification language. Okay, we know probably what a specification is, right? We are specifying what are the requirements of our software, what it should do, what it should not do. But in TLA+, you do that formally. And formally means there is no room for ambiguity. There is no room for interpretation, right? So you're specifying it in a way, and it's that way, and that's it. And the way this is achieved, the lack of ambiguity, is by establishing a formal semantics to the... syntax, right? So whatever you write there, there is one precise way about what this means going all the way back to mathematics and how it's established in mathematics. So really, there's no room for ambiguity. That's how it was born, to be a precise language, to define algorithms, protocols, especially in the distributed systems area. So TLA+ was created by Leslie Lampard, the father of distributed systems, also creator of text for Latex. So Leslie Lampard was writing papers, right? He was coming up with all these distributed systems, algorithms, and he was writing papers and he realized that he was not being precise. He found like imprecision in his own papers. And he's like, oh, if I'm this like super smart person and I'm making this imprecision, so for sure other people are being imprecise as well, and that's a problem. So let's come up with a shared language we can use. So it was just a language used in papers. And then people realized they could add tooling for that. So you can like use machines to check what was written there, not only like be a precise way of writing it, but actually checking properties. So they implemented a model checker, the TLC model checker, which is an acronym that don't stands for anything. They don't define what the acronym stands for, just TLC. That is the model checker for TLA+, which is, you can think of it as like the compiler for a language, right? Languages have compilers. Specification language is they don't have like a compiler that will execute your code or produce executable code. They have something like a model checker, which is going to verify the code, right? So it takes your TLA+ specifications that will define your specification and check that it is correct. RD: If I have it correctly, the formal specification is not something you would build a piece of software off of. You have that first and then have the software later. It would be something to verify that the software you've written meets the specification, right? GM: There is a big problem with formal methods, which is we don't really have something to verify that the actual code is correct. There are some tools for verifying that the actual code is correct, but they are often very limited because the amount of things you can write in code is very big. So it's hard to write, for instance, a model checker for Rust. There exists some model checkers for Rust, but they are often quite limited in how much they can do and how much they can check. In TLA+, you can check much more, like everything you write in the language pretty much. There's some KPIs, but like most things you can write in the language can be checked because it's a language made for that. So it doesn't have such a big scope. You said like you first write your specification and then you go and write your code. And that's like the main pitch for TLA+ mainly, right? So for TLA+, the main pitch is like you go first, you write your TLA+ model, and then later you go and write your code. Leslie Lempore talks about this as who would construct a building before drawing a blueprint. You first need your blueprint, and in your blueprint, you can do some sort of calculations, see if the walls match in size, they add up. You can do all of these calculations, and if you notice something is off, it's much easier to fix a blueprint than to go and fix a building. And that's true also for code, although there are some like, oh, but code is so much cheaper to fix than a building. But like, is it? Because it's very expensive to write code. If you are going to change code, you might introduce bugs. It's very complicated. So you're thinking about a design, you might want to first check the design on a simple abstract level in a formal specification language, and then later you go to implement it. I don't think it's only on this order. I think that's the ideal order. Like you first go and design and then you go and implement. I think this might be one of the reasons why the industry struggles to see the value in formal methods and like, oh, think this is for me because we... people pitch a lot like, oh, you have to do it before. And you're like, oh, but I already have my code. Then what should I do now? But it's still valuable, of course, if you already have your code. You can go and find design issues even after the code is written. And then you go and attempt different fixes, right? So if you found a problem, you can go like, oh, would this be a fix for my problem? You can go and model that in TLA+ or other specification language. And then... oh yeah, no, that's not actually a fix. There's this one case where actually this fix doesn't apply. So I actually have to think about a different fix before you go and apply to the code. So there are different moments in your life and your project lifecycle where you want to use formal specifications. RD:There's some edge cases that don't arise until you sort of hit something like several times. Like it'll only show up in production because of the volume of traffic. So formal specification would be able to catch the faulty logic before it has to go into production, right? GM: So I want to talk about a recent example we had of that, but it's actually, this one was not using TLA+, it was using Quint. So it's a good way maybe for me to introduce Quint. Quint is just a surface syntax on top of TLA+. TLA+ syntax, you can see, is kind of like very mathematical, hard for people to onboard. So it started with a different syntax and also would develop like more tooling on top of TLA+ for like making things easier for industry applications. So it's just another version. RD: TLA+ seems very rooted in like analytic philosophy and logic, right? GM: You want programmers to adopt it and programmers are much more used to writing words and call functions into type mathematical symbols. They think about AND and OR, they don't think about backslash. We started as a syntax and then we added more tooling. It's the same philosophy underneath. We had recently a use case where we have a blog post about this, if you want to read more, but there's basically this bug that was happening with an external team from OpenHands. So OpenHands was having a Kubernetes deployment and it was causing problems. It was like triggering alerts all the time and they had a bug, a race condition. And then they had like some Quince tooling installed and they were to apply a fix. But between applying a fix and then seeing the problem happening again, it would take weeks because of the nature of the deployment. So they decided to check that with Quint if the fix was enough. And Quint said, no, this is not enough. This case is not covered by your fix. It's still going to cause a problem. And actually, they did that after deployment. And then they saw the actual problem that Quint reported happen in production later on. And then they experimented with different fixes until… Quint could verify the fix and then they shipped that fix and they didn't have problems anymore. So this case is where it tells you no, right? We actually posted a meme yesterday that fits well here. We posted a meme that like Claude and ChatGPT and other tools, they will tell you you're absolutely right. But formal method tools, they'll tell you you're absolutely wrong. RD: Right. I think that information is probably better for engineers. Engineers want to know what's wrong with a thing. What's right with it is that's fine. Like, let that go. GM: And it's also helpful if you are trying to make optimizations in your code. So not only applying fixes and checking that fix apply, but applying optimizations and checking that optimizations are not going to break any existing behavior that you have, right? This is a nice case from AWS. So AWS, there's probably like the most famous and strongest user of TLA+. And they wrote this comprehensive paper about the different projects in which they apply TLA+, and what they got out of it. And it's super nice. And like one of the cases that they could apply aggressive optimizations that they wouldn't feel confident in applying if they could not actually check. It's not affecting behavior. It's still holding all properties for all cases. So that was super nice. RD: So AWS is an interesting one because they just hired the creator of the Lean language, which is another formal specification language. Do you have an opinion on the difference between TLA+ and Lean or other formal specification languages like that? GM: I love Lean. I actually learned ROC, like previously COC, when I was also in... my graduation. So I haven't had much contact with Lean, but it's essentially the same thing, just like a little bit better. The same as TLA+, right? So there are different families. So for model checking tools, like TLA+, Quint, Alloy is also one. It's a bit different, but also in there. You can just specify what you want, and then you have automatic proofs. And you don't even have to go all the way to proofs. You can also get value just from like random simulation. So if you're like... you don't have time to go and reduce your state space such that the tool can find a proof for you or like tune the spec until you can actually prove it, you can also get value out of just like running simulations. And this we have a bunch of experience on. We had done a lot of like just simulations and got a lot of value out of specifications. So there is that. And then if you go to the proof assistants like Lean, COC, Isabel, Agda. There you have to put more work in. So besides writing your specification, and also the specification is written usually in a different, like more specific form, and it's harder to write your specification. You also have to go and write your own proof, which is a lot of work, right? So before, like until last year, it was like, okay, you go to model checking if you want something more lightweight, and then you go to these other tools if you really need to be super thorough with everything. And it was way more reserved to like spaces where safety was super, super important to really not have any flaws. So it was way harder to justify applying that to the industry, right? How can you spend like maybe one year, maybe three years proving something? Does it really justify? Things have changed a lot this year because now you can ask your AI buddies to write the proof for you. And it seems like this is working quite well, right? So it's very interesting. I'm super excited about the… evolutions on like, especially with Lean, a lot of like AI is getting good at writing Lean proofs. There's a lot of debate on things there. But I think like the main point that concerns me with this is who is writing the specifications, right? Because I think in a lot of these scenarios, people are relying on getting AI to also write the specifications and then you get a proof, but it's a proof of what? Did you really check? So I think tools like TLA+ and Quint and Alloy, they can help you iterate a bit more. So especially with Quint, we've done a lot of things just to help you understand what you have specified. So you're not just like spec and then you go and check. You also can understand what's in there. You can like go give me one example run and then you look at that. Does that sound correct? You have like interactive tools. So I think it's way more important now that we understand what is specified and we check like, oh, the specification matches what I intended. And then if I have a proof of that, then perfect. But like, I think the biggest gap now is in this, making sure you're really specifying what you have intended and not like just delegated to AI because people are redoing that a lot. Especially also like with TLA+, there is more adoption than ever now because the syntax was a pain point. Now AI can write it for you. So it kind of like took that pain away. But then if you cannot read what the AI wrote because the symbols are too complicated, then I have a big concern with that. RD: Where do you put the vibe coding, right? The vibe coding here is in the former proof stage. We talked a little bit about this and I think one of the things I've seen in the last year or so is people talking about spec-driven development. You know, with TLA+ being a sort of formal spec, are there ways to use AI to kind of generate code from it? Or I think you're talking about the reverse way of like generating a formal spec from whatever specification you have. GM: Yeah, the two paths are feasible and being explored for the spec-driven development path, right? Where you first write the spec and then produce code out of the spec. It was interesting because like last year, I think around this time or earlier, I think like around April last year, maybe, there was a talk at AI Engineer, like this big AI conference. And the person was proposing like, oh, spec-driven development. This is where the terms arise again. And then I watched the talk and I was very excited. Like, oh, this is a time for specs, finally. And then it was like, oh, no, you write this markdown and you have the agents read the markdown. And I was like, oh, no, markdown. It can be imprecise and then you also cannot really check what was written there. So if more and more people are using agents to write the markdown, are you really going to read the markdown and make sure that matches your intention? RD: The spec in this case is just a larger prompt. GM: Especially if you're not reading it and you're not refining it, it's just like a more agentic output and where does your intention land there. And it's not executable, right? You cannot really, like, I think a lot of joy that comes from programming is, like, you go and write some code, which is your, like, intention. You run it and you get maybe unexpected results. And like, oh, no, that's not what I meant. Let me adjust. The fact, like, when you execute it and you see the results is where, like, you can refine and you're very used to this loop of iteration. And when you remove the execution and you're, like, produce a text document, you have to read a text document, refine it, it's very frustrating. And because it's frustrating, I don't think it's very productive. And I think we will make a lot of mistakes. RD: When I spoke to a creator of C++, he said, English and other human languages are very imprecise. And code is a precise definition of a solution, right? GM: Some people say a precise specification is the code. And I agree with that to some extent. I think there's stuff in the code you don't care so much about. Whether you're calling this function this or that. Now, especially if you're developing a lot with AI, there's stuff in the code you don't care so much about, like whether you're logging things this way or that way as long as they get logged, or there's some small details in code that are not as important as your core algorithm, your core protocol. So when you're just going to code, especially if you're not spending time writing it, if you're iterating with AI, it's very hard to play with the code. It's a lot of code. Get that all in your brain and then see if it's right or not. And it's nice to extract that most important bit, core algorithm, the core protocol, and reason about that in your head while maybe leaving AI to the side some smaller details. And this is also what formal specifications can help you with. They are in a high level of abstraction. So when you see a TLA+, specification is not going to be talking about like, when do you log some line? When you do this, it's not like going to be in all level of detail. It's going to be on the level of the things you actually care about. RD: It's becoming clear, I think, with folks doing a lot of, offloading a lot of the tasks you said, like the specification itself, not just decoding to the AI. A little bit of formal specification understanding is going to become important for everybody. So how do you make formal specification languages like TLA+ a little more accessible for people to understand? GM: Well, there are some layers to it. First thing we tried in our team was to make this different syntax that was more familiar to engineers. And I think that helps if you're going to read the spec. I think it helps a lot, especially if you're writing spec by hand, then for sure it helps a lot. We had like autocomplete, it was easier to write, etc. Now people are probably not going to be writing that by hand. Maybe they'll be reading it. I don't know. The future is kind of unclear. But let's assume they maybe will not be reading it because everything is moving so fast. No one's reading anything anymore. I don't think they need to read the spec if they have a good way of executing it. I'm so passionate about this executability and this feeling you had when you were programming that I'm just trying to figure out ways to bring that back more. So when you're interacting with AI, you still have something, you execute the goal, like change something, run again, see the results, some of that feeling. But in this more high abstraction level in the formal specs, let's say everyone has to work with formal specs because of AI, let's imagine this scenario. I think the best way they can start with this is by having something they execute and see results, right? And when you're talking about TLA+ and Quint, and in this case, not Alloy, It's all about behaviors, right? So a specification in TLA+ is a specification of all behaviors, and in Quint, is a specification of all behaviors our software can have. It's a set of all behaviors. You can also think of it as a state machine, right? A state machine defines all the possible behaviors. So it's all about behaviors, and behavior here in this context is a sequence of states. So you start in an initial state, then you go to that state, then you go to that state. It's sometimes easier to think of it as a sequence of steps. Start in a state where you have 100 bucks in your account. Then you withdraw and you end up with 50. And then you transfer and then you deposit. You know, there's a sequence of things that happen. That's one behavior of your system. That's one thing that can happen. It cannot happen maybe that you end up with negative balance because you don't allow you to withdraw more than you have. That's a behavior that is not allowed by the specification. So we are thinking about behaviors a lot. And I think talking about behaviors is easier than talking about formal specs. So like, oh, what if you have a tool that allow you to define all behaviors a software can have and then check that, let's say like you're testing those behaviors properly, that all those behaviors are actually things you want. So maybe like you look at them, some of those behaviors, some random behaviors maybe, and then like, oh, actually this one I don't like. So let's make sure we don't have that. And then you write properties about those behaviors. So I don't want any behaviors that end up with negative balance. So I think thinking about behaviors, which is the core part of TLA+ and Quint anyway, is a nice way to get started. And I think people are starting to talk about behaviors a lot in the context of AI. So we don't care about the specifics of the code as long as it behaves correctly. Let's just test that it behaves correctly. We just need some spec or some harness. And here people are sometimes even talking about markdown, right? Just some spec and some harness that make sure the behaviors are correct. And I agree a lot with that. That's what I think is going to make it accessible. That's what I believe. That's my thesis. That's what I'm trying, right? I'm not sure if I'm right. RD: I like that way of talking about it, that it's behaviors. But think about that, like the code that people write was intended to implement those behaviors. And that's not always how it works, right? There's logic bugs in there. What about TLA+ in these formal specification languages makes those logic bugs more visible or makes them harder to implement, basically? Or is there something in there? GM: You can start with a spec and produce code from that, or you can go the other way around. You already have some code and try to write a spec from your code. So I think what you mentioned now is more on the first one. So you have a spec. How do you know if you have bugs in your spec, they would end up as bugs in the code, right? The thing there is, with a spec, you can verify it. Properties, you can check properties. So if you, for instance, if you write your little bank that I was talking about, withdraw, deposits, transfers, right? And you write a property, no negative balances. All balances should be greater or equal than zero. You write that, you run the model tracker or simulator even, and you see like, okay, it's impossible to reach a scenario, a case where balances are negative. So I'm sure that this one bug, the code won't have, right? If you implement properly from the spec. So that's why you don't have the same sort of like logic bugs in the spec level. And then on the other way around, there is also something interesting that we discovered more in practice when we were writing specs. I worked on a team where we had like an audit business. So you do security audits for software, right? And we were trying to use formal specs in some of them. And when we were writing like these formal specifications, we were using Quint. More often than not, we found bugs not by running model checkers, just by writing the spec. So you would read the code and the documentation that the team supplied to us, and you're going to write some, and just the formal language, it makes you be more precise. So for instance, in Quint and TLA+, all if statements need to have an else branch. So it cannot be the case where you forget to handle, okay, in the else scenario, what happens? You have to tell what happens. Oh, nothing happens. Oh, we throw an error. You have to say what happens in that else branch. So just thinking you have to cover all scenarios. So just by writing the spec, you would often like, oh, wait, something weird happens here. There's not visible in the code at all, but then the else branch here is not taken care of. Some bug can happen. And we would go back to the team with a report before even running it too, just by writing the spec. And we're actually producing that now just by having agents write the specs, they can already find bugs even before running any tools. So this is also interesting. The language, it makes you be more precise and then you find things you didn't consider while writing code. RD: For Quint itself, where does it sit in this sort of process? Like when I hear about formal specification, it almost sounds like part of the test suite, right? That's probably not entirely accurate, but it does feel like you're asserting like, this value has to be true, like no negative balances. But where does it sit in the sort of software development lifecycle? GM: What makes this answer difficult is that it can fit in very different places depending on what you want, right? We were talking now here, like we can do it before development for a design. I think it's a great, I think that's the most obvious one. If you have like in your Kanban board, you have a solution design column, you know, that's a very good place to insert from specifications because then you can like validate your design before you go and start implementing. And then I think you're also right when you say it's part of the testing suite. So we were talking before about how you cannot really model check the code or it's really hard to model check the code. So you want to check this spec that's like separated from your code. But what you really care about is the code. In reality, you don't care about the spec. You care about your production code working. So how do you bridge that gap? How can you make sure that they are doing the same thing? The model and your specification and your code are doing the same thing. So the things you've verified for the model are also sort of checked in the code to some extent. And the way to do that is... there are two main ways people approach this. One of them is model-based testing. So it's a testing strategy where you would take random behaviors from your model or specific behaviors from your model and replay them against the code. Make sure that at every step it's doing the same thing, right? So, oh, the model did a deposit of 50 bucks. Let's call the deposit function of the real code and see the resulting state. Does Alice have 50 more bucks now after she did the deposit. So you go and like reproduce maybe like thousands of these behaviors to make sure that you're not absolutely certain that, but you have some more trust that they match, right? The model and the code. That's one strategy. But still, as you said, as well in this podcast, what you really care about is production. And in production, sometimes weird things happen that you didn't think of testing. And this strategy might not really cover that, right? So there might be stuff that happens in production that you're not testing for, the model is not accounting for, because the model is also constrained to some domains. And then when that thing happens, then things break. So if you want to check that the things with the weird data that comes from production also respects the rules and the specification you're written, then there's the other strategy called trace validation. And that one is harder to implement. But the idea is we take logs from what happened in production, and then that log is also a behavior, right? So you can also see like, oh, this happened, and then that happened, and then that happened. And then you take this one behavior and you make sure that the spec allows it. So let's click the spec, hey, is this event behavior according to what we specified? And the spec can say yes or no. And this is the challenging part because sometimes the granularity of things you have in production and how much data you can get out of production, it's tricky, right? You cannot just take like the entire bank and how much balance every person has and log that at every step, right? So that's where the challenge comes in. But that's one strategy. So I think those two are like more on this testing side of things. And we are experimenting with some new stuff now. We achieved this. We managed to do this and it's working well. We just see how muc