EP. 228 - Quint Co: The Executable Spec Language Made For The AI Era

**Gabriela Moreira** (0:00)
How much can actually AI know what correct means for your application, right? They can, maybe like, I think with AI, we get more of these applications that don't crash, right? But there are so many new ones in software behavior, how systems should behave, that AI will not be able to tell what is right and wrong, right? Who knows what's right and wrong is the person building the application.

**Narb** (0:24)
Welcome to the DevNTell Podcast, where founders, hackers and anyone in between showcase their products built on the bleeding edge of tech. GM, GM, welcome to the show, Gabriella. I'm excited to have you on today.

**Gabriela Moreira** (0:36)
Yes, thank you for having me. I'm very excited.

**Narb** (0:39)
Yeah, likewise, likewise.
Yeah, in this age of AI, we know there's a lot of code being produced and shipped, but not necessarily verified. And who knows what vulnerabilities people are shipping today. So I'm really excited for our audience today to learn about Quint and how they can start using it in their Vibe-coded builds. But before we get into that, would you just like to give an introduction about yourself?

**Gabriela Moreira** (1:12)
Yes, for sure. So I was doing my bachelor's in computer science, started over 10 years ago. And at that time, I was doing some compiler work. I really liked compilers, programming languages, type systems, all that stuff.
And then someone introduced me to a language called TLA Plus, the formal specification language. And at the time, I was also working in the industry with web development, distributed systems, databases. And I was like, oh, this thing would be super useful in my job. But also, the syntax is so mathematical and so scary, I doubt anyone in my team would like to use this. So I don't know how I can introduce this to them. But I fell in love with formal methods right there, and I got this passion to, okay, we have to make this a little bit better. So it's more useful in the industry because everyone should be using this thing. So I continued working on my job, and then I made a master's about all of this topic of to lean around formal verification. And then I met this company called Informal Systems, which was doing a lot of web tree development, founding the Cosmos blockchain. And they were also very informal methods from the beginning and doing a lot of work with TLA+.
So we met at the TLA plus conference, and right away, we're doing pretty much the same thing, like the same kind of tool. So naturally, like I started working with them, and that's when Quint was born as well. So my origin story has a lot of intersection with Quint's origin story, but that's me. I'm living in Brazil. I was born here. I love the country. I love living here. I have a little cat that might intervene in today's podcast.
And yeah, very excited about the World Cup.

**Narb** (3:02)
Yeah, I can imagine. Yeah, we're talking out there. Yeah, FIFA has taken the World by storm the last little while. So I can't blame me if we hear some cheers once in a while to the podcast.
But yeah, I just want to kind of dig in. You mentioned kind of gravitating towards the crypto scene with the team behind Cosmos. I was just curious, what drew you into this space, other than that same passion for formerly verifying code?

**Gabriela Moreira** (3:37)
It's pretty much the same passion, but what I like to highlight about the intersection of WebTree and Formal Verification, is that WebTree is really the best use case in order to exceed at this kind of thing, because first of all, you have this problem where when you ship code in WebTree, it's hard to patch it. This is also true when you're in rocket launches. If you have software within the rocket, in the spaceship, you don't get to fix it because the software is on the air, same with airplanes.
So I think blockchain has that same sort of thing where it's hard to fix mistakes once they are out there. Second, there is such high incentives for people to exploit problems because the money is right there. So if you find an exploit, that usually means you make money instantly. You don't have to do anything else. So there's a lot of incentives for exploitation, which means we have more of that asymmetry between attacker and defender. We have to put more effort into making share code is correct. And third is by the time I joined, the ecosystem is where the most money incentive was into formal methods. Basically, when I was starting with formal methods, you would hear from the research groups and stuff, if you want to work in the industry with formal methods, you have to work on blockchain.