Why Antithesis?

Home

Blog

Why Antithesis?

October 30, 2026 | Hillel Wayne, Developer Educator

Hillel WayneDeveloper Educator

In this post

Making formal methods work

In which I use the word “nondeterminism” too many times

DSTplacing luck

So really, why Antithesis?

The latest from antithesis

The latest

Monthly reliability and distributed systems news, curated for teams building critical software.

Please enable JavaScript in your browser to load and submit this form.

Check your inbox for your confirmation message.

We couldn’t submit your form. Please try again later.

When I told people I was joining Antithesis, I got two responses:

There’s a misconception that software verification is like an “evolution of Man” diagram, with unit testing becoming property-based testing becoming formal verification. In reality, these all make different tradeoffs in the verification space, a topic on which I am now going to spend 2000 words boring you to tears.

To start, let’s lay down a premise: there are things that should be true in your system, no matter what. “What” here is inputs, user events, server behavior, execution order. Let’s call these properties. If a property you want is not true in your system, then you need to fix something.

A widespread example of this is type safety: If a function has type String -> Int, that means no matter what string is passed in, the output is an integer. And this can be automatically verified, both that the function is only called with strings and that the output for every string is an integer.

Formal methods just asks “why can’t we do this with any property?”

We might want to be sure that our unsafe Rust never has a memory error, or our consensus protocol eventually elects a leader, or our optimized function behaves identically to a simple one. We’re already used to reasoning about these properties in our brains. Formal methods takes this reasoning and turns it into a mechanical check: if the code doesn’t have the properties we want (or we can’t prove that it does), the code won’t compile. You can see examples of this at the project Let’s Prove Leftpad, which shows how you can prove Rust code, C code, and about two dozen more languages.

Formal methods works okay for small, pure functions like leftpad, but gets really messy when we add concurrency, state, or other systems. Let’s say we want to prove that a block of code doesn’t have a race condition. For a toy example, I’ll have two threads check if a counter is zero and, if it is, increment it. The property, then, is “after the code finishes, counter == 1.” Here it is in C++:

// race.cpp

#include <cassert>

#include <thread>

#include <vector>

const int NUMTHREADS = 2;

int counter = 0;

void update()

{

if (counter == 0) counter++;

}

int main()

{

std::vectorstd::thread threads(NUMTHREADS); //create 2 threads

for (int t = 0; t < NUMTHREADS; t++) threads[t] = std::thread(update); //make each thread update the counter

for (auto& th : threads) th.join(); //wait for all threads to finish

assert(counter == 1);

return 0;

}

#include #include const int NUMTHREADS = 2;int counter = 0;void update(){ if (counter == 0) counter++;}int main(){ std::vector threads(NUMTHREADS); //create 2 threads for (int t = 0; t

I ran this code 100,000 times and the assert didn’t fail once, so I (falsely) believe that the property is true. But if I want to prove this property always holds, whatever proof I write would need to account for C++ thread semantics. And account for the compiler we used. And the compiler optimizations we used. And the number of CPU cores on the target machine, and the phase of the moon, and a dozen other things.

This was on an exe.dev box, with both threads pinned to one CPU. I reran the experiment with two CPUs and the code failed exactly twice. We’ll talk about why later.

If compiled with -O1, gcc rewrites the counter++ into counter = 1.

And once we do all that, we have a proof of this exact code, with these exact APIs and data structures. We have to start over if someone replaces the threads with processes or, heaven forbid, counter with a Redis key. Do you have a complete formal model of Redis? I don’t think Anthropic has a complete formal model of Redis.

In conclusion, the answer to “why can’t we just prove any property?” is “because it’s really frickin’ hard.”

Does that make formal methods useless? Of course not. It makes them expensive. In practice, we can do one of two things to make them cheaper. The first is to prove a tiny, mission-critical part of the system instead of the whole thing. That’s what we did to prove the thread-safety of a C++/Rust bridge primitive. The second, and more common approach, is to abstract. I mentioned that a proof of the C++ needs to cover the complexities of C++ threading behavior. If we handwave that away, we can write a pseudocode-like representation where threads can run in any order and some actions are mystically atomic. This is in the same algorithm in the formal specification language TLA+:

Actually PlusCal, a higher-level DSL on top of TLA+.

---- MODULE counter ----

EXTENDS Integers * "import integers"

(*--algorithm counter {

variables counter = 0;

define {

NoRace == <>[](counter <= 1) * The algorithm finishes with counter at most one

};

fair process (thread \in {1, 2}) * Create two threads

{

Check: * Check block is one atomic action

if (counter = 0) {

counter := counter + 1;

}

};

}*)

====

