Latest / Superlinear / Coding Agents Just Changed Formal Verification Forever | Poteto's Skill, Bend2, Drifting Models

Transcript

Coding Agents Just Changed Formal Verification Forever | Poteto's Skill, Bend2, Drifting Models · Superlinear

• 0:00
  Christine: There's been so much security news this past week, including critical PHP vulnerabilities that led to many websites being taken offline.
• 0:08
  Christine: It's a reminder of how hard it is to catch every bug even with extensive testing.
• 0:14
  Christine: And then Anthropic published something pretty remarkable. So they used Claude to prove that certain parts of over a hundred open-source libraries cannot crash under specific conditions.
• 0:27
  Christine: And what's interesting is that this is becoming practical not only for big labs but developers are starting to build this way too.
• 0:36
  Christine: So today we're talking about whether we should be using formal verification when building software with coding agents, how to start doing it, and we have some really interesting possibilities to share with you about how to formally verify your code in a more direct and easy way.
• 0:55
  Christine: So, Brandon, why should developers start thinking about formal verification now?
• 1:00
  Brandon: In a few words, it's that overengineering is now regular engineering.
• 1:03
  Brandon: Things that were super expensive, required specialists, we can do easily with agents. Agents can help write specifications, they can run verification tools, and they can automatically fix counterexamples. And using formal verification can give the agent strong feedback to push your agents to write the kind of software that you need faster and better.
• 1:32
  Brandon: And if you don't do it, then you're gonna be left behind.
• 1:35
  Christine: Yeah, and I guess coding agents are not just faster and better at building things, they're also faster and better at breaking things and finding vulnerabilities. So it's really important that we also, I guess, level up the way how we build software.
• 1:50
  Brandon: Yes, yes, yes.
• 1:50
  Brandon: Defensive co-scaling.
• 1:53
  Brandon: If we're worried that agents are gonna find a lot of bugs for us, then we need to put more work upfront when we're building software to prevent bugs from existing in the first place.
• 2:04
  Christine: That makes sense. And we're talking about formal verification, but what is the actual difference between running tests and formally verifying code?
• 2:14
  Brandon: You can ask your agent to write a hundred tests or even write tests that generate hundreds, thousands, hundreds of thousands of examples.
• 2:24
  Brandon: But what formal verification does is it proves that some piece of logic is correct in all scenarios, not just for the specific examples that you've tested.
• 2:35
  Christine: Right. So instead of just testing more and more cases, we can mathematically prove that a particular kind of bug or bad situation cannot happen under the condition that we're checking.
• 2:48
  Christine: Right? So I guess that makes what Anthropic did across those open-source libraries really powerful too. Just for my understanding, though, can you give an example of how formal verification is applied? Like, what is exactly being proven?
• 3:12
  Christine: How does it work?
• 3:13
  Brandon: Each tool is different, but I'll just pick a really simple example. So let's talk about reversing a string. So, I'm saying, OK, if I have a function that takes a string, like hello, and I would get back O-L-L-E-H. If I write tests, then I would come up with specific examples and then those are unit tests.
• 3:35
  Brandon: Or I could even generate lots of examples that could be a property-based test.
• 3:40
  Brandon: But what's happening is I'm actually running the code and trying to find a bug.
• 3:44
  Brandon: When we use formal verification, we can prove that reversing the string meets some specific property. For example, if I reverse the string twice, I wanna get back the thing that I started with.
• 4:00
  Brandon: So if I reverse hello twice, I get back hello, for any string I put in.
• 4:05
  Brandon: And when we use formal verification, we actually prove this is correct by taking a model of the logic and we can in this case use, for example, mathematical induction to say, OK, if I start with an empty string and I reverse that, here's what it means.
• 4:25
  Brandon: And if I have a string that already is halfway reversed, like here's how I reverse the next part of it. So we reason about the code mathematically to prove in any possible scenario that it's correct. It's kinda crazy that computers can do this in the first place, but they can.
• 4:45
  Brandon: So we should take advantage of it.
• 4:47
  Brandon: So yeah, so reversing a string obviously is like very simple, but imagine you're making like an elevator or a traffic light.
• 4:55
  Brandon: You can talk about, for example, that you always see a yellow light if we start at green before we get to red.
• 5:04
  Brandon: We can prove that's true.
• 5:06
  Brandon: We can prove that, for example, if I'm refunding my user that I don't refund them twice in certain scenarios.
• 5:12
  Brandon: You can prove that your application that's doing lots of things at the same time that are all waiting on each other, that it never hangs, it never stops, and always eventually shows something to the user within some deadline. These are examples of things you can prove with formal verification.
