コーディングエージェント時代のソフトウェア検証

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. 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 underinvested, what makes stateful 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. Carl, welcome to the show. Hey, Sean. Happy to be here. Yeah, absolutely. So we're going to get into all kinds of stuff today, but I thought just to start things off, could you give people maybe a sense of 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? 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. And like a lot of times Red Teams are like more like a security team, maybe like an internal like Red Teaming 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 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. 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 long on are you with customers? Is this like fully, hey, we're an FDE organization and we're going in and making commits? Or what is sort of the overlay capacity that you're doing with customers? 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 in to 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 FDE has the information they need and the knowledge they need to be able to make the right call. So a lot of times our FDEs just 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. Yeah, and I guess also in the multiplier effect, some of this is going to go back into product warnings, I'm assuming, to try to take your and the team's subject matter expertise

back into the product. So this isn't something that you're just one-off fixing or addressing each time. 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. Yeah. So what do they call this function in businesses? We just call it the red team. Oh, yes. Sorry, the red team. Yeah. 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. 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 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. 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 Antiphysic AI skills repos. We have like a CLI tool that is designed to be used by agents interacting for 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. Okay. And we'll probably talk a lot about testing and approaches to testing today. But I think like clearly software testing, 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 Wilton.

It's been treated as this genital work that most engineers hate and few people are focused on. Typically, you don't put your very best people on what is your testing strategy, whereas it might be focused on some other area. But I guess, like, why do you think that reliability tooling, testing has kind of been this like chronically underinvested area, given how impactful like a bad bug could be to an actual product experience? That's such a good question. So before I was at Antithesis, I was at a company called Single Store, which used to be called MemSQL. I was there for 10 years. And at Single Store, 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. So at Singlestore, we had this internal testing product called SciDuck. So that was our testing cluster. And one of the things about SciDuck 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? And like, what are all the different ways I could test it? And then let me 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. 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 in 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 exists as opposed to tests in the future space of what are the unknown unknowns. In terms of testing in the future space of the unknown unknowns, I guess what is hard about that type of testing where you have all these moving parts, presumably, especially in a redeployment, you're going to have multiple machines, concurrent processes, things are probably happening in unpredictable order. Those are not things typically 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? 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 stateful.

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 stateful. It's highly dependent on the history of inputs up to this point across the entire software and also all the future inputs. It's like this huge, huge space. 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. 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 tests 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. Yeah, like a combinatorial problem there. 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, we 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 So we could try to verify that some error was like handled correctly Right 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 an 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. Right. Was Netflix introduction of

chaos engineering in some sense, like an attempt to try to deal with this unknown. Yes, absolutely. So chaos engineering and Netflix. What is the other 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. Yeah. I mean, I think that Netflix was the one that popularized it. And then I'm sure the similar The hyperscalers probably had similar functions, but maybe it didn't have such a memorable name to it. And then other people sort of copied from there. 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 change 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. Yeah, we had an unintentional version of this years ago, like my first ever engineering job, this was 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 was like, if this is fast in this environment, it's going to be really fast when it actually hits production and it can survive a whole host of conditions. Yeah. Like I actually, I've talked about this a lot with Antiphas 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. 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. What about now where increasingly we're building software systems that are also largely dependent on non-determinant processes where they're going to hit some LLM to generate an output? And essentially, we can eval that and basically have a probabilistic measurement of how often it's going to return the result in a form that matches our expectation. But how does that change, I guess, the way that we think about testing?

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 LLM 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, an extreme case, you're basically letting the LLM agent run in some kind of 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 range of new inputs. And so the need for procedural testing or in antithesis parlance, like deterministic simulation testing, where you're actually testing 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.

