Software Verification in the Age of Coding Agents

Software testing is widely understood as essential to building reliable systems, and it’s one of the hardest things to get right. A fundamental issue is that tests are good at confirming the behavior a team expects, but the most damaging failures tend to hide in the edge cases no one thought to check during development. Those blind spots are only growing as AI produces more code that no human has closely reviewed. Antithesis https://antithesis.com/ is a software verification company built around an approach called deterministic simulation testing. The platform runs a customer’s software in a fully controlled environment, exploring thousands of different paths through it at runtime. Crucially, the paths aren’t pre-specified and they’re not merely the expected cases. In this way, it can surface rare, damaging bugs that normal testing would never catch. Carl Sverre https://x.com/carlsverre is on the Red Team at Antithesis and he also leads much of the company’s AI strategy. In this episode, Carl joins Sean Falconer to discuss the Antithesis approach to software verification, why reliability tooling has been chronically underinvested, what makes stateful and distributed systems so hard to test, how deterministic simulation testing works under the hood, and much more. Full Disclosure: This episode is sponsored by Antithesis Sponsorship inquiries: [email protected] mailto:[email protected] The post Software Verification in the Age of Coding Agents https://softwareengineeringdaily.com/podcasts/software-verification-in-the-age-of-coding-agents/ appeared first on Software Engineering Daily https://softwareengineeringdaily.com.

• 0:00Speaker 00

  Software testing is widely understood as essential to building reliable systems, and it's one of the hardest things to get right. A fundamental issue is that tests are good at confirming the behavior a team expects, but the most damaging failures tend to hide in the edge cases no one thought to check during development. Those blind spots are only growing as AI produces more code that no human has closely reviewed. Antithesis is a software verification company built around an approach called deterministic simulation testing. The platform runs a customer software in a fully controlled environment, exploring thousands of different paths through it at runtime. Crucially, the paths aren't pre-specified and they're not merely the expected cases.

• 0:45Speaker 00

  In this way, it can surface rare, damaging bugs that normal testing would never catch. Carl Svera is on the Red Team at Antithesis, and he also leads much of the company's AI strategy. In this episode, Carl joins Sean Falconer to discuss the Antithesis approach to software verification, why reliability tooling has been chronically under-invested, what makes staple and distributed systems so hard to test, how deterministic simulation testing works under the hood, and much more. This episode is hosted by Sean Falconer. Check the show notes for more information on Sean's work and where to find him.

• 1:35Speaker 01

  Carl, welcome to the show.

• 1:36Speaker 02

  Hey, Sean, happy to be here.

• 1:38Speaker 01

  Yeah, absolutely. So, we're gonna get into all kinds of stuff today, but I thought, just to start things off, could you give people, maybe a sense of like what you actually do day to day? It seems like you're embedded with customers, you're tracking the shape of defects as they hit. What is it your day-to-day kind of look like?

• 1:54Speaker 02

  That's a great question. So, I work at Antithesis, and Antithesis is a software verification company, right? And what my job is on the paper is I'm on a team called the Red Team. And this is not to be confused with Red Teams in, like, a lot of times, Red Teams are more like a security team, maybe like an internal, like, Red Team-ing security team. In this case, we named the Red Team after the idea that, what if we hired a bunch of distributed systems experts, people who had spent their whole careers working on building distributed systems and testing them? What if we gave them essentially unlimited access to Antithesis to become experts in how to use Antithesis as a testing technology? And then, basically, use that team to then go and help our customers use the technology

• 2:39Speaker 02

  to its fullest. So I would say my core goal is to become an expert in Antithesis and then help our customers solve and find these very hard bugs in distributed systems. I also am taking a lead in a lot of our AI strategy. So, I sort of bridge the gap between a customer-facing role and more of like a product role.

• 2:59Speaker 01

  Okay, so it sounds like, in a lot of ways, you're like the zero developer in some sense with these tools and doing some customer zero stuff, and then you're also, I mean, how on- on are you with customers? Is this like fully, hey, we're FDE organization and we're going in and making commits? Or what is sort of the overlay capacity that you're doing with customers?

• 3:18Speaker 02

  Yeah, we have a full FDE team who, they're actually in there with the customers and working with the customers on sort of a daily basis and helping them write test harnesses and use Antithesis. We act as like an internal backup team. So, we will go into a customer situation and try to figure out the strategic thing that needs to happen for that customer to become successful, and then offload that to the FDE. So, basically make sure the FDEs have the information they need and the knowledge they need to be able to like make the right call. So, a lot of times, your FDEs just like learn strategies from us and then can apply those strategies to a bunch of different customers. So in many ways, our goal is to find that multiplier effect where if we teach a couple FDEs to fish, then they can go and fish a lot more.

• 4:01Speaker 01

  Yeah, and I guess also in the multiplier effect, some of this is gonna go back into product learnings, I'm assuming, to try to take your, in the team, subject matter expertise back into the product. So this isn't something that you're just one-off fixing or addressing each time?

• 4:14Speaker 02

  That's exactly right. We actually report up to head of product and not in the sales org, and we do that specifically because we want to bring everything really deeply into the product so that every single customer can take advantage of it.

• 4:26Speaker 01

  Yeah, so what do they call this function at Antithesis?

• 4:29Speaker 02

  We just call it the Red Team.

• 4:30Speaker 01

  Oh, yes, sorry, the Red Team, yeah.

