Can We Trust AI-Written Code?

Claude has written for me 400 tests and I have no confidence whatsoever in any of these tests. I think you shouldn't read the spec. You should execute the spec and the behaviors. Right? So you simulate it and say, oh, this is 1 behavior.

Or simulate, oh, this is another behavior. Or AI wrote a proof. Okay. But what did it prove? You still have to understand something.

In order to feel confidence, you need to understand something. And it might be understanding the code or understanding the spec or understanding something else.

As AI helps us write more software than ever before, 1 question matters more than ever. How do we know that the code is actually correct? In this episode, I'm joined by Gabriela, CEO of Quint, to explore how formal specifications can help engineers build stronger systems with more confidence. We talk about what software correctness really means, why testing alone can leave blind spots, and how thinking in terms of system behaviors can reveal issues before they reach production. Gabriela also shares how Quint makes formal methods more accessible for everyday developers and why understanding your software may be more valuable than simply trusting what an AI agent produces.

So if you build complex systems, work with AI generated code, I hope everyone does these days, or want to ship with greater confidence, with understanding, this conversation is for you, my friend. So please enjoy the episode. And if you like the episode, please don't forget to hit the like button and subscribe to the channel. Now enjoy the episode. Welcome, Gabriela.

I'm really happy to have you today. And it's such an interesting topic. I'm always excited to talk about software correctness, especially in in today's world where all of us are using AI in our software development process. And we are generating more and more code at a higher speed, probably the fastest speed ever. So software correctness is important topic, and I would love for you to explain how all, you know, things have changed and how Quint helps with that.

So welcome again. But before we go into the technical discussions, let's start with a little bit of introduction about yourself.

Thank you. Thank you for having me. Super glad to be here. So my name is Gabriela. I am from Brazil, from the South Of Brazil.

I have discovered formal methods when I was like finishing university. At the same time I was working in the industry and I was like, oh, this thing here from academia would be super useful there in my job. But it's so hard to get people to adopt it there because it's so complicated in this current shape. So I've been trying to write different tools for making formal methods more accessible since then. So I worked a bit in the industry with like some distributed systems, message queues, and that kind of stuff.

Database, adjacent stuff, I would say. And then I moved on from that job to a job at a company where I started developing Quint. And Quint is a formal specification language, I've been working on this for the last 5 years almost. So I was working at this company and then this year we decided to spin out Quint as its own company. So Quint is now a company.

I'm the CEO, and that's, what I've been doing full time for a while now, trying to figure out formal methods for the industry. So that's about me.

Perfect. Awesome. So before we, you know, talk about formal specification and go deep into GWENT, I would love for us to, you know, create the foundation by defining what exactly do we even mean by software correctness.

It's a good question. Maybe we can start with the formal methods that I bet a lot of people are using, which is type systems. I think a lot of people are using languages that have types. Some of them have inferred types, you don't have to type in the keyboard what is the type of the thing, but you still have the type correctness being checked by the type checker. Right?

That's the most like a common probably formal methods that people use. And it means that if you like have a program, you're using a language that is typed, that has a type checker, and if it has a good type system, then it means that whatever program you write is type correct. So it's correct in relation to the types. It might be incorrect with relation to other things, but in relation to the types, it is correct. And you are writing a specification, you're writing which types you want some things to have.

And then you run the Type Checker and that is checking the types. And if it's incorrect, it will tell you. So it's not, maybe that's a nice way to think about formats to something that we are already using, but it's a bit bit of cheating because it's like a very lightweight way and very common way of formal methods. Right? So I bet you didn't invite me here to talk about type systems all day.

So the other way of defining correctness is something more high level. So it can express more than just about type safety, but it can express a lot of different properties about your whole system and what things it can do. So I like to talk about this as the behaviors that software can and cannot have. So when you're writing a specification in a language like Quint or TLA plus you're defining what are the behaviors that are correct. And anything outside of that definition is incorrect.

And then you're going to check if your software... If your solution, if your system already has those behaviors that you define or has any behavior outside of that. And then you define properties about those behaviors. Right? So that's like 1 way of thinking about correctness.

It is hard to define properties, right? I think especially now with AI, is way easier to write the actual formal spec, Cause you don't have to learn the syntax of the language, the TLA plus syntax or the QUINT syntax. You don't have to go sit down and learn another language and has some nuances. It's different from programming languages. So you don't have to do all of that.

You can just write like, Hey, I have to have this idea or I have this code. Can you, my dear agent, please write some formal specification for me? That part is easy nowadays. Still defining properties is kind of hard. You can ask the agent to kind of like guess some properties for you.

Are some properties that are way more obvious than others. And I think that's the interesting part when you talk about formal verification, like adoption in the AI era. A lot of teams are just like assuming we can infer the properties or just check the basic properties of like this software doesn't crash. Of course, we don't want the software to crash. There's no nuance in there.

Or maybe like we can tolerate crashes up to some certain threshold. And then it's ensure correctness under that threshold. So there are some ways of defining... So some correctness definitions that are more obvious than others. And then I'm way more interested in the more nuanced part of correctness where we have to think a little bit about, okay, what is the correct 1?

Is this that or is it this or is it that? What do we want the software to do in this case? I think that's like a whole problem there. Super interesting. And it falls outside of this like more obvious case.

The obvious cases are still super useful. If you can prove software doesn't crash, it's amazing. If we can prove the types are correct, that's amazing. That's why we do it every day. But I'm very interested in this like more nuanced, what is the correct 1 and what is the incorrect 1.

Yep. Makes sense. And so my problem, my personal problem with formal specification has been that it's... It has been like kind of inaccessible to folks who are not used to, you know, writing specs and already they are dealing with, let's say, writing code and distributed systems, understanding the failure modes and whatnot. And then understanding specs itself feels like, you know, kind of inaccessible.