[](counter

This creates two threads that each run the body of Check in a single step. Notice we don’t say which thread runs first. In a real system this would depend on the thread scheduler, here TLA+ can try whatever it thinks will break the property. In any case, we can use a model checker (called TLC) to explore all of the possible states of this system. Running the model checker confirms that no matter what, the property is preserved. Success!

But, ah, I said that Check is a single atomic step. That means TLA+ can’t make one thread preempt the other in the middle of the if block. If there’s a bug, that’d be the source, so why not see what happens if Check is two steps?

Check:

if (counter = 0) {

• Set: * Now incrementing is in a separate atomic block from the if

counter := counter + 1;

}

Now the model checker finds a bug in our system:

Temporal property NoRace was violated.

[I'm skipping showing the error trace for this blog post]

This turns out to be a bug in the C++ program, too. I ran the test another 6 million times and the bug only appeared 8 times, which explains why I didn’t see it in “only” 100k runs.

To understand the bug, let’s have the model checker generate the whole state space:

Following the blue arrow represents the first thread evaluating if, and then evaluating counter++. The red arrow represents the first thread evaluating if, and then the second thread evaluating the if, and then both (in either order) incrementing the counter. So there’s a race condition where we increment the counter twice, and our property is violated. We learned this without having to know anything about how the real world scheduler works.

Abstract models are incredibly good at exploring high-level behavior. If I want downloads in my system to sometimes fail, I don’t have to model network outages or my disk filling with junk; I can just write “downloads either succeed or fail”. I also don’t need to think about the nitty-gritty details of what I’m modeling. Is counters stored in memory, in a database, or in an old tally counter? Are the thread processes literally threads or are they separate computers? Doesn’t matter, don’t care, same model either way.

The devil is literally in the details, though. The model may correspond to the actual system, but they’re not the same. What if I make a mistake in implementing the system? Or worse, what if one of those details I handwaved away was absolutely critical to correctness? When I first modeled if (counter == 0) counter++ as a single atomic action, TLA+ didn’t catch the bug.

Abstraction is a powerful tool because it’s so much faster and easier than doing a full end-to-end proof. But since it distances us from the code, it’s low “fidelity”. It finds issues in the design, not issues in the code.

Formal proofs are too expensive, modeling is too abstract, and regular testing is too unreliable. Antithesis solves exactly one of those problems.

Specifically, it solves unreliability. The root of that problem is that tests have no control over the broader system. Let’s go back to these three states:

We have a nondeterministic choice here: either have thread1 run counter++ or have thread2 run if. But while the model is nondeterministic, the model checker is totally deterministic. It first sees what happens if thread1 runs (following the blue arrow), then rewinds and sees what happens if thread2 runs (following the red arrow).

race.cpp can’t pull the same trick. When it runs std::thread(update), it hands off control of the thread to the operating system’s thread scheduler. So it only finds the bug if the scheduler just so happens to interrupt thread 1 between if and counter++, a window of literally one CPU instruction. So almost all runs follow the blue arrow, and we have to get very lucky to see the red arrow.

This is why we see more errors if we run race.cpp with each thread on a separate CPU. Then both can run simultaneously, and we don’t need an unlucky thread interrupt to trigger the bug. It’s still very rare, though.

This is the problem with testing nondeterministic systems. Lots of bugs come from a combination of factors, like “these processes ran out of order in the middle of a network partition while a user was uploading a ten hour video”. These are all totally outside the test’s control and it could take billions of runs for them to all coincide.

If we want our testing to actually hit rare cases, we need some way to externally trigger nondeterministic effects. In other words, we need to make it a little more like model checking.

And this brings us to Deterministic Simulation Testing (DST).

DST is basically just doing the same thing as model checking, except with a real codebase. We run the whole system in a VM managed by a deterministic hypervisor that can control nondeterminism, inject transient errors, and rewind the simulation to previous states. If it thinks interrupting thread 1 between if and counter++ would lead to a new state, it can first run the system without the interrupt, and then rewind and try it with the interrupt and see what happens. And then rewind and try it with an interrupt and a clock skip, just for good measure.

Let’s demonstrate this with a tweak to race.cpp. Instead of looking for a 2-thread race condition, we’ll look for a 64-thread race condition.

const int NUMTHREADS = 2;

const int NUMTHREADS = 64;

assert(counter == 1);

assert(counter != 64);

Just to be thorough I ran this one hundred million times and never even saw a 3-thread race. Run this on Antithesis for five minutes and it finds the 64-thread race a hundred times.

This isn’t as rigorous as formal methods. Proofs and model checkers verify the property for all possible executions, not merely a very large number. But it doesn’t require us to model the whole universe or check only an abstraction of our code, it works for our codebase as it is. It works whether the language is C++, Python, or an internal DSL, whether the workers are threads, processes, or servers, and whether the counter is stored in a variable, a Redis key, or a Postgres table row.

So, why am I joining Antithesis if I already do formal methods? Because the formal methods I do verifies a low-fidelity blueprint of the system across all possible executions, while Antithesis verifies the actual system across a subset of executions. They are different approaches with different strengths and weaknesses, and both serve important roles in the correctness landscape. Correctness is no