• 4:32Speaker 02

  It's such an ambiguous role because we sort of bridge this weird gap between customer-facing and product, so it needed a name that was just sort of abstract to give us a lot of latitude as to what we could help with.

• 4:43Speaker 01

  Yeah, I've seen different versions of this, maybe not exactly this configuration at different companies I've worked for, and I've been part of even some of those teams in certain areas during my time at Google, for example, but I think it's like a highly valuable function that hasn't quite made like a mainstream name for, and everyone's kind of agreed on, but it seems like, in a lot of ways, it's this intersection between product engineering and, I guess, like some level of field engineering at the same time.

• 5:07Speaker 02

  That's a really good point. Like, I think what's most interesting about the Red Team is every single Red Team member has a sort of product area that they are really focused and specialized in. So for me, I'm really focused on our relationship to AI. So I was the person who wrote the Antithesis AI Skills repos. We have like a CLI tool that is designed to be used by agents to interact with the product. So that's sort of my focus. And then, one of my team members, Lawrence, like, he is focused on our, like, property-based testing libraries like Hegel and Bombadil, too. So like, we each sort of have a different product facet that we're really excited about that we spend a little bit of more product time as well.

• 5:47Speaker 01

  Mm-hmm, okay. And it, we'll probably talk a lot about testing and approaches to testing today, but I think, clearly, software testing is something that's always existed. It's kind of gone through, I think, different phases of where a lot of it used to be sort of manual QA engineering, and then we moved into a world where we shifted some of the responsibility, kind of left the engineers writing the code with unit tests, system tests. But I think in a lot of ways, this was echoed by your CEO, Will Wilson, like, it's been treated as like this geniterial work that most engineers hate and few people are focused on. Like, typically, you don't put your very best people on what is your testing strategy, whereas it might be focused on some other area.

• 6:27Speaker 01

  But I guess, like, why do you think that reliability tooling, testing, has kind of been this like chronically under-invested area, given how impactful like a bad bug could be to an actual product experience?

• 6:40Speaker 02

  That's such a good question. So before I was at Antithesis, I was at a company called SingleStore, which used to be called MemSQL. I was there for 10 years. And at SingleStore, we invested a very large amount of engineering effort in testing while we built a database. And not only that, but we were extremely like hyper-shift left culture, so every developer wrote all the tests to test every single thing they wrote. So it was a very like, you know, you write your code, you write your tests, you own the whole thing. And what we discovered was that the more we made testing something that you can do procedurally, so like, the more testing could feel like procedural generation, the more likely engineers would like to use it. And maybe I can phrase that slightly differently.

• 7:24Speaker 02

  So, at SingleStore, we had this internal testing product called Cydeck, so that was our testing cluster. And one of the things about Cydeck was that it allowed you to write procedural tests. You could write tests that essentially were like, you'd write one test, but it would be expanded into many tests by sort of parameterizing the input space. And by doing this, it turned testing into like a little bit of an engineering puzzle. Like, you had to sort of think about, okay, what is the thing I'm trying to test in? What are all the different ways I could test it? And then let me generate, write a test that generates all of those different sort of attack strategies to try to verify this particular piece of code. And by doing that, it actually turned testing into a little bit more of an engineering problem.

• 8:06Speaker 02

  Now, I mention this because I feel like, one of the reasons that engineers maybe don't like tests as much is because the tests tend to just usually test for regression. Like, most tests are written as a, I've implemented feature X, and the test sort of cements feature X into like the acceptance space of being like, this is an acceptable outcome for the software to behave. And, and rarely, it's actually really hard to write tests that test for the unknown, unknown part of the space, right? But that's sort of the most fun test. So I think that the reason why testing isn't something that we think of as being really, like, you don't want to put your best engineers on it, is because we tend to write more tests in the like regression space where we're just having to encode behavior that already

• 8:49Speaker 02

  exists, as opposed to tests in the future space of what are the unknown unknowns.

• 8:54Speaker 01

  In terms of testing in the future space of the unknown unknowns, like, I guess, like, what is hard about that type of testing where you have like all these moving parts, presumably, especially in like a real deployment, you're in a multiple machines concurrent processes, things are probably happening in unpredictable order. Those are not things typically like a regular unit test is going to catch. So what is the hard parts about that? And then why is it that we haven't typically focused on it?

• 9:18Speaker 02

  Yeah, so I think what's hard about that is a couple of different variables. So the first variable is that most code basically either is pure or it's somehow staple. If it's pure code, we tend to reach for unit tests. We tend to basically think about just verifying some number of inputs lead to some number of accepted outputs. And the sort of like space of how you test that is very straightforward. But most actual interesting software and like, once you get to like a higher order software, you know, it just should be the system, almost the entire piece of software is highly staple. It's highly dependent on the history of inputs up to this point across the entire software and also all the future inputs is like this huge, huge space.

• 9:58Speaker 02

  And I think that when you're wrestling with trying to test that, just by testing it, you basically have to take into account the fact that a lot of behavior stems from faults. Essentially with tests, you want to say like, what if A happens and then B happens and then C happens, where B and C are like bad things, like faults usually. Something went wrong, some input was incorrect. And in order to test such a thing, people tend to reach for like integration tests, right? So they sort of encode a particular series or a particular timeline of events. And as humans, it's very easy to reason about an integration test because I can think, okay, I just want to force the software to like do A, do B, do C. But let's say you wanted to write an integration test to test something you didn't know existed.