As you mentioned, with AI, it has been accessible because you can ask AI to write a spec for you. But then if AI is writing the code, if AI is writing the spec, if AI is writing the tests, how do we show... How do we make sure that, you know, of course, the code is correct. Let's assume assume that. Tests are also correct based on whatever understanding we have given to the AI agent.

But how do we ensure that spec is correct? Because still, as an engineer, I can read the code, I can understand the test at a high level, but sometimes reading a spec can be, you know, really overwhelming if you're not used to it. So at what point a human should, you know, be... Feel confident that, okay, my spec is written by AI and it should be largely correct. And that gives me the confidence to, you know, move ahead and deploy my code to production.

Okay. There's a to unpack here in this question. 1st of all, I don't believe so much in this like, oh, AI goes and writes something and then I feel confident. Like, there's no something here. Like, even formal methods, even formal proofs, right?

Oh, yeah, I wrote a proof. Okay. But what did it prove? You still have to understand something. In order to feel confidence, you need to understand something.

And it might be understanding the code or understanding the spec or understanding something else. I'll get to that in a bit. Then you mentioned, oh, I might be more comfortable reading the code because I'm more used to that than reading the spec. And then I think that's true for most programmers nowadays, because we are used to reading the code and we are not familiar with the language of the spec. But the spec is more high level than the code.

It doesn't have so much detail as the code. So the code will have log lines. It will have some comments explaining some nuance. It will have some details. It will have some optimizations.

So because of performance, we have to do it like this and not like that. There's so much details in the same scope. So if you're like 1 function and there's logging, there is performance optimizations. There's so much things going on in 1 function and you're mixing a lot of scopes. You're mixing your logging concern, your performance concern with your correctness concern.

And in the spec, you are on a more high level and it's often easier to understand an algorithm if you read just the spec or compared to just reading a code that has a bunch of other details. So in theory, there is a reason to like reading specs can be easier than reading code. It's just that we are more used to reading code, but like maybe if the future changes, it might be actually more feasible to read specs. That's just 1 point. I'm really a defecating for that.

Was pointing that out that there's this level of obstruction. But the main part of the question thing here is like, if AI is writing the specs, AI is writing the code, AI is writing the test, like where do we fit in? Where do we check if things are correct? Right? And my thesis for this is that we check the behaviors.

And my favorite 2 words, okay, you see whenever you see 1 of my talks on the internet yourself, see my favorite words are behaviors and executability. I like things that are executable. When I started coding, you would write some code, execute it and see the results. And that felt really great. And then you would refine your code, change something, execute again.

And that is how we like think. That's how we operate as programmers. And now it's bit different, right? Because you read some prompts and it generates a bunch of code, but then you don't necessarily like go and execute it. You maybe like, let's do some tests and so different.

And we are losing that executability thing. But if you have a description of the system that we can execute and see like, oh, this is how it behaves. Oh, so it's behaving in a way I like. Oh, it's behaving in this way and I don't like that. This behavior is not good.

Then I think that's the level where I define correctness. So to simplify the answer a lot, or not a lot, but to simplify the answer, I think you shouldn't read the spec. You should execute the spec and the behaviors. Right? So you simulate it and say, oh, this is 1 behavior.

Or simulate, oh, this is another behavior. And of course you don't just random simulation. You can do like some other smart things so you can query it. Is it possible that this happens? And then it goes, simulates, oh, it is possible.

Look, here's how it happens. This is the behavior. 1st, the user logs in and then the user clicks this and then the user clicks that. And then you get that scene. And oh, that should not happen.

And it doesn't have to be. And talk about behaviors. I think front end. And I just gave you an front end example, right? The user goes, clicks here, clicks there.

Front end does like this behavior driven testing where you just described a high level behavior and then the engines go and like enforce that. And it's so beautiful And it works. The term, the concept of behavior works well there because you have so much non determinism. So you have like, the user can either click here or there or here. The user can decide to log out at any point.

The user can do this. The user can open 2 windows at the same time. There's so much non determinism that can happen there. And that's why you have to think about all the different things the user can do. And this is so much similar to what we have in a distributed or concurrent system.

There's also a lot of non determinism. The difference is that it's not the user that is going to do all of the weird things. It's like your scheduler on your processor. It's going to play all tricks on you and schedule things in the order that you didn't expect, and therefore your things are going to break. So I'm very defending of behavior driven testing also for your core parts of your system, not only for the front end.

So like for your different orders in which your threads can execute and your files can be read in the system. So it's all about behaviors. Yeah. Interesting.

I I kind of agree, but I still want to gather more information here. You mentioned behavior, and I think it's easier for all of us to kind of visualize when we talk about, you know, let's say, end and, you know, user adding an item to the cart and, you know, removing the cart, clicking the order button, and whatnot. But it's... And also the... Probably the the state transitions that can happen from a user's perspective are sort of limited.

Like, on a web page, I know what, like, 100 actions can a user do. Right? So I can probably enumerate all those 100 actions and probably have, like, a mental model of, okay, what can happen from a user's perspective. When we talk about like, let's say, systems, there are like millions of things that can happen in... At least in a complex distributor system.

And then to create sort of mental model and making sure that all of these things are included and well thought of when we are writing a spec or verifying a spec is difficult. So how do we bridge that gap? Right? I mean, I understand the point that we look at the behaviors, but there are just so many behaviors and so many possibilities that it may not be always possible. So what is your take on that?

Well, I think I think there's still a lot of complexity when interacting with users in terms of behaviors. It might be easier to predict all of the different things that can happen. I have a interesting anecdote maybe here. I was teaching formal methods at university and I had a very challenging setup because the students in my classroom, they, not all of them or many of them didn't do the course on distributed systems yet. So they were not familiar even with operational systems, so not familiar with threads.

So how could I explain like, oh, you need this tool to consider all possible scenarios, right? Formal methods. If they don't, like if they are used to writing code where they already can consider all the scenarios in their head, right? Which I think relates to the question you're asking here. So I tried many different things.

