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

Ryan Donovan (0:08)

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 (0:28)

Thank you, Ryan. Thank you for having me.

Ryan Donovan (0:30)

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?

Gabriela Moreira (0:38)

I started a bachelor in computer science in 2015

I think I had two ways into software. One of them was because I was customizing my Tumblr themes and I like changing the code and seeing how things switched in the screen and I thought it was really magical.

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. And I ended up, the parts that I liked 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 software, computer science, I liked 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.

Ryan Donovan (1:35)

Yeah, I think I ran across TLA+, briefly, in researching a sort of joke-ish 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?

Gabriela Moreira (1:55)

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 the 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.

Ryan Donovan (2:32)

What is TLA+, how does it work?

Gabriela Moreira (2:34)

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 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 is like, oh, if I'm this super smart person and I'm making this imprecision, so for sure other people are being precise 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 precise when 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 stand for anything. They don't define what the acronym stands for, just TLC. That is the model checker for TLC+, which is you can think of it as like the compiler for our language, right? Language that 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 TLC specifications that will define your specification and check that it is correct.