• 10:42Speaker 02

  Like, it's not obvious how to do that. The only way you could maybe reasonably do that is write a test which tests all possible inputs at A and then test all possible inputs at B for all possible inputs at A and then so on. So you end up with this sort of tree shaped thing.

• 10:59Speaker 01

  Yeah, like a combinatorial problem there.

• 11:01Speaker 02

  Exactly. You sort of want to like test all the things that can occur after every sort of step of this like big state machine. And state machine testing is very straightforward if it's pure, like if the state machine doesn't have any kind of like side effects that are non deterministic. But most modern software, especially distributed systems, they have a huge surface of the state space is non deterministic. And because you can't sort of simulate those non determinisms deterministically, it becomes this like very difficult problem. And so people, in my experience at SingleStore, so pre-Antithesis, you basically ended up with integration tests which tested series of events that we knew existed. And those ended up being mostly regression tests, but maybe every once in a while, we would inject some faults on the way sort of thing.

• 11:45Speaker 02

  So we could try to verify that some error was like handled correctly.

• 11:49Speaker 01

  Right.

• 11:49Speaker 02

  Or they sort of showed up as like stress tests where instead of trying to like test a particular timeline, we just tested huge numbers of random timelines. And then we were basically saying like, in aggregate, all of these timelines have a behavior that we want or property that we want, like they all converge or they all recover sort of thing. So that was basically a long way of saying, I think it's just way harder to test for unknown unknowns. And so I think most people just prefer to stick with the sort of simpler case of like, okay, let's make sure that the most obvious failure paths are sort of handled. But the best kind of testing you can do is the one that can reach the space of like sort of future possibility.

• 12:30Speaker 01

  Right. Was Netflix introduction of chaos engineering in some sense like an attempt to try to deal with this unknown unknown?

• 12:38Speaker 02

  Yes, absolutely. So chaos engineering and Netflix, what is another one? I feel like Meta had a similar thing that they sort of talked about, and I know Google does this as well, like Google does a lot of chaos engineering for like Google Cloud, for example.

• 12:52Speaker 01

  Yeah, I mean, I think that Netflix was the one that popularized it. And then I'm sure the similar, the like hyperscalers probably had similar functions, but maybe didn't have such a memorable name to it. And then other people sort of copied from there, but.

• 13:06Speaker 02

  Yeah, I mean, Netflix essentially is doing stress testing at scale. Like they're essentially scaling up stress testing to production, first of all, which is amazing. And then they're doing it with the goal of basically verifying that if your system is constantly experiencing sort of bad weather, you're going to be having to make it more reliable at a much faster pace than if you only experience bad weather very rarely. And so they changed the culture to be, we have to handle this sort of bad weather all the time. And that's a very similar mental model to just like, what if you make your testing system basically a continuous bad weather stress test? And then you require that your system can survive under that weather at all times.

• 13:48Speaker 01

  Yeah, we had an unintentional version of this years ago, like my first ever engineering job is like 20 years ago in college. But we had basically our dev server was so bad and so slow that if we could make things work there in some reasonable way, we knew it would work on production because the production server was like, had so much more capacity and was such better. So it's like, if this is fast in this environment, it's going to be really fast when it actually hits production and can survive a whole host of conditions.

• 14:15Speaker 02

  Yeah, like I actually, I've talked about this a lot with Antithesis customers is like, Antithesis customers, at some point, they need to bring their system into Antithesis. And sometimes that means that you might have to like mock a service. Like, for example, let's say you depend on Stripe. Well, we can't put Stripe in Antithesis, so we need to provide some kind of like Stripe like thing, like a mock. And a question that comes up often is like, well, what if the fidelity of the mock isn't as equivalent to Stripe? Isn't that going to be an invalid test? And the way I generally frame this is you just need to make sure that the mock is worse than what can happen. As long as it's sort of a superset of behaviors where the behaviors are all worse than what you're going to get for production, you sort of can use that as a way of like verifying some software, right?

• 15:00Speaker 02

  So it's easier sometimes to make a worse mock that has a wider range of potential failure scenarios than like a perfect fidelity mock. And so that's sort of one way to balance that equation.

• 15:11Speaker 01

  What about in now where increasingly we're building software systems that also largely dependent on non deterministic processes where they're going to hit some L M to generate an output? And essentially, we can eval that and have a, basically have a probabilistic measurement of how often it's going to return the result in a form that matches our expectation. But how's that change, I guess, like the way that we think about testing?

• 15:37Speaker 02

  I don't think it changes it. I think that it opens up the state space that you need to test quite a bit. So like, if you think about, let's say that as part of your application's business logic, it's essentially asking the L M what to do next at some point in some multi-step process. Now, the potential like next steps you might be able to go from that point may have just exploded in possibility. Like if you're, you know, in extreme case, you're basically letting the L M agent run in some kind of like Linux sandbox and it's just able to essentially do anything it wants on the machine. So now what you have to do is you basically have to verify that all of your downstream effect, all of your software that reacts to that new input can react to a much wider

• 16:21Speaker 02

  range of new inputs. And so the need for procedural testing or in Antithesis parlance, like deterministic simulation testing, where you're actually testing like all of the possible next steps is even more important because you need to be able to handle sort of a much wider range of inputs.