I was mostly using games actually to explain concepts because in games, there's a conflict. You would have like some strategy in order to... That you can beat your adversary in all scenarios. So you have like all these things that can happen in the game, but still you have to win in every single case, which looks a lot like a protocol. You have to ensure something at every single case.

That's what I was doing. But it was very challenging to teach in that setting. And then 1 of my students actually had what I would call a front end bug. And he came like, Gabriela, like it's a... I can use quit here.

Right? Because in the log, it's like they're having... Was a concurrency bug on the front end. Basically, they had 2 different users opening with the same screen open, and then 1 of the users would delete something. And then it wouldn't like automatically update on the other user screen.

So what happens if they go and edit that thing that was deleted? What should happen in that case? It's nuanced behavior, right? It could just error out or it could apply an overwrite, but what is the right behavior? We don't know.

It depends on the domain. It depends on what they want. So I think there's room for complexity in unexpected places, but definitely where we are most certain to find complexity is on like distributed systems and like different failure modes. And there, I think you have to combine different techniques. I'm a big fan of chaos engineering.

You know, what antithesis is doing. I think it's really amazing in simulation. And deterministic simulation testing is also like a good way to, I guess, coming from the formal methods perspective, right? You go and you design your system or your solution there and say you verify some properties. You're right that you're probably not going to be able to encompass all the complexity of the, what can happen in the real world in a system like that.

So you probably are not covering some things. So you have your suspect that is correct, but your code is not. And you don't want that because what you care about is your code. How can you check that your code matches the spec? I have a few techniques, but 1 of them is a model based testing.

So you can take your model, produce different behaviors, different traces, and replay them against code. And in that kind of system, this is very challenging because how do you replay what the scheduler did? You need the deterministic simulation engines in order to be able to do that. So this is like a whole big challenge. And I think I'm very excited about the recent developments in distributed simulation testing.

I think they will help a lot. Also, like we, the formal methods world to come and like be able to test those systems better and cover more of these scenarios. But it's a hard 1. Yeah.

Makes sense. And just to validate my understanding and your answer there, I think the idea is not to feel confident just by looking at the spec, but you have to execute it. And then not stop there. Right? Because there are multiple techniques that you produce.

There are different types of testing, like distributed simulation... Deterministic simulation testing, chaos testing you mentioned. And I think we should... As software engineers, we should always be sort of pessimistic that, okay, there are some cases that might have been missed, and I need to hit it from that angle to figure out if I have some bug. And all these testing methodologies can really help.

So it's not just about using 1 approach, but hitting that system from all the other different angles that you could possibly can, and then finding the bugs. Right? So it's it's a continuous process. It's not I've written a spec. Now I'm confident because spec also needs changes as your requirement changes, as you find more improvements and so on.

So I I totally agree there. Talking a bit about the model itself. Right? So if I understand correctly, model is a simpler version of your code that is going to be executed in in production. So there's a lot of probably implementation details that are intentionally skipped.

So in that sense, how do we make sure that... What is the right level of abstraction to include in a model in a spec and not go too far so that it looks like almost like a code?

Yeah. That's a really big challenge. I think we... There's like a lot of techniques. Probably could probably spend a whole hour talking about the different things you can do.

Right? But let's try to cover some basics. 1st of all, like, is the spec like a simpler version of the code? I'm not sure. But it's a more abstract version.

I'm not sure simpler is the word. Right? There are some things you can do in a spec and you can or cannot do it. On the literature, this is a recommended way of doing things. For instance, if you're going to have a sorting algorithm in your code, right?

So in some place you need the sort, you're going to call quicksort because you decided that's the sorting algorithm you're going to use. In your spec, you don't necessarily need to implement quick sort or define. You specify quick sort and then call it out. Because they're not so worried about quick sort being correct or not. You can assume quick sort sorts the thing, right?

The list. So you might just say like, hey, this function receives an unsorted list and returns a sorted list. You don't have to worry about the details. This is a more like default answer that I guess when I was teaching, this is the kind of thing I explained. But in reality, I think the most useful thing to consider is, is the spec enough to catch bugs?

Am I modeling enough things to catch some class of bugs? Right? And for instance, if you're thinking about a distributed system that tolerates failures, right? So if 1 of the nodes fails, you don't want the whole entire system to fail. You want to tolerate some.

If more than 0.5 of the nodes fail, then maybe you cannot do anything and then it actually fails. But if only like a few nodes fail, then you want to tolerate that. So you want to tolerate crashes, tolerate faders. In that case, the model is not going to be just a simpler version of your code. The model has to set up the whole environment in which you have multiple nodes and an environment in which nodes can fail.

In your code, you're never going to write, oh, fail. I want you to randomly fail here. Like you're not going to implement the failure, but when you are modeling it and try to see what can happen in the reality, you also have to model this like environment. So you can say like, oh, at any given point up to n number of nodes can fail, can crash. And what does it mean to crash?

Oh, it means that they will not respond to messages. Oh, it means that they would drop their message buffer. So all those things you have to define in your model. So it looks quite different in the code in those scenarios, right? Because you have all this adversarial surface there.

So getting the adversarial surface correct is I think 1 of the main things that makes a model correct or not. And the tools can help you because remember the spec is executable. So you can like define your property, say, well, I don't have a good property to talk about crash failure. I'm not sure There's like a nice 1. But let's talk about consensus, right?

So 2 phase commit. So if you have like... I know that the main example people use is like you're trying to book your flights. You try to book your hotel and you only want to book them if both of them are successfully booked. You don't want to have flights if you don't have a hotel.

Don't want to have hotels if you don't have flights. So this is a property of consistency, right? So you only have a hotel if you already booked the flights or if booked the flights, then you only have flights if you booked the hotel. You never get to a state where you have 1 and not the other. Say you want to show this property and then you go and run your model with all the adversarial surface and it still that can find like a violation of the property, might reconsider.

