AIは「その通り」と言い、形式手法は「間違いだ」と言う

Hello, everyone, and welcome to the Stock 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. Thank you, Ryan. Thank you for having me. 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? 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 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 plus. And then I started working with it like right away. It never stopped. Yeah, I think I ran across TLA plus 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? 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 or talk about an 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 to 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. What is TLA Plus? How does it work? So TLA Plus is a formal specification language. We know probably what a specification is. You're specifying what are the requirements of our software, what it should do, what it should not do. But in CLS Plus, you do that formally. And formally means there is no room for ambiguity. There is no room for interpretation. 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. 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 Plus was created by Leslie Lamport, the father of distributed systems, also creator of text for Latex. So Leslie Lamport was writing papers. 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 you 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 precise where you're writing it, but actually checking properties. So they implemented a model checker, the TLC model checker. It's just an acronym that don't stands for anything. They don't define what the acronym stands for.

It's just TLC. That is the model checker for Chile Plus, which is, you can think of it as like the compiler for a language, right? Languages have compilers. Specification languages 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 CLF specifications that will define your specification and check that it is correct. 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 this specification, right? 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 Plus, you can check much more. Everything you write in the language, there's some cases, but 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 you first write your specification and then you go and write your code. and that's like the main pitch for TLA plus mainly right so for TLA plus the main pitch is like you go first you write your TLA plus model and then later you go and write your code Leslie Lampard talks about this as who would construct a building before drawing a blueprint right you first need your blueprint and then your blueprint you can do some sort of like calculations see if like the the walls match in size you know like 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 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 like 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 until it was for 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 in your project lifecycle where you want to use formal specifications There some edge cases that don arise until you sort of hit something like several times Like it 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? So I want to talk about a recent example we had of that, but it's actually, this one was not using CLF plus, was using Quint. So it's a good way maybe for me to introduce Quint. when it is just a surface syntax on top of TLA+. TLA plus syntax, you can see, is kind of, like, very mathematical, hard for people to onboard. So we started with a different syntax, and also we developed, like, more tooling on top of TLA plus for, like, making things easier for industry applications. So it's just another version. TLA plus seems very rooted in, like, analytic philosophy and logic, right? We want programmers to adopt it, and programmers are much more used to writing, like, words and call functions into type mathematical symbols. They think about AND and OR. They don't think about backslash. We started with it as a syntax, and then we added like four 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 race condition. And then they had like some Quint 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 like 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 from a method of tools, they'll tell you you're absolutely wrong.

Right. I think that information is probably better for engineers. Engineers want to know what's wrong with a thing. And what's right with it, that's fine. Like, let that go. And it's also helpful if you are trying to make optimizations in your code. So not only applying fixes and checking if the fix applied, but applying optimizations and checking that optimizations are not going to break any existing behavior that you have. And this is a nice case from AWS. So AWS is probably like the most famous and strongest user of TLA+. And they wrote this comprehensive paper about the different projects in which they applied TLA+, and what they got out of it. And it's super nice. And like one of the cases there, 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. 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 Plus and Lean or other formal specification languages like that?

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, LOI is also 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 simulations. So if you don't have time to go and reduce your state space such that the tool can find a proof for you or tune the spec until it can actually prove it, you can also get value out of just running simulations. And this we have a bunch of experience on. We have done a lot of 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, Koch, 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 troll with everything. And it was way more reserved to, like, spaces where safety was super, super important. You could 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, especially with Lean. A lot of 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 Plus 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, like, can understand what's in there. where 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 delegating 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. 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 that we've seen in the last year or so is people talking about spec-driven development.

You know, with TLA plus 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 generating a formal spec from whatever specification you have. 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 last year, I think around this time or earlier, I think around April last year maybe, there was talk at AI Engineer, like this big AI conference. And the person was proposing like, oh, spec-driven development. And this was where the term Arised again And then I watched this talk And I was very excited Like oh This is the 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 Like It can be imprecise 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 Like it can be imprecise And then you also cannot really check what was written there So if more and more people are using, like, agents to write the markdown, are you really going to, like, read the markdown and make sure that measures your intention?