• 5:29
  Christine: So, does it work like this?
• 5:32
  Christine: So you describe the behavior that you want as an equation, as a mathematical equation, and then you prove that in certain conditions there's no way that equation can have like the bad outcome, the bad behavior.
• 5:51
  Brandon: And what's really cool is with a lot of these tools.
• 5:54
  Brandon: So it's different for different formal verification tools. But some of them your agents have to do some work to prove it themselves.
• 6:03
  Brandon: Some of these tools will do that for you.
• 6:05
  Brandon: And some of them will give you the specific counterexamples. So imagine that I wanted my traffic light to never miss the yellow, but under this specific set of conditions, if it's raining on a Wednesday, the yellow is skipped.
• 6:23
  Brandon: Well, with a formal verification tool, you can get a specific trace as output when the proof fails, which your agent can then immediately ingest, fix the bug, and move on.
• 6:36
  Christine: It sounds like if we can use formal verification, it can really prove the behavior or guarantee the behavior of our code much more reliably and robustly.
• 6:46
  Christine: But it also sounds like it could be very complex or difficult to apply it. It feels to me like there's a big hurdle to overcome.
• 6:57
  Christine: Maybe you need to know math, maybe you need to learn these new formal verification languages, but I actually remember that, or saw on socials, there is this really accessible skill that people are now talking about and using. Actually, you showed it to me.
• 7:16
  Christine: Can you jump into that a bit more?
• 7:19
  Brandon: Yeah, so there's a new skill in pstack, Lauren (Poteto)'s project, called Create Formal Verification Skill. And this is really cool because what it does is it will do all the hard work for you.
• 7:35
  Brandon: It'll look through your code base to find something of high value to formally verify so you don't have to worry about that. It'll choose the correct verification tool for you.
• 7:45
  Brandon: It will set up the verification for that property.
• 7:48
  Brandon: It will then make sure that it's actually proving the right thing. It'll generate a skill so that future coding agents can re-run and maintain that verification for you. And basically it does the full thing end to end.
• 8:02
  Christine: So I do not need to know or choose the verification tool or the language.
• 8:05
  Christine: I do not need to know like where exactly and how to apply it even.
• 8:11
  Christine: It does everything for me.
• 8:12
  Brandon: Yes. You can stop there and it'll work.
• 8:16
  Christine: There's something that I feel we need to dig into a little bit more because when you use a formal verification language, I guess you typically write a model, right?
• 8:30
  Christine: For example, TLA+, you typically write a TLA+ model and then you formally verify that model.
• 8:37
  Christine: Am I then actually proving that my application code is correct? Or am I just proving that model is correct?
• 8:43
  Brandon: Yeah. So in that example you're proving the model is correct. So you need to make sure that the model, which you can just think of as another version of your code that's simpler. So you have to ensure that your real code matches your model code.
• 8:58
  Brandon: And then the thing that you're proving makes sense.
• 9:02
  Brandon: And then you have to make sure that the model code stays in sync with the real code.
• 9:05
  Brandon: With a tool like TLA+.
• 9:08
  Brandon: So there are tools, for example, Bend, which we talked about a few weeks ago, which allow you to prove or formally verify your actual application code. So the model is the same as your code.
• 9:22
  Brandon: And this is really powerful.
• 9:23
  Brandon: And I think this is something that we'll talk about more. Bend is really cool and you can watch our other episode to learn more about Bend.
• 9:31
  Brandon: But there's other ways that you can allow your model that you're formally proving to be something that actually lives in your application and is your real application code.
• 9:42
  Christine: Right. It feels like that's something really important because especially now with agents constantly modifying the code and building faster, the model could become outdated pretty quickly too. So even if your proof passes maybe your actual code could behave differently.
• 10:00
  Christine: So what happens exactly when an agent makes a change that invalidates the proof or the model?
• 10:08
  Brandon: If the underlying code hasn't changed and the model of that code hasn't changed, then the proof can't be invalidated. So if there was a proof, it's always true. That's sort of the nice thing about these things. Now, if your code changes in some way, then if your agent doesn't update your model of that code, then you're proving the wrong thing. So that's bad.
• 10:31
  Brandon: If your code changes and the model of your code changes, you could fail to prove the property.
• 10:39
  Brandon: I'll use reversing a string.
• 10:40
  Brandon: If I change my function that reverses a string to add the letter A to the end of the string, then thank God that my proof fails if I try and prove that it reverses all strings because all strings don't have A at the end of them.