• 16:38Speaker 01

  Yeah, can you go in a little bit more detail about the deterministic simulation testing? Like, how do you explain that, I guess, to like clients, like what exactly was happening there?

• 16:47Speaker 02

  Yeah, so the fundamental idea of DST is a couple of things. The first thing is that you need to take your code, your system that you're testing, and you need to basically be able to make it deterministic. And there's a number of ways to do that. Antithesis provides a solution that does this automatically for like Linux software, essentially. So you could just deploy your software as is to our platform. We, you can think of this as like a deployment target, like an EC2 server. So you deploy your software to us and as long as the software is entirely running inside of that same EC2 server, so like, let's say you split up your software into Docker containers or whatnot, the whole system as a whole is deterministic. So it will only suffer non determinism that we inject. So we control it. Your software still sees non determinism, so it sees randomness, it sees time, it sees

• 17:32Speaker 02

  ordering of events that may differ, stuff like that. But we can reproduce the exact non determinism that we inject. So that's one way you can do it is use the Antithesis model. The other way you can do it, of course, is by essentially rewriting your software where all possible non determinism is injected. So that essentially means you need to control the environment. So any reads you have to a non deterministic source like time, randomness, and so on, is controllable. And then you also need to be able to control scheduling. So you need to make sure that like the software ordering of events occur in a controlled way. So that is the first sort of ingredient to deterministic simulation testing is a deterministic way to run your software.

• 18:12Speaker 01

  And is the user responsible for some of that? Like you mentioned, for example, like time. So if I have something that maybe generates like a random number in my code, do I have to, when I'm using the software to set up these tests, do I have to set something specific in my software, like using, I don't know, library or whatever, to kind of mock up a deterministic response rather than a random response in that case? Or is that something that is offloaded to the platform?

• 18:38Speaker 02

  On Antithesis, it's offloaded to the platform. So we control system randomness. So if you read any random number from the system, like, for example, you read like devu random on Linux or you do anything like that, you're always going to get something that we completely control. Now, a lot A lot of software will read W random and time and then they'll like mix the bits and then they'll initialize like a PRNG, for example, to be able to have faster random number generation, which most runtimes will do. When you're running an antithesis, we actually recommend that you don't do this. So if you do use a PRNG in your software, you actually replace the PRNG with direct reads to system randomness. And there's a reason for that, and that reason is the second ingredient of DST.

• 19:20Speaker 02

  So the first ingredient is determinism, so the ability to be deterministic, so the same series of events occur. The second ingredient of DST is simulation. And the reason why we want to be able to control randomness at every moment, so you not having a PRNG that's preceded, that has this a particular series of events that's going to happen, but instead you're always asking us for randomness, is that in DST, we want to be able to branch the simulation. So if you think about your software as being like a series of inputs that lead to some change to the software, some state change. Effectively, all of this starts at like the root moment. So your software has just booted, it's fresh, it's starting from like a completely known state.

• 20:02Speaker 02

  And then something is happening to the software, it's provided inputs, it's proceeding linearly through history. And since it's deterministic, we can go back to any point in that linear history and we can branch. And we can say, you know what, what we want to do is at this moment, we want to change randomness, for example. And then we're going to create a new timeline, starting at that moment, that's going to proceed in its own sort of butterfly effect history. And so because your software is reading from like, for example, our random source, like our system randomness, every single time it's making a decision, we can branch at a much more fine-grained point. Like this is a little bit of in the weeds detail, but if you instead use a PRNG,

• 20:43Speaker 02

  then even if we branch the timeline, you're still going to see like the same series of random numbers in that new branch, unless we have a way of like reseating the PRNG.

• 20:52Speaker 01

  Mm hmm.

• 20:54Speaker 02

  That's a little bit of an aside on like randomness. But the point, going back to like your original question of like, what is DST, right? We have determinism and simulation. So determinism is your software sees the same series of events every time and we can replay, basically. Then simulation is the ability to branch the state space or branch that timeline into a new timeline and explore different orders of events. And so the really powerful thing about DST is once you do this, you can basically say, like, a good example is, let's say you have a distributed system with like three nodes. What you can do is you can basically say, all right, like, we're going to wait until one of the nodes crashes for some reason. So great, in most distributed systems like Raft, for example, it should be able to handle like one node dying, right? So one node crashes.

• 21:39Speaker 02

  And then what we want to do is we want to basically branch a whole bunch of timelines after that node dies and then experiment with different series of events that happen. So what happens if that node recovers during a new leadership election, like right in the middle of leadership election? Does something occur that is bad? And so by being able to branch the simulation and trying different things out in different orders from any point, we have the ability to sort of breadth first search the state space of your software. And that is the sort of ingredients of what DST is.

• 22:10Speaker 01

  How does it figure that out? Like, how's it deciding where to look and like what tests to run and do that branching? Is it actually inspecting like the bytes of the code that I've uploaded to execute?

• 22:20Speaker 02

  So almost. So there's another sort of adjacent area of research, which is called fuzzing. And you've probably heard of fuzzing, and if you haven't heard of fuzzing, I mean, fuzzing basically is, let's say you're writing like a JPEG encoder or an image encoder, and you want to basically verify that the encoder can take any amount of input bytes, so some arbitrary noise, and it always can encode like a valid JPEG or it can error in a clean way. It doesn't ever crash, for example. And so in fuzzers, in that world of research, one of the strategies that they use is called coverage guided fuzzing. So coverage guided fuzzing is basically, we're going to monitor all of the branches that the code under test is taking.