The spec in this case is just a larger prompt. Especially if you're not reading it and you're not refining it. It's just like a more of an agentic output and where does your intention land there. And it's not executable, right? So 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 an expected result. 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, is 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. When I spoke to Creative C++, he said, English and other human languages are very imprecise. And code is a precise definition of a solution, right? 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 are 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 are 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 interacting with AI, it's very hard to play with the code. There's, like, a lot of code. Get that all in your brain and then see if it's right or not. And it's nice to, like, extract that most important bit, core algorithm, the core protocol, and reason about that in your head while maybe leaving it to the side, some, like, 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 plus, 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. going to be on the level of the things you actually care about.

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 the coding 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 Plus a little more accessible for people to understand? Well, there are some layers to it. first thing we tried, right, 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 I assume they maybe will not be reading it because they're like, everything's moving so fast, no one's like 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, like, executability and this, like, feeling you have when you're

programming that I'm just, like, trying to figure out ways to bring that back more. So when you're interacting with AI, you still have something you execute to go, like, change something, run again, see 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 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 ScaliPlus and Quint and in this case not Alloy, it's all about behaviors, right? So a specification in ScaliPlus 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. So start in a state where you have $100 in your account.

Then you withdraw and you end up with $50. And then you transfer and then you deposit. 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 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 allows 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 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 CLA Plus 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 specs 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. 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 plus in these formal specification languages makes those logic bugs more visible or makes them harder to implement, basically? or is there something in there? You can start with a spec and produce code from that or you can go down the 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 properties.

You can check properties. So if you, for instance, if you write your little bank that I was talking about, withdraw, deposit, transfer, 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 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 the 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. Like, a bug can happen. And we would go back to the team with a report before even running into it 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. 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? What makes this answer difficult is that it can fit in very different places depending on what you want, right? So 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 your testing suite. So you 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 reach that gap? How can you make sure that you are, like, doing the same thing. The model and your specification and your code are doing the same thing.

So the things you verified for the model are also like 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 states. 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 so certain, 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, you actually really care about production. and then 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 a constraint 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, like, 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 that's like the spec, hey, is this a valid 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 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 more on the 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're just seeing how much other teams pick it up. But what we're doing is running your existing test suite. This is what we're doing in our product. We run your existing test with instrumentation, with logs. So as if it was like production traces. And then we do this like trace validation technique over your logs. So we can see which behaviors your existing tests are exercising. Right. So we say like, hey, you have tests for like deposits. You have tests for like transferring after a deposit. But you never tested a withdrawal after a deposit. So maybe you want to test that. Right. So we are experimenting with some stuff there. But it's all in this area of like writing useful specs and then making the code match the specs. It almost sounds like you're getting into test observability. Yeah. So Quint is completely open source, right? It's a, if you like TLA+, we integrate it with the same model checkers as TLA+, you can like transpile Quint into TLA+, and try it out. So if you're curious about Quint, we have that. And we're also having a product in beta now,

which does this like trace validation on the test, seeing it suggest a test for you, and it's very centered on behaviors. So this product is our attempt at making this more like behavior-centric development, especially if you're using AI. So, yes, people want to try it out. It's called Queen Studio, trying to express these ideas that I'm sharing here in something that everyone can use because that's all they want. Thank you very much, everyone, for listening. It's that time of the show where we shout out somebody who came on to Stack Overflow, dropped some knowledge, shared some curiosity, and earned themselves a badge. Today, we're shouting out the winner of a populist badge, somebody who dropped an answer that was so good it outscored the accepted answer. So congrats to Alex K. for answering SQL Server Select Top Zero. If you're curious about that, we have the answer for you in the show notes. I'm Ryan Donovan. I edit the blog, host the podcast here at Stack Overflow. If you have questions, concerns, topics, comments, email me at podcast at stackoverflow.com.

And if you want to reach out to me directly, you can find me on LinkedIn. Okay, I'm Gabriella Moreira. I'm CEO at Quint. I'm trying to make formal methods more accessible and make AI development more fun with behaviors at the center you can check out what we're building with my team at Quint we're building Quint Studio and you can find me on socials as Bugarella especially on LinkedIn it's where I'm most active all right thank you for listening everyone and we'll talk to you next time Thank you.