• 10:58
  Brandon: Right? You do have to reprove the code or you have to reprove the model every time that it changes and it needs to change when the code changes.
• 11:11
  Christine: So this is like really the pitfall or the catch when using formal verification. Like there's a lot of advantages to use it and benefits but this is really what I guess we need to watch out for.
• 11:25
  Brandon: This is something: it scares me.
• 11:27
  Brandon: It scares me a lot when I'm working with these formal verification tools because it's one of these things that we talk about a lot like hope and enforcement. We have to hope that our agent is knowing that when I touch the code I should update my model. There's no way to enforce that.
• 11:48
  Brandon: Well, not out of the box, but maybe we will talk about some ways that we can get better.
• 11:55
  Christine: Yeah, so even though formal verification is so reliable, so robust, but actually if you miss this part, the connection between your model and the code that you're actually proving, it doesn't mean anything. You still end up with bad verification.
• 12:11
  Christine: So what are some approaches to solve this drifting of the code from the model?
• 12:17
  Brandon: I think the easiest thing to do is to just choose a formal verification tool, if you can, where the model is the code by definition. So, Bend, for example is an example of that.
• 12:36
  Brandon: So Bend code is your application code and that same code is the model by which you're proving properties against. So that's a simple example.
• 12:50
  Christine: Wait, before you continue.
• 12:52
  Christine: That's very unique to Bend, right?
• 12:54
  Christine: Like the traditional formal verification languages like TLA+ and Lean, they're all proving the model and not the code itself that application is running on.
• 13:06
  Christine: Is that right?
• 13:07
  Brandon: Yeah. There's Lean, Idris, Agda, Dafny and then there's a new one, Bend 2, which we talked about in another episode. These tools all can prove kind of general-purpose things.
• 13:20
  Brandon: They all have different proof systems underneath them. And Bend's whole thing is it's like the first general-purpose programming language that you can use to build real applications depending on who you ask.
• 13:34
  Brandon: But that's how I see it.
• 13:36
  Brandon: Whereas these other tools are kind of built for formal verification and while maybe you can build applications in them it's sometimes a little gnarly and difficult. So if you wanna learn more about Bend you can watch our last video on it.
• 13:51
  Christine: Cool. So the Bend 2 from Victor Taelin actually closes that gap between the model and the actual code that you're running so that fills that hole that we just talked about.
• 14:05
  Christine: Like, OK, what if even though formal verification is so robust what if you're not really proving your code? OK, that's cool. So does that mean if we all want to do formal verification from now on and let's say if Bend becomes a mature ecosystem, we should all just program in Bend?
• 14:25
  Christine: And not use any other programming languages anymore?
• 14:28
  Brandon: So each of these formal verification tools has like a proof system underneath it that powers it and makes it really good at some things and less good at other things. And tools like Bend or Lean they're not suited for proving properties on state machines in the same way that TLA+ or Quint is, where I can say like my traffic light always has yellow in between going from green to red and these kinds of state machines show up in our applications that we write all the time, like they're so common and so it's really useful to have tools that let us state these properties, these temporal logic
• 15:20
  Brandon: properties: eventually, never, always,
• 15:25
  Brandon: and then something about our states. And so that kind of leaves us with this ache, this pain of like, OK, there are cases that I wanna use some kind of temporal logic checker system like TLA+ like Quint, but TLA+ and Quint, they work on a model of your code, not your actual code.
• 15:58
  Brandon: So it's something to think about.
• 16:02
  Christine: So it's not solving that problem that we just talked about, how the model or the code could drift from the model.
• 16:09
  Brandon: Exactly.
• 16:10
  Christine: So then we're still stuck with the other languages and there being a gap between the code that you're actually running on and the code that you're proving.
• 16:21
  Brandon: That's what you'd think. That's what you'd think.
• 16:23
  Brandon: But let's just think outside the box, right?
• 16:27
  Brandon: So, look, TLA+ is software.
• 16:32
  Brandon: Like, it's code that someone wrote that's checking these properties of these models.
• 16:37
  Brandon: You can just write that code again in your software.
• 16:43
  Brandon: So, what TLA+ needs is a representation of your state machine with the transitions, how the states change.
• 16:55
  Brandon: You could write your software very explicitly by saying here are these states and here's how these states change. And actually that's a good way to write your code. It's very straightforward, like it's very easy to figure out what's going on, it's easy for your agents to do a good job.
• 17:13
  Brandon: And if you do that, you could write your own temporal logic checker on the model which is your code for whatever you're trying to do.