Yeah, can you go into a little bit more detail about the deterministic simulation testing? How do you explain that, I guess, to clients? What exactly is happening there? 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 Linux software, essentially. So you could just deploy your software as is to our platform. 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 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 seems 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 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. 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 it is, 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? 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 dev urandom on Linux or you do anything like that, you're always going to get something that we completely control. Now, 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 pure NG, 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 pure NG in your software, you actually replace the pure NG with direct reads to system randomness. And there's a reason for that. And that reason is the second ingredient of DST. 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 PRND that's preceded, that has 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. 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, 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 reseeding the PRNG. 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 DSD, 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 RAP, for example, it should be able to handle like one node dying, right? So one node crashes. 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. How does it figure that out? How's it deciding where to look and what tests to run and do that branching? Is it actually inspecting the bytes of the code that I've uploaded to execute? 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. So we have this fuzzer code, like libJPEG, 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 can 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 Right Yeah See basically you treating the system as a black box but you have inputs coming in and you can send the same input generate the same output Exactly And then vary the inputs to vary the output It actually kind of similar to a conversation I had last year on reverse engineering kernels essentially where they doing the same thing to try to figure out what is the or sorry reverse engineering chips where Apple doesn give you the blueprint about how the chips work But you can 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. Yeah, it's exactly like that. So we basically apply the same strategies from fuzzing research to the DSP. 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 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. I mean, it vaguely rings a bell, but maybe give us some background on that. 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 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 book. But the thing 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 KaleScale, but one big customer ever like actually hit this book. 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 specifically hit this bug, but it was exercising the relevant code. And I just ran it in a loop. And 15 minutes later, the fuzzer found the exact bug, like narrowed it down to the exact order 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. 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 discovered it? 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 the default journal-based transactional system. So basically, I wrote a generic workload that just sort of exercised the entire system. And that still found the bug in 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 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. 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. 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, were 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 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 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 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 can go back in time and you could 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 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 where the bug was sort of locked into the simulation. So yeah, those are some of the ways that we help. So we had Joe Hellerson from AWS a little while ago talking about the project Hydro.

Are you familiar with Hydro? I don't think I am. 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 is kind of like trying to prove this stuff up front. Maybe you can 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 in tension, or are they sort of complementary? Yeah, and 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? 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 it 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 basically baked into the software. You can think of it the same way that you might do a type system check on you're suddenly stuffing an int into a string or vice versa. Yeah, that makes sense. I don't think these approaches are necessarily in tension. So let me explain why. So first of all, hydro is a very advanced form of other kinds of static verification. So for example, 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 the 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 it more deeply as to like whether or not it has any kind of compromises. 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 kind of top of the file 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 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, 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 Hydra, so I can't say maybe they've made something even better, but the traditional solution to this or other traditional ways of doing this that I've seen, like rolling your own DSP, involves a very high tax 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 modeling, you create like 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. There's a lot of different ways of testing software. We've mentioned a few of them around like unit tests, system tests there compilation as a test Like I guess the approach that you 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? So I think where the antithesis style testing,

So deterministic simulation testing fits into like the 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. 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 antithesis really, really serves you 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 away, sends a read to another node and then it fails. Testing these types of systems in integration tests, I find 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. 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. Even at database, 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 could absolutely occur

even in a very simple three-tier architecture or something like that. 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. 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 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 hyper-focus on the goal you give them. So if you give them a goal... You're basically overfitting to the test. 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 make the code behave to pass the test, there's nothing really to overfit to. You're trying to solve very general purpose properties. The database never goes corrupt. And it's much harder to overfit to those properties. And so you just end up basically being forced to just implement the code in the most generic and correct way possible. What is the cost to the development lifecycle in terms of 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, this code doesn't work because it doesn't compile or this code doesn't work because it doesn't pass the unit test. Yeah, so the question is basically like, you know, how tight of an iteration loop can we create and like what's the sort of cost of development? So there's a couple of different ways to answer that question. So the first question, the first way to answer it 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, 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 into this 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? 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. 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 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. 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. 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, 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. I totally agree with that. I think that as we sort of see the like time it takes code, effectively as 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 specifications and being able to prescribe exactly what you want in 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. where you want your verification to be a net of saying, for all possible paths, do they all match my specification, right? And the antithesis sort of story to this is that your specification should derive properties and invariants of the code that you want. You should encode those into the workload that is running an 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.

Carl, as we start to get closed on time here, is there anything else you'd like to share? 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, I've been thinking about the reality of coding sort of becoming almost like diffusion, like image diffusion, if you've seen 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 code base. 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 code base 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. Yeah, absolutely. I mean, this was super fascinating. I feel like we're just 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. 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. Carl, thanks so much for being here. And cheers. Cheers. Thanks, John.