• 23:00Speaker 02

  So we have this fuzzer code, like lib JPEG, for example, and it has a bunch of internal if conditions that go down different branches. And we're going to monitor which branches are triggered. And as we run random noise through this, we're going to start building a map of this noise triggered this series of branches. And then we change the noise and we could see, oh, a different series of branches were taken. And by doing this over and over and over in a tight loop, we gain some knowledge about the system without having to.

• 23:25Speaker 01

  Right, yeah, see, basically you're treating the system as a black box, but you have inputs coming in and you can send the same input, generate the same output.

• 23:34Speaker 02

  Exactly.

• 23:34Speaker 01

  And then vary the inputs to vary the output. It's actually kind of similar to a conversation I had last year on reverse engineering kernels, essentially, where they're doing the same thing to try to figure out what is the, or sorry, reverse engineering chips, where Apple doesn't give you the blueprint of how the chips work, but you can, and basically through inputs, you can simulate what the hardware is going to generate, you can watch what happens. And then eventually you can build a simulator that actually mimics what the hardware does, but you don't actually know specifically the internals of it, you just know what the inputs and the outputs are.

• 24:08Speaker 02

  Yeah, it's exactly like that. So we basically apply the same strategies from fuzzing research to the DST. So your software is running inside antithesis, completely deterministic, and we are monitoring coverage branches as one of our inputs. We have a bunch of other inputs that we monitor about the system that helps us understand whether or not we're seeing sort of new behaviors or pre-existing behaviors. Effectively, we're trying to detect if we're going in like a cycle. And then we can essentially branch to try to break out of that cycle and find some like different interesting area of code to exercise. And there's a couple of really cool, like sort of emergent properties of this that is neat. So like one emergent property is that we're really good at finding thread, like a bug caused by like a particular order of threads

• 24:52Speaker 02

  and how they're like taking locks and interacting with shared memory and stuff like this. Because what we'll do is we'll notice that we're seeing different branch paths really quickly in that area. And we'll kick off like a whole bunch of autonomous sort of searchers that are going to all start from that like beginning of that sort of highly contentious section of code. This was very useful recently. I don't know if you heard about the SQLite wall reset bug that happened earlier this year?

• 25:16Speaker 01

  I mean, it vaguely rings a bell, but that maybe gives us some background on that, but.

• 25:20Speaker 02

  So one of my other passions is SQLite. I love SQLite, I like to track it. And earlier this year, there was like a reported bug on SQLite and a fixed bug, which existed in the SQLite project for 10 years. So it's been around since they basically wrote the original write ahead log code in SQLite. And the bug is like, you know, your standard sort of bug that's really hard to find. It was like, you know, one thread read a shared memory, essentially some, some data out of shared memory. Then the thread like slept and then another thread changed the data, then it woke up and then, but it didn't do a correct like revalid validation after it woke up. So your standard sort of concurrency bug. But the thing is, is that the window on this was so, so, so tight that I believe only like maybe one SQLite big customer, it happened to be TailScale,

• 26:03Speaker 02

  but one big customer ever like actually hit this bug. Anyways, it took a long time to narrow, like nail down what the bug was. TailScale did a lot of research earlier this year and they published their findings and it got fixed. Great, SQLite has this sort of resolve. When I saw this bug, I was super excited because I was like, oh my gosh, like a bug that is like the perfect shape of a thing that antithesis should be able to find like quickly, like this should be very easy for us to find. So sure enough, I took the like latest version of SQLite pre-patch, so like the last version that has the bug in it. I put it into antithesis with a very simple workload. The workload just ran inserts and wall checkpoints in a loop, basically. So it wasn't trying to, you know, specifically hit this bug, but it was exercising the relevant code.

• 26:47Speaker 02

  And I just ran it in a loop and 15 minutes later, the fuzzer found the exact bug, like narrowed, narrowed it down to the exact order of, of operations that had to occur. And it sort of proved out this point that because of the way in which antithesis can sort of autonomously find interesting behavior spaces and then exhaustively test them, these kinds of bugs fall out of antithesis very easily.

• 27:09Speaker 01

  Did you, in this situation, since you already knew the bug was there, was there anything that you're giving in terms of like an unfair advantage, since you already know that the bug is there to kind of point it in the right direction? Or is this something that you didn't have to do any kind of configuration, you just let it go and it discovers it?

• 27:24Speaker 02

  The actual workload that was created, like I did know the bug existed. So obviously I focused the workload on exercising that area of the code. However, after I verified the bug and I was able to find it very quickly, I then wrote a generic workload. So a workload that runs all SQLite operations with even probability. So it runs selects, inserts, it uses other things than the write ahead logs. It uses like the default journal based like transactional system. So basically like I wrote like a generic workload that just sort of exercised the entire system and that still found the bug in like 15 minutes. So the nice thing about Antithesis is that like its ability to find these spaces that blow up the behavior space. So like when it discovers, I'm seeing like

• 28:06Speaker 02

  a bunch of new behaviors happening, it will automatically focus on that area and then spend a bunch of fuzzing energy to until the rate at which we're seeing new behaviors starts slowing down. And then we'll go and focus on another area.

• 28:19Speaker 01

  What is like as the user of this, like what are you giving me? Like, how do I, since this is a black box, like, how do you help point me in the right direction other than it was this input that presumably generated like an output that was unexpected?