So like, oh, maybe I'm not modeling all the aspects. So I need to refine my model. Okay, now I have some scenarios here where I can hit a problem. But then when I implement the algorithm correctly, then I don't hit this problem, right? So basically implement the wrong version, see if it actually breaks the property, and then you go into the right version.

So there are a lot of these techniques. You also have to check if the algorithm is doing anything correctly or if your model is doing anything good, right? Because it's a good model that satisfies this property is a model that does nothing. A model that never books any flights or any hotels satisfies the property. So you have to make sure your model is actually sometimes booking hotels and booking flights, and it's also holding the property.

So, yeah, those are a few things. And we leverage like simulators and even the model checker, like the thing that verifies the software too, to help us see if our model is good enough to catch some bugs.

Yeah. I think that that makes sense. And... Yeah. I mean, model is definitely not simpler, but probably more abstract, as you rightly mentioned, a bit more concise.

And, I think there are techniques that, like you mentioned, and checking the properties, they're valid for implementation while actually hitting the problem from different angles and also leveraging different types of testing to reach that level of correctness that you want. And again, it's a continuous process. There will be always bugs. So you can still be confident, but not 100% confident. There will be always some surprises.

Awesome. So I think this is the right time we should start talking a bit about Quint itself. What problem does Quint solves and what is the gap that you are trying to fill with it?

Let me give you how Quint started. Okay. So what problem Quint was born to solve. And that was a problem that TLA plus was really useful. But if you went to your colleagues on your team and asked them to, Hey guys, let's try the TLA plus model for this because that will help us solve our problems.

They probably say no. Or even if you did, okay, I'm going to do it myself then. You don't want to do it with me. I'm going to do it on my own. And then you go and write the model and like, hey, look, I wrote this amazing model.

I even found bugs with it and we fixed those bugs. Look how amazing this is. And the guy is like, oh, yeah, that's pretty cool. But yeah, I have to learn this language. It always goes like into the drawer.

Right? So hard. Even if a person is finding a lot of value, it's so hard to expand it within Teams. There are a few companies that have succeeded at this. So this is the problem we were facing.

We wanted to... We're using TLA plus We were having success stories with it and still we could not convince engineers to adopt it, to even read the specs that we wrote. We're not even telling them to write specs themselves. So we were like, okay, we need a better language and some better tooling as well that has more like what developers expect. And by better language, I mean actually a language that's more suited for developers because mathematicians, they like TLA plus as well a lot.

I had a student that actually had a PhD in mathematics and in my classroom, I would allow them to do the tests in either TLA plus or Quint. They are very similar to 2 of them. So I'd explain the 2 and they could choose. And this student, he picked TLA plus and he was very happy with it. He loved the syntax.

He loved the mathematical stuff that he was used to. And he had trouble with the programming syntax. Right? So I'm not saying like the syntax is better in all regards, but we were thinking about the engineering field and developers. So beta syntax was more fit to that and the tooling.

The tooling then started to evolve because we realized when we give a specification, when someone goes and like is learning, try the specification and they finish, they type the last character and like, okay, I'm done with my specification. How do I run it? And how do you run a TLA plus specifications? The answer is you don't. You run the model checker that verifies the context.

You don't like get like TLA run and then pass the file. Like there's no such thing. And we were like, okay, people really need that. So we addressed that gap. And you're like, okay, Quint, run.

And for that, we implemented a simulator. So it's very simple, like random simulator. And we started leveraging the simulator a lot. And then we learned so much just by using the simulator, which is not doing form of verification, right? It can still miss some scenarios.

But then we learned there's so much value in just the formal specification part, not necessarily verification. And then we started leveraging this more and more. And then AI came. And AI... So since the start, was trying to do...

What I was trying to do with my life, right? Is reduce the cost that it takes to get value out of specifications in general, right? So TLA plus a lot of costs for engineers to learn, let's reduce that. Or the tooling is too hard to onboard, so let's reduce that cost. Or the model checker takes too long to run and I don't know how to optimize.

Okay, you can run the simulator. Reduce the cost and also increase the value. So how can you increase the value of specification? Oh, you don't only find bugs. You can also connect it to your testing environment and have better tests.

Oh, you can also do this. You can also do that. You can also have better maybe onboarding material because your other people can go and like start playing with this instead of like reading extensive documentation. Thinking a lot about different things on improving value. AI came and it did both, right?

Because AI came and like, okay, now the cost is basically 0. You can just ask an agent to write it for you. Done. Perfect. And the value is also like, okay, now we have this tool that writes code for us, but how do we know if it's correct or not?

Like everyone's wondering this. And then like formal verification comes as this like obvious solution. Of course, like formal specification can just go and like checks if your code is correct or not. Suddenly we were like, okay, are so many things we can do with Quint, right, as a tool. And what do we want to do?

What do we believe in the most? Like, oh, we can do it. We can do a design tool. So we can do a plan mode with formal specs. We tried that.

It works quite well. Very exciting. We have some open source skills that help with that. It's very, very nice. My main outputs I had with that experiment is that it asks better questions.

So during like normal plan mode, it was like, oh, do you want this file to live here? Like it asks some like low level questions. I'm like, I don't care. And with the the plan mode, it was asking pretty smart questions because it was trying to write this formal spec and then, oh, what should I do in this scenario? It was asking some some smart questions.

So that was, I think, the main output from that experiment. It was nice. But like, oh, but this is not the most pressing issue. People can still like do design and stuff. What is the most pressing issue?

And it's again, how... I have this... All this code. How do I know if I can ship it? Right?

That's the most pressing issue. Like, okay, we can do stuff to help there, but what do we do? And then I realized, as we already have a bunch of prototypes ourselves and hitting those problems ourselves, I was like, oh, Claude has written for me 400 tests and I have no confidence whatsoever in any of these tests. Okay. So it's testing a bunch of stuff.