• 17:28
  Brandon: Maybe you say, hey Brandon, that's like, inconceivable, whatever. No. OK. I actually know of a team that did this before LLMs could write code. OK? So it is possible.
• 17:43
  Brandon: It's very difficult.
• 17:45
  Brandon: It's an impressive engineering feat.
• 17:47
  Brandon: But if humans can do it before agents, then with agents we can do it better.
• 17:52
  Brandon: We can do it faster, I should say.
• 17:53
  Brandon: OK. So there's this team called Viable Systems.
• 17:56
  Brandon: I've worked with them previously. A great team of engineers.
• 18:00
  Brandon: And they were building this complicated distributed system which you can represent as a state machine.
• 18:10
  Brandon: Right? And so what they did is they were able to build a library in Rust.
• 18:17
  Brandon: Basically, what you do is you're just very explicit about your states and your transitions.
• 18:25
  Brandon: You structure them in a way that's very similar to the Elm architecture or the reducer pattern, if you're familiar with that. And by doing this, this library reifies this representation in a way that one, you can execute it and your real application is using the state machine to determine what to do next when it gets a message from this client over here it checks something and then puts the message over there, right? So it actually runs.
• 18:58
  Brandon: Or you can prove temporal logic properties about the state machine. So it is an embedded little kind of TLA-style tool that's part of the application.
• 19:15
  Christine: Whoa, that part I find really interesting.
• 19:18
  Christine: So instead of creating one model to prove and another implementation that might drift away from it, what this team did and what you're now describing is you can make the actual program structure the code in TLA style itself.
• 19:35
  Christine: And then basically that's another way to like remove that gap, that drifting away from the model and the actual code that you're running on.
• 19:42
  Christine: That's really smart.
• 19:43
  Brandon: Yeah. Rather than taking your code and making a simple model of it so this tool can check what it needs to check, just change your code and then take that logic and vibe code it into your application. It's crazy, but you can do it.
• 20:00
  Christine: Can you really like just do it, or does it still feel like quite a feat to really be able to do that right? Like, in which situation should people do this and in which situation is it probably not worth it?
• 20:13
  Brandon: This is more of a crazy idea.
• 20:15
  Brandon: But it's less crazy than it sounds because it's already been done. So it's not too crazy and it's something that I'm actively exploring I guess you could say.
• 20:28
  Brandon: But I won't claim.
• 20:29
  Christine: What kind of project are you exploring it?
• 20:32
  Brandon: So this example that we talked about is a back-end example, like on the server.
• 20:38
  Brandon: But I think there's an opportunity on the front-end to do something similar. I mentioned that the way that this team built the system is they expressed the state machine in a similar way to the Elm architecture to the reducer pattern.
• 20:52
  Brandon: Actually, these are ways to manage state on front-ends. And front-end code, where a user is interacting with an application, these are wild, nasty, complex state machines. You can click on anything, there's network requests going on.
• 21:09
  Brandon: Lots of stuff is happening all the time.
• 21:12
  Brandon: And so there's lots of different states and there's lots of different transitions. And there's lots of properties that you want to prove. Like, the user never is stuck in a loading state forever. That's like a good property to prove.
• 21:25
  Brandon: And the way that people deal with this now, this is actually something that people are actively tweeting about because you can formally verify this. I'm gonna show it to you.
• 21:36
  Christine: So there are more people doing this. That's cool.
• 21:39
  Brandon: Not exactly how I said, but people are taking their front-end logic.
• 21:47
  Brandon: They're formally verifying parts of their front-end. So they're taking these state machines, they're making them really clear in the code.
• 21:57
  Brandon: They're being able to extract them into visualizations like this. This is a tweet from Poteto talking about asking their agent to draw a state chart.
• 22:09
  Brandon: A state chart is just nested state machines and then when you have this state chart, you can really easily translate that into a model that Quint or TLA+ can prove properties about.
• 22:24
  Brandon: But what I'm saying is what if you don't have to make a separate model?
• 22:31
  Brandon: I want a library and I did research, nothing like this seems to exist in TypeScript where the actual state and the state chart, the nested state machines that are driving my application, I make them explicit in the code.
• 22:48
  Brandon: This is like best practice.
• 22:50
  Brandon: People are doing it anyway.
• 22:52
  Brandon: I can derive a visualization which my agents or me can use to understand the thing.
• 22:57
  Brandon: But not just stop there.
• 22:58
  Brandon: I want to also be able to write down temporal logic theorems and prove them directly without having to translate it to a separate model. So. Anyway, this is something that I'm actively working on but not quite ready to show yet.