• 28:34Speaker 02

  Yeah. So our platform offers a couple of sort of like tools to help you understand what's happening, like debugging essentially and observability. So from an observability perspective, we give you basically a view of all of the logs in the system, except the logs are strictly serialized with the exact order of operations. And so unlike traditional distributed systems where you have to guess, you know, where these like which of these two events occurred in what order in Antithesis, because we control serialization of all execution, we can guarantee that like the order you see the events in the log is exactly the order of events in the simulation. So you get this very high resolution log, basically. So that's one output. The second output is we have this concept called properties. And so when you put a system in Antithesis, you

• 29:19Speaker 02

  also provide us a whole bunch of properties. So the specific property that I used for testing SQLite was a very simple property. I just simply told Antithesis to run Pragma integrity check, which is the built in, is my database corrupt check that is just built into SQLite. I just basically said, run that check at random points in the simulation, just like pick any point and just see if it's corrupt. And so Antithesis will just do that automatically. And whenever it discovers a corruption, it will then narrow down fuzzing energy around like that region, which is another way that we, another signal that we have that we found something interesting, basically. Those two things get you pretty far because it gives you the ability to look at the system in any

• 30:01Speaker 02

  particular order that, you know, discovers something and then also teaches Antithesis when you discover something potentially bad about your system. The next two features are what separates Antithesis from just being an observability platform. So the first one is multiverse debugging. So we basically give you the ability to SSH into the system at any time in the simulation. So let's say that you discover this like bug in SQLite, you see that the integrity check happened at like the, at time like 30 seconds. Well, you know that something corrupted the database in the previous 30 seconds, but you don't know exactly where it corrupted that database. So one thing you could do is you can actually just SSH into SQLite into the actual like cluster. And then you could run SQLite operations and you could go back in time and you could

• 30:43Speaker 02

  basically binary search for when that corruption actually occurred. That's sort of one thing. And then once you find it, you can, you know, GDB in and stuff like that. The fourth tool that we have is called causality analysis, which is where we do that for you autonomously. So basically, if you find a bug and you're like, I want to figure out exactly when this bug was introduced into the system, we'll basically just binary search for you. So we'll go back in time, we'll perturb the environment and we'll roll out and we'll see what, where the bug was sort of locked into the simulation. So yeah, those are some of the ways that we help.

• 31:14Speaker 01

  So we had Joe Hallerston from AWS a little while ago, talking about the project Hydro. Are you familiar with Hydro?

• 31:21Speaker 02

  I don't think I am.

• 31:23Speaker 01

  So essentially what they're doing is they're trying to catch distributed bugs at compile time through the type system. So essentially the theory is that certain classes of bugs can't be written in the first place because essentially the compiler stops you from running it. And so a lot of it's kind of like trying to prove this stuff upfront. Maybe you could think of it as like formal methods for testing. Whereas, you know, some of the stuff that you're talking about is really about catching these things at runtime, you know, breaking them through this simulation. I guess like, what's your take on that? Are these like two approaches intention or are they sort of complementary?

• 31:57Speaker 02

  Yeah, this is a really good question. So I'm not deeply familiar with Hydro. However, from what you just described, does Hydro try to make these proofs on the actual implementation of the software? Or is it making these proofs on sort of a formal, like abstract model of your software?

• 32:14Speaker 01

  So I believe that from what I remember, it's actually, it's a compile time check. So it's actually running, you're writing your code and then during compilation, it can determine whether the code that you wrote is going to break something that would break in a distributed system. So prevents you from writing it in the first place. So it's not something like a model on top of the software. It's actually like basically baked into the software. You could think of it the same way that you might do like a type system check on, you're suddenly stuffing it into a string or vice versa.

• 32:45Speaker 02

  Yeah, that makes sense. I don't think these approaches are necessarily intention. So let me explain why. So first of all, Hydro is like a very advanced form of other kinds of like static verification. So for example, like if you're using Rust, you're obviously already taking advantage of the type system to ideally eliminate a whole bunch of bugs. If you write very pure Rust and very safe Rust, you can actually just eliminate whole classes of like memory style bugs, right? So you should be doing this, like the more lines of defense between you and your buggy software you have, I think the better. So like, that makes sense. The thing that I'll have to like research Hydro and understand more deeply as to like whether or not has any kind of compromises.

• 33:24Speaker 02

  But sometimes these types of systems force you to write your code in a very particular way. They tend to be integrated into your runtime, essentially, maybe just at compile time, but it's basically integrated in sort of the way in which you structure your code. And so just like building your own DST is really, really valuable that you should do it. Hydro may also fall into that same category of being perhaps I suited better for like greenfield projects, projects that start from zero, where you can write your code in a very particular way to take advantage of these properties. The downside, of course, is that like that particular way, first of all, it may not be that intuitive how to express like your problem in that way. And of course,

• 34:06Speaker 02

  you're sort of stuck with potentially having to have some compromises in like your implementation to be able to make those proofs. I don't know about Hydro, so I can't say maybe they've made something even better, but the traditional solution to this or like other traditional sort of ways of doing this that I've seen, like rolling your own DST involves a very high tax on the software, like on the software development effort. So that's sort of one aspect of it. It would be interesting to know what classes of things can be checked with something like Hydro versus what are still unknown unknowns in the system. So I still think that having something like Antithesis on top is good, but we can talk a little bit more about formal methods if you want, because formal methods has a different set of trade offs. With formal methods, you end up