Every time I look at the test, it seems stupid. It's just searching some stupid thing. So I don't have any trust of making changes in the software because I don't trust any of these tests. If I go back to the open source point that I was writing before, I wrote those tests. I trust them a lot.

So I'm way more like, I feel way better about making changes there than on this where the cloud has written tests. So like, oh, we have actually a big testing problem. We are trying to do something super fancy with formal verification, but now we actually lost trust in the thing we are using for years in the industry, which is tests. Okay. So I like, maybe let's take a step back and try to solve the testing problem.

So to finish the answer, the gap we are trying to address now Quint and packaging Quint inside their products, it's called Quint Studio, but it's basically like a easier version to use. It's not like the language itself. It's like a tool where you can click around to use things. And in the main gap we're trying to address now is how can you trust your tests again? And the stuff we're doing is basically taking your test, your existing test tools, and playing them against the model, the formal models that we also write, we generate with using agents.

So we generate the model, we run your tests to make sure that the model is like producing your tests. And then we see like how many behaviors are actually covering and how many important behaviors of your system is uncovered by tests. You are never exercising this like super important behavior. You might want to do that. You're never exercising this transition.

You might want to do that. And I think like having this language with humans, right, between AI and humans be these behaviors, right? This is the correct behavior. This is an incorrect 1. I think it might be a good solution to this, like cognitive problem we are having as well when developing code with AI.

That's what we are trying. Let's see how much people pick it up.

Yeah. Yeah. Thanks for, you know, taking us through the journey and, you know, how you came to this problem statement. When you talk about tests and gaining confidence back in our tests, what kind of tests are you talking about? Are these like unit level tests, integration tests we are talking about?

Because I was trying to understand when we run the spec and we gain confidence, and let's say the spec is telling us these behaviors are not covered, how does the spec know that these behaviors are actually possible to test in that environment? So 1st, what kind of tests are we talking about? And how does the spec identify if that is really testable in a test environment?

So you're talking about all the different kinds of tests, honestly. So what we do now is we instrument the the code, the actual source code with, some... Like, this is when... So let's choose the bank example. Right?

So we have withdrawals and deposits and transfers. So whenever in the code you do like a withdrawal, you log like, oh, I did a withdrawal of this value or I did a deposit of this value. And then we go and run your test suite And then we see what is exercising those functions, right? So whatever test you run that printed withdrawal, that's because it exercises that. So if...

Depending on if it's a unit test or behavior test, like end to end test, integration test. If it's exercising that, we can measure it and compare it against the model. So we take that and then replay against the model and see if it's like the model is compatible. It's like modeling the proper behaviors. And then in order to tell you what tests you're missing, right?

You're going to think about behaviors you're not testing and then tell you, oh, you should test this. And then on the product we have like little buttons, okay, add the test for this. And then you're right, because it's not always the case that we can test it. Like we were just talking about the tumor risk simulation testing and how like sometimes you cannot really control your scheduler and then it's hard to do that. So we don't predict this from the model stance.

We 1st tell you what scenario you should be testing so you can evaluate also like, oh, this is actually something important. I should be testing that. If you try to test it, it might be the case that, oh, it's impossible to test this. We feel don't refactor your code. So you'd need to like isolate, for instance, the scheduler and receive this as a parameter.

And then here, then you can exercise this behavior. So it would like suggest you some refactors. We have some ideas also like how to integrate more like something like the deterministic simulation testing. I think there's a lot of interesting things to explore there. But, yeah, it's a it's a problem.

Understood. Let's take an example here. Maybe it will also help, you know, understand the whole process. So let's say I'm working on, I don't know, a database system or... Yeah.

I'm working on a database system, and then I add a new functionality. And so far, my team, let's say, hasn't been using any, you know... Haven't used any formal specification. But I, as an engineer, I still feel that, okay, we should use some formal specifications so to find more bugs beforehand, before going to the production and so on. How do I do that?

And how frequently do I run the spec? Is it run on a periodic basis? Like, for example, any change we make, we build our artifact and we... The tests are run and then the CICD pipeline. Again, there are some of the tests that are running.

And eventually, it goes to production. But how does the spec execution tie with this traditional way of, you know, deploying software?

Well, so if you make a change that might... So... And and say you're insecure about your change. Right? It might be that the case that your change is like a whole design, and then you want to check that standalone.

Most likely, like if it's just a small change... Well, let's say you're making a change and you want to make sure you didn't break any existing behavior. So you have a lot of behaviors that were desirable, a lot of behaviors that are undesirable, and you're just like, say, making a performance optimization. So you don't want to change in behavior. That's 1 type of change.

Other type of changes, oh, you're adding new behavior and you want to make sure that behavior is correct. Like those things are very different when it comes to what you do with the spec. Right? And we are trying to address all of these different cases. Or you also can be like removing a behavior.

So if you identify some behavior that is a bug, you don't want it. So now I want to remove the possibility of this behavior to happen. And then now I want to make sure I ship something that doesn't have this behavior anymore while keeping other existing good behaviors. So basically talking about a behavioral diff. You're adding, removing, changing, or maintaining behaviors in the case of a refactoring or performance optimization.

So in order to talk about a diff, you have to have a baseline. Right? So if you're talking about evaluating what a change is doing, you 1st need to go remove the change, right? Go to the head of your git and check and make a spec for that. Whatever scope your change is in, right?

So if you're making a change in this module of the database, maybe let's model that. Make a quick spec for that part. Generate that. That would evaluate your tests. Might be also a good idea to improve your testing suite.

Right? So if you have a lot of like blind spots in your testing suite, so things that are not covered before you go and make the change, you might want to cover those to make sure you are not going to break things. This is very similar to things we do with legacy software, right? When you're going to change legacy software, what do you do 1st? Test the hell out of it.