• 23:17
  Brandon: It's not working yet.
• 23:18
  Christine: That's really cool.
• 23:18
  Christine: It just tells me that there's a direction that people are moving into in the way how they're building new software with coding agents. That's really interesting.
• 23:32
  Brandon: Yeah. Yeah. And I think I'm disappointed that people are just okay with the fact that they have to have a model of their code that lives outside the code. It's so ridiculous to expect that stays in sync.
• 23:53
  Brandon: I don't want to be rude to these amazing people that are popularizing formal verification.
• 23:58
  Brandon: I'm so happy with and excited about Poteto's skill. It's amazing for creating formal verification.
• 24:08
  Brandon: What is it? Create Formal Verification Skill.
• 24:13
  Brandon: It is so easy to use.
• 24:15
  Brandon: I've used it on like five projects.
• 24:17
  Brandon: It takes two seconds.
• 24:17
  Brandon: You all should immediately right now just start using it.
• 24:21
  Brandon: It's amazing. But I guess what I'm saying is like we can push the boundaries and be more creative because our agents are here.
• 24:33
  Christine: Wait. Is there also a way to mess it up?
• 24:37
  Brandon: Yeah, it's crazy, honestly. It's crazy.
• 24:39
  Brandon: Look, the TLA+, Quint, all these formal verification tools, they have like maybe not Bend because it's brand new but even Bend.
• 24:50
  Brandon: They have hundreds of thousands, millions of hours of people like trying to break them and successfully breaking them and then fixing them and so when you use these tools that already exist, you can be fairly confident that there's not bugs in the tools.
• 25:10
  Brandon: This is actually something that is important for formal verification tooling. You wanna make sure that if you have a proof, you don't want there to be a bug in the tool you're using.
• 25:20
  Brandon: It invalidates your proof.
• 25:21
  Christine: But I think Victor Taelin, he put out a bounty for people to break Bend or to find the bugs But no one has found it yet and he's been like very proudly tweeting about it.
• 25:33
  Brandon: Yeah. So Victor worked on Bend for years and then released it and now it's solid. So if you are coding something yourself in a few hours, I guess you can't be certain that there's not bugs in your own thing.
• 25:51
  Christine: But I was just wondering, like, because you were like, I'm so excited, everyone should try this or do this or build this way, but is there also a way to mess it up?
• 26:03
  Christine: Like is there risk to try to always implement formal verification into what you're building with coding agents?
• 26:11
  Brandon: Oh yeah. Don't actually do this.
• 26:13
  Brandon: It's crazy. This is more experimental and exciting.
• 26:16
  Brandon: It's an exciting idea.
• 26:16
  Brandon: I think what you should do is you can today take Poteto's skill and use it.
• 26:23
  Brandon: You can today tell your agents, oh, like, there's some messy state machine here, use Quint and prove that yellow light always comes in between green and red. You should start doing that because those properties that you prove are guardrails for your agents to make sure that they don't mess things up.
• 26:45
  Brandon: And if you do have a mistake, these tools will produce counterexamples which then can steer your agent to immediately fix those issues.
• 26:57
  Brandon: So yeah, you should today start using formal verification in your code. And that's crazy because two years ago almost no one was using formal verification in their software because it's so hard and so time-consuming.
• 27:13
  Brandon: And now it's not.
• 27:16
  Brandon: And then, if you wanna be on the cutting edge, you can start experimenting with implementing these formal verification tools directly into your own software.
• 27:26
  Brandon: But that's on the cutting edge.
• 27:27
  Christine: That's really cool. I think what's really exciting to me is that formal verification is becoming much more accessible and more mainstream for developers building software with coding agents.
• 27:39
  Christine: And I was so excited about the new general-purpose formal verification language, Bend 2, that Victor Taelin launched a few weeks ago, and that's why we did a whole episode on it.
• 27:50
  Christine: But the approach of building the formal verification checker directly in your code, that is a really smart, crazy but also smart approach.
• 28:00
  Christine: I really hope that people listening got some new ideas or thoughts about how to use and implement formal verification.
• 28:06
  Christine: If you have tried experimenting with it or are building it into your existing applications, we'd love to hear what you're building. We also just started a Discord for Superlinear. It's a place to share experiments, discuss emerging practices for building with coding agents and continue the conversation from the episode. Come join us at superlinear.fm/discord. The link is also in the description.
• 28:34
  Christine: And next week we will be back with another emerging practice for building with coding agents and we hope to see you then.
• 28:40
  Christine: Thanks for listening.