• 34:49Speaker 02

  modeling, you create like a sort of a different version of your same system where it's an environment where you can actually express these kinds of like formal methods. You basically end up defining an abstract model of your system, which you can then prove has some kind of correctness and variance.

• 35:04Speaker 01

  There's a lot of different ways of testing software. We've mentioned a few of them around like unit tests, system tests. There's compilation as a test. Like, I guess the approach that you're taking, which is like, you know, simulation testing kind of fit within this stack. As a software vendor, like how should I be thinking about, I'm going to build out my testing stack? Where do all these pieces kind of fit together? And what problems do they specifically solve that are maybe complementary and don't overlap with each other?

• 35:32Speaker 02

  So I think where the Antithesis style testing, so deterministic simulation testing fits into like to sort of overall testing picture is a little bit closer to like the integration and sort of stress testing world. So you should still be obviously using unit tests to verify small independent pieces of code. It's the fastest way to be able to verify those types of code. And you should still be using as many types of testing as you basically can spend money on just because you're going to have an overall better code quality. And obviously in the age of AI, I think the more testing, the better, basically, like the more constrained you can make the model, the more likely it's going to give you something that is good quality. So that's sort of the high level idea. The lower level idea is like Antithesis really, really serves you

• 36:15Speaker 02

  well when you use it to test the unknown unknown space. So with a single Antithesis test, you can basically write that test once and you can test almost the entire state space of your software. You can theoretically reach everything that can possibly happen, every bad order of events that can happen. And this is particularly good for integration level tests where you're testing like multiple components at the same time, like a distributed system, for example, or even just like a crud app where you have a database, you have some like, you know, horizontally scaled web servers, you have a cache and you have a client. Even that distributed system is complex enough that you can very easily have weird situations where like, you know, a client sends a write to one node, it for some reason gets cached, it doesn't flush to the database right

• 36:58Speaker 02

  away, sends a read at another node, and then it fails. Testing these types of systems in integration tests, I find you just, it's just really hard to express in an integration test, all the different sort of flavors of failure that can occur and order of events. And so I find simulation testing just like a more natural way to do it.

• 37:15Speaker 01

  We make a big deal talking about distributed systems as this kind of thing that you're only doing at scale. But in reality, every system is basically distributed now, like even at Client and server. We've had those systems for a very long time that far predate even cloud and Kubernetes and the types of technologies we would be using today at scale. So these bugs can absolutely occur even in a very simple, you know, three tier architecture or something like that.

• 37:40Speaker 02

  Even inside a single process, I mean, like if you have multiple threads interacting with shared memory or message passing, you have a distributed system and you need to be able to think deeply about the order of events that can occur within that system to be able to know that it is correct. I've been doing a lot of work with AI recently where I've been teaching AI how to write workloads that run in Antithesis for arbitrary pieces of software. And by virtue of doing this, I'm also learning about how to use Antithesis more as like a tool to give the AI the superpower to ask questions about the future. So like, if you think about AI writing like a normal test, like let's say you're doing test-driven development.

• 38:21Speaker 02

  In test-driven development, you're going to write like an integration test that fails because it's dependent on some kind of feature or change that you haven't yet written, right? And then you're going to like have the AI iterate to make sure that that works. I actually think this maybe is not the right path for AI. AI tend to like hyper-focus on the bully you give them. So if you give them a

• 38:41Speaker 01

  You're basically overfitting to the test.

• 38:43Speaker 02

  Exactly. You end up really fitting tightly. Now with Antithesis, if you do the exact same thing, instead of TDD, you do ADD, I guess. And with Antithesis-driven development, I suppose, you end up with this interesting thing where you can't possibly overfit because Antithesis is designed to find counterexamples to whatever you give it. So if you, you know, make the code behave to pass the test, there's nothing really to overfit to. You're trying to solve like very general purpose properties, like the database never goes corrupt. And it's much harder to like overfit to those properties. And so you just end up basically being forced to just implement the code in the most like generic and correct way possible.

• 39:21Speaker 01

  What is the cost to the development lifecycle in terms of like how long it takes to run one of these simulation tests? I mean, the advantage of a unit test, for example, or even a test as compilation is very fast. So I can get, if I'm doing AI coding, I get an immediate almost feedback loop to my AI system to know that, okay, well, we, this code doesn't work because it doesn't compile, or this code doesn't work because it doesn't pass the unit test.

• 39:47Speaker 02

  Yes. The question is basically like, you know, how tight of an iteration loop can we create? And like, what's the sort of cost in development? So there's a couple of different ways to answer that question. So the first question, the first way to answer is like, let's say you already have a workload. So my SQLite example is a good one. I already have a workload that tests sort of the full state space and surface area of SQLite. So I can use that exact same workload on a new feature and I can continue to verify that all the properties hold. So the database never goes corrupt and all this stuff. However, the longer you run that workload, the more confidence you get in the output, right? Because Antithesis is effectively doing breadth-first search over the state space. So if you run it for 15 minutes, you get some amount of coverage. If you run it for an hour, you get more coverage and so on. And it probably plateaus at some point, right? So if you ran it for like 12 hours,