Test it a lot until you're confident that your tests are covering everything you need and then you can make changes confidently. It's very similar, I think. I think it's a very similar thing with what we have to do with a lot of AI generated code. And like when you end up with a project, oh, it's amazing project, but the code is very bad and AI generated. So what do I do?

Test the hell out of it and then you can start maintaining it. So making a change, maybe you can... You will be able to make the change with more confidence if you 1st test a lot of the stuff you had before and you want to preserve. Like you want... Trying to preserve what you had before while making just this change and not changing anything but accident.

And then you have then a spec that is linked to your existing tests that are hopefully good tests. And now you have a change, right? And then for this change, 1st of all, if you try to replay this change, so you don't touch the spec at all. Everything's the same. Just make the change to the code.

If you now try to run your tests and replay those behaviors against the spec, you're likely going to find a divergence, right? Because you changed the behavior of the code, but you still have not updated the spec. So this is a good way to not forget to update the spec, right? So you this check-in the CI and you see this check is just running your tests and replaying them against the spec. It's not doing any like agents, please check if my spec is not out of date.

It's just running your tests with instrumentation. So you do that in your CI and CI say like, hey, you forgot to update the spec. You should have updated the spec because you're changing the behavior. Did you notice by the way that you're changing the behavior? Because you are.

You should go and update the spec. And you're like, oh, 0, true. And if you were changing behavior by accident, that's when you would notice that and make like, oh no, I didn't mean to change behavior. Was just trying to factor this. Okay, wait, let's discard this PR and try again.

And if you are changing the behavior like, oh yeah, that's true. I'm changing the behavior. I should update the spec. So you go and potentially ask your agent, go, please now and update the spec for me. So using Queen Studio, that would happen automatically.

And then now you have an updated spec. So it's not the... If you're using spec also as a form of documentation, something that doesn't go out of date. So I hope this answers the questions about how you use this over time. But I think the problem of the spec going out of date only happens if it's...

The spec is not connected to the code at all. If you have connections of the spec to the code and there are different ways of doing that, then run those connections in the CI, and you can see when spec got out of date.

Okay. That makes sense. And it looks like a lot of it, again, is based on behaviors. Right? Like, how well we define behaviors and when we are changing something, if a behavior change or not, and then making sure that the spec is always kept up to date for those changes and if they touch behavior at all.

Talking about behaviors again a little bit. So if we talk about, let's say, at the front end user journeys, so I think a behavior is a bit more clear. When you talk about distributed systems, what is a good example of a behavior and what is a bad example of a behavior?

Well, a behavior... The definition of a behavior in the context of QUINT and other formal methods is a sequence of states. So you start in an initial state and then you go to other states in sequence. I think it's easier to explain if you think about it as a sequence of steps or transitions. So you start in the initial state and then you make a deposit and then you end up with a different amount of money and then you make a withdrawal and then you end up with a different amount of money.

So you're like making transitions and changing your state over time. If you think about the model as a state machine, the behavior is 1 path inside the state machine. Right? So 1... You can draw like with a pen, 1 path.

That's 1 of the behaviors of the state machine. In the... Yeah, sorry. In distributed systems or concurrent system, an example of a behavior would be like for mutex. Right?

I don't know. You have a process thread A and thread B. Thread A acquires the lock. Thread B tries to acquire the lock and fails. So let's say blocks.

Then thread A does what it needs to do. Thread B is still blocked. Thread A goes and exits the mutex. Then Thread B acquires it. And then Thread B releases it.

So like that sequence is 1 of the behaviors. Another behavior would be if Thread B acquires the lock force, right? That's a different behavior of the system. All of those behaviors are permitted. A behavior that is not allowed by that model if you implement the mutex correctly, is a behavior where both a and b have the mutex at the same time, have blocked the same time.

So that would be like a bad behavior in this definition of the... Of a right mutex.

Okay. That that makes sense. And... But I I think by bad behavior, I I meant in terms of defining behaviors. So so good behavior is, as you mentioned, like, thinking of your system as a state machine and then talking about 1 path in that state, like how it starts and then how it terminates and what is the path taken.

But how deep and how shallow should I take that path? For example, it has to be like a complete path for you... For a journey to happen, or it's just about, let's say, talking about mutexes. Is it is it just about, okay, thread a takes the mutex and then thread b is waiting and then thread a releases it and then thread b takes it. Should I stop there?

Or should I also go forward and take the next step as in tie in 1 behavior, as in what thread a is doing next and then what thread b is doing next, and what happens to the mutex. So at what time... At what point should I stop that, okay, this is like a boundary of a behavior versus extending it to, you know, further steps that the threads are taking?

Good question. And the answer is the same as we talked before about what is a good model. It's a model that's good enough to capture problems. So what defines the scope of a behavior is also what defines like adversarial surface. What's enough to capture good and bad things.

There is no like absolute right or wrong answer, right, to that. It's just like, if you think about all the different things that Tread does in their lifetime, it's probably going to get out of scope, too big to reason about, to mix a lot of concerns in the same scope, and it would be hard. So the the level of granularity of a behavior is whatever, it's a good... Makes for a good spec. Right?

What we do is we start by the spec. The 1st thing we do is writing a spec for a component. Actually, 1st thing we do is scanning the code base for the different components. We call it components. What are components?

Different state machines. And it could be like the whole code could be 1 state machine and that would be useless because it's like way too big to do anything interesting with. So we don't do that. We go and like find small enough state machines that are big enough to do something interesting. Oh, this is an interesting state machine here because there is a mutex here.

So in this part of the... You're talking about e commerce, acquiring, putting an item in your cart, then the other cart. There are some mutexes needed there. Oh, this is interesting. There's a carts, mutex.

This is an interesting state machine. Let's take this. And what's the adversarial surface here? Oh, what if 2 users try to add the same item to the cart at the same time? And then how does the inventory deal with that?

Oh, that's an adversarial surface. Let's make sure the model can cover that adversarial surface. Oh, now we have a really good model. Now let's create quint version of this model. And now let's make sure the tests they're good tests for this, the behaviors of this model.

The model ends up defining the scope of the behaviors, right? But, yeah, it can... They can be... Behaviors are... It's a very like arbitrary word.

I guess it could be like a lot of things. All that happens in the lifetime of HD.

A lot

of things. Right? So you have to find a good level of granularity.

Okay. Yeah. I mean, that's that's where talking about nuances and different cases come into picture. It's not like Yeah. Yes and no answer.

It's pretty involved. And probably it's a learning journey. Right? Probably you would define behaviors that do not capture anything or you would define behaviors that are just too extensive. And then you will learn along the way based on your experience with specs, you know, you would probably define behaviors in a different way or, you know, be correct about it.

So, yeah, I think it makes sense. Talking about the the the hardest problem that you faced, let's say, while solving this problem with Quint, like, the problem that you mentioned with TLA plus I think it's true. It's faced by everyone, but it's still, like, let's say, the gold standard of, you know, formal specs. Companies have used it too. For example, AWS found, you know, critical bugs in AWS s 3 using TLA plus What was the hardest challenge for you guys to sort of reduce that accessibility gap and building Quint, which is more accessible?

What kind of trade offs did you have to make? What kind of design decisions did you have to make?

Well, there's so many. Well, think the... I can talk about, I guess, the most recent 1. And a question that I get a lot is like, where does Quint live in the life cycle, in the software development life cycle? Like, at which point should I use it?

And I think that just the answer changed so much because before AI, we would think a lot about formal methods, formal specifications as something you would do at the design phase. So because it was so expensive to write code, So the sooner you catch bugs, the better. It's so true that the sooner to catch bugs, the better. But now I think even the design phase can involve a lot of like code if it's cheap to like just put something together. So I think it's all mixed up.

And I actually think no 1 knows what's going on. Like everyone's still figuring out what is the new developer life cycle. There are so many like different proposals. Like if you go to LinkedIn, every single post is like proposing stuff. No, you should do this.

No, you should do that. This is a better way. So figuring out what is the best entry point for PointNote because there's so many opportunities. As I said, we tried this design tool and it was good, but then we're like, okay, but is this the best entry point we can get to get people to start trying it, to start experiencing it, to seeing it that is not like this. Oh, I should only do this if I want to be like absolutely sure about something.

And also a lot of people have the expectation that it's just like a check mark. So it will... You give it a job to do and it will tell you proved or not proved. And that's it. You don't have to do anything else.

But it's so much more involved because I don't... Again, I don't believe in confidence without understanding. So you're like having to do... The the hardest and also the most rewarding part of this, like making it more, for us, it's more accessible is bringing understanding. So instead of like coming to you and say like, Hey, you should really use Quint because it will prove your software.

I don't really believe a lot in that story. I believe much more in the story like, hey, you should use Quint because you understand better what your software is doing. And therefore you'll be able to ship it more confidence and it will be better to help you understand what your tests are actually testing. Even if they are generated by AI, you're going to understand your tests, improve your tests. And then you feel more confident because you have more understanding.

So I think the biggest challenge with this is like pushing understanding. And again, AI is helping because AI is making it very clear that we are not understanding something. It goes and writes a bunch of code for us. And they're like, okay, what is this thing they've been doing? And Quint helps with understanding it.

Think that's the story I believe in the most of all different stories because I've seen it. I've witnessed it. I struggled a lot to understand some of my protocols. I was working company that... With a company that did a lot of like Byzantine fault tolerance.

Super complicated. I am not from this area. I'm not from distributed systems. I struggled. And then Quint really helped me understand very complicated things just by going, looking at the spec, writing specs, running the simulator and seeing like, okay, how...

When does... Is this mechanism of the protocol really necessary? I cannot really think about scenario where this is needed. And then Quinn comes and presents a scenario for me. Oh, that's how...

Okay. And I see it now. How can disagreement happen when you have too many Byzantine nodes? Because that's how it works. Right?

If you have too many Byzantine nodes, malicious nodes, then you must have disagreement. That's what the math tells you. But how? How does that happen? You can go and see how that happened.

You're like, oh, okay. Now I understand. That's great. And it feels great. So...

Yeah. How... But how do you convince people of that? I think that's the hardest part. And how to make it super easy.

Right? Because the more barriers you have in order to get that feeling before you get that feeling, then the less likely people are to go all the way. So a lot of challenges, but I'm very passionate about the problem.

Interesting. Very interesting. And I think the thing that you mentioned about confidence without understanding, I think that's the key there, right? Like you can be confident, for example, that, okay, I trust my agent to do the right thing, and that is a different type of confidence. Right?

But if you are if you are confident that whatever you are delivering in production, along with this solid understanding of the behaviors or the, you know, the properties of your system, I think that's the next level. And bridging that gap is absolutely important. And I I also face this problem every day, like using AI agents for writing complicated code. And at what point should I stop and, you know, take a step back and, you know, oh, hey, do I really understand what's going on? I understand the test.

I understand the code. I understand, like, a high level plan in my mind, like, what is this trying to do? But what gives me that understanding? And then I end up, let's say, reading a lot of code, asking a lot of questions to the AI, and then probably it can hallucinate, explain me something differently. So I think it boils down on to me, you know, asking the right questions to the AI agent.

It takes a lot of effort to actually be confident along with understanding. And if that is made easier for me, let's say, with using Quint, I think that that's a big win. So, I totally get that problem, and it's it's a really hard problem and and and a good problem to solve, to be honest. So that's amazing. Talking about...

You mentioned that people use Quint and share some success stories, some experiences with you. What are some of the, you know, the... Let's say, the the best examples you could share with us where Quint solved the problem for a company or for a for a for a individual, be it simplifying the process, be it identifying some critical bugs, or just, you know, saving a lot of cost in verification of the software.

Okay. I do want to comment on something you said before. I will get into the use cases. 1 2nd. Yeah.

You said like, oh, yeah. Asking the right questions to the AI agent so they help me understand. I I feel that a lot, and I see people sharing online a lot of cool ideas about how to do that. And it's like, oh, yes, it's AI to explain with like with this, with that. And I feel like we could all use some more structure, right?

So if we find a good way of understanding things and then you just put that in like a little framework that AI can use. Then we just repeat that and always have the information in the same structure. Everything now is like either text or just like arbitrarily generated HTML artifacts with some diagrams. And it bothers me. They are like different all the time and they're not like standardized and there's no structure.

So I'm advocating here for more structure. I am trying this with behaviors in Quint. This is what I'm doing to contribute, but I think there are a lot more things that can use more structure. So this is my pledge here. Going back to the use cases we have.

My favorite user stories are when people find more understanding, right? So I understood this better because of... That's my personal favorite ones. And I have some of that. But the most, I guess, impressive stories are about finding bugs and about preventing bugs before they happen.

We have a few of them. We we were doing some like audits in the blockchain ecosystem. So we prevented like, I don't know, millions of dollars in a migration because we found some bugs in the migration before it happened. That was using Quint. That was quite nice.

More recently, the Terso database team, they published a blog post where they found 10 bugs in SQLite using Quint. Right? So the idea was very they... Similar to what we've been discussing here. Like, you know, when you're trying to like rewrite a system, like a legacy code and you 1st go and like test the hell out of it.

And then you're like, okay, now those tests are enforcing the behavior, correct behavior, so I can easily change it. They were doing something similar. They were doing that for SQLite. So they were trying to capture the behavior of SQLite such that they could put that in terso and make sure that it also has the same good behaviors since SQLite is like more battle tested. So that's the context in which they were using Quint around SQLite.

They're not like necessarily trying to find bugs, if I understand correctly. But they ended up finding a bunch of bugs using Quint in SQLite. And some of them were fixed upstream. So that was a pretty nice use case and completely external as well. It was like just a person from interest doing the things and telling us what they did.

It was pretty nice. And then the 1 that I like a lot is a company called OpenHands. They're using a Quint already with AI. They are like a genetic company. So they were using the...

We have a Quint LLM kit, which is open source, a bunch of like skills to use Quint with. They had that plugged in and then they had a bug happening in production in 1 of their Kubernetes deployments. So they would deploy things to Kubernetes. And after a few weeks, it would start like triggering alerts for them because there was a race condition. And they're like, oh, we have to fix the race condition.

So they prepared the fix. I think they actually... They shipped the fix, but they were also like, I wonder if this fix is actually going to cover all scenarios. And they asked, they said like they asked Quint. So they went to the agents that were having this Quint skills.

Okay. Is my fix good? And then quint like model the race condition that they were having in production, model the fix. And I was like, oh, nope, actually it's not a good fix because in this case here, it won't fix the problem. And that actually happened because they had applied a few weeks past and they actually got the alerts for that problem and that actually happened.

And then they experienced a bit of couple of other fixes and then there was finally 1 that Quint approved. So So they shipped that and didn't have any part problems. So we named the blog post. Quint told me no. Right?

So it tells, it tells you no before you go, I can implement something. It tells you like, oh, that's not gonna work. So it's a good way to validating the design as well. And then this person, AI Vong, used Quint and she came to us just to tell what happened. We didn't have any influence on this.

She just came to us on a call and we were talking about it. And she was oh, and it was so much better because this is a part of the Kubernetes cluster that I did not understand. It was part of the code that I, it was so complicated. I didn't understand. But after doing this with Quint, now I feel like I understand it.

I can do more things with the code. So that was my favorite part of the report. It was not really like the bug finding 1. So, yeah, that those are some some stories. Hopefully we'll have much more, especially with, the tests.

I'm really excited about the test story. I'm looking forward to have some some cool use cases about that as well.

Impressive. Awesome. Yeah. I think bridging that gap, giving confidence along with understanding, I think that's that's a big win for a software engineer, especially in the AI world. So before we wrap up the discussion, do you have something specific to add about Quint?

What do you think our audience should know? How they can check out? How they can try Quint? Anything, how they can reach out, or just general tips and recommendation around formal specification, yeah, feel free to add that.

All right. Yeah. So for Quint, Quint, the language is completely open source. Our LLM agent skills things are also open source. You can find them on GitHub.

We are developing a product called Queen Studio, which just puts everything both in a UI and an MCP server, makes things easy to use. And then it's more focused on improving your testing suite and also can find bugs in your system, generates the spec automatically for you with a lot of techniques that we've implemented with this matching of your current test behaviors with the model to make sure that they are the same thing, all using agents, all automatically. It's a local tool, you install it, run it with your own agents in your machine. And we have just launched the beta this week. So we are recording, can I say that this is recording in September and we just launched the beta?

So if you wanna sign up for that, probably can give you access pretty soon. So that's 1 thing to try about Quint Studio. You can try Quint Studio. You can try Quint Open Source. And there's a bunch of our documentation website.

We have blogs. And I would also tell you that you should follow me on LinkedIn. I post a lot about these kinds of things. You can find my name there on LinkedIn, but I'm boogarela on every on every social media. So I think that's all.

Yeah. You should be able to find all the information in our website.

Yeah. I'll also make sure that I add all the necessary and interesting links that I found around in the YouTube description so people can actually check it out. Of course, you can always reach out to me if you have any questions. But, yeah, thanks a lot, Gabriela. It was a wonderful discussion learning about Quint, about formal specification, the problem you have been trying to solve.

And I think it's an important problem. So thanks for, you know, paying attention to that.

Awesome. Thank you so much for having me. This was a plus.

Thank you.