• 40:31Speaker 02

  maybe you're getting very little value after a certain number of hours, like eight hours or something. So the way that we tend to like wire this up is almost like this continuous exponential process. So on an individual PR, you may want to just run Antithesis for like 15 minutes. In 15 minutes, we run at a default parallelism of 48. And we also do a bunch of tricks inside of the systems to sort of fast-forward time. So for example, if you sleep in the code, we'll fast-forward to that sleep point. So we don't have to actually spend real time on those types of things. And so because of that, we often see at least a 48x speedup, sometimes much, much higher, depending on the shape of the code. If the code is like a workflow engine or a job system, the speedup could be like a thousand X, right?

• 41:15Speaker 02

  And so basically in 15 minutes, you could easily test like hours and hours and hours of simulation time of your software. So because of that, 15-minute runs give you like actually pretty high confidence that you haven't broken something obvious. But then what you want to do is you want to basically run like exponentially longer runs on exponentially larger chunks of untested code. And so we tend to have this like almost a propagation wave from PR where you're running relatively short tests, but you get feedback quickly to like your main integration branch, which has a propagation wave of confidence. So yesterday, the code you shipped has been run overnight on a 12-hour stress test, which simulated, you know, three months' worth of time in Antithesis. At which point you're very confident that there isn't some kind of like big catastrophic bug.

• 42:00Speaker 02

  But maybe like the PR you landed three hours ago has only had a one-hour test on it. So you have like a lower amount of confidence. So those are some of the ways that we're exploring making this like iteration faster. We also have recently started exploring giving agents the ability to like run commands and ask questions about in-progress runs. So an agent can basically kick off a run in Antithesis and then immediately subscribe to a particular failing property that they're interested in. And if that failing property occurs, like let's say it happens within the first five minutes of the run, the agent can immediately get that notification and then start debugging without having to wait for the run to complete.

• 42:38Speaker 01

  And I would think too, you kind of touched on this earlier where testing has become even more critical when we're generating more and more code. And it's not necessarily because by default, or there's some truism that every line of code that AI generates is sub-quality to a person's ability to generate it. But it's just that, you know, if the person generating the code is only maybe looking at it a little bit or not looking at it, they don't have the same connection to that code and might not fully understand it at the same length. So then a lot of it gets shifted to, like the responsibility gets shifted to sort of testing and verification. I think that would also shift what is maybe the amount of effort and time that we're putting into actually testing and verification.

• 43:19Speaker 01

  Because there's such a risk now associated with pumping out code that maybe hasn't been fully vetted because like a person never looked at it or barely looked at it. So it kind of changes the equation, I guess, is what I'm trying to say in terms of where we're willing to spend time and compute cycles on than maybe what we were willing to spend time and compute cycles on, you know, just a few years ago.

• 43:41Speaker 02

  I totally agree with that. I think that as we sort of see the like time it takes code, effectively as the coding time decreases, we basically should be rebalancing that effort into verification and specification. I see the role of engineering in the future being one of being very, very precise in specification. So being able to prescribe exactly what you want in a higher precision than we currently do. I don't think markdown documents necessarily cut it for the level of precision that we need. And then on the other side, you want verification to tie back to specification. You want verification to not be hyper-focused on like individual paths through your software. You want your verification to be a net of saying, for all possible paths, do they all match my specification, right?

• 44:26Speaker 02

  And the Antithesis sort of story to this is that your specification should derive properties and invariance of the code that you want. You should encode those into the workload that is running in Antithesis, which then acts as a net that says for all possible paths through your simulation, we always reach a valid property outcome. We never see a counterexample. And by doing this, as we go back to like the sort of TDD thing, like your agent ends up focusing just on building the code that can like exist within that net in a safe way.

• 44:57Speaker 01

  Carl, as we start to get close on time here, is there anything else you'd like to share?

• 45:02Speaker 02

  Something that just I was thinking about recently that I'd like to like leave your audience with, related to that last point of basically with modern coding, with AI coding, you want to build this like net and you want to build really good specification. In some ways, like I've been thinking about the reality of coding sort of becoming almost like diffusion, like image diffusion, if you've seen like all the AI-generated images. At which point, we may get to an extreme case of this, like in some potential future, the ability for AI to generate very large volumes of code may be so much that we could actually completely change software engineering from an iterative process to almost like a diffusion process where you change the specification and you re-diffuse the entire codebase.

• 45:47Speaker 02

  And as long as it matches the specification and the, you know, passes this sort of huge, huge net of potential state space, you basically just release that completely net new codebase as the new version of code. And I'm very interested to see how software engineering as a practice evolves as we get closer to that point. And I think Antithesis is a good sort of solution to the verification side of that problem.

• 46:11Speaker 01

  Yeah, absolutely. I mean, this was super fascinating. Like I feel like we're just, you know, barely scratching the surface here. And I totally agree. Like I think that so much has changed in software development, even in a six-month period. I don't think we're at steady state now. I think things are going to continue to massively change over the next couple of years. I don't know that anybody knows for sure, you know, where we're going to end up. But regardless of where we end up, I think it's going to be sort of exciting times, highs and lows to maybe get there.

• 46:37Speaker 02

  Yeah, totally agree. Well, I had a really good time on this chat. Thank you so much for having me. I'm excited to listen to this when it goes live.

• 46:43Speaker 01

  Carl, thanks so much for being here and cheers.

• 46:45Speaker 02

  Cheers. Thanks, Sean.