Worried about AI slop in the code you're dealing with? Wondering how AI agents can help you move faster without leaving a nest of bugs behind? Concerned about the future of software reliability? Me too.
I always knew of some tools that could help check correctness of my code, but until recently I didn't have a good understanding of the state of the art. I suspect I'm not alone: the landscape of software-correctness tools can feel amorphous and forbidding. Commercial offerings often indulge in vague promises, while open-source tools tilt toward highly academic terminology, from "formal methods" down to "model checking" and "property-based testing". How does all that relate to the day-to-day experience of evaluating code—human-generated or otherwise? This post is my attempt to lay out the space for the rest of us.
Think of your software as a room full of bugs. Our goal is to construct techniques that shrink the interior of this room as much as possible.
The floor of this room is assembly code—whatever the compiler emits onto bare metal. The ceiling is a formal proof that the program meets its specification, machine-verified from the top down. Everything between the floor and the ceiling is where bugs live.
The bugs in this room come in two kinds. Bugs regarding universal properties violate rules that every program should follow—type safety, memory safety, avoiding data races, etc. Bugs that break arbitrary properties violate the rules that are specific to your program—things like "every voter can only vote once" or "the game physics must observe Newton's laws". (Folks sometimes call this "business logic", which always felt limited to me; software is not only for business!)
To shrink the room, the field pursues two complementary strategies:
The room. Correct-by-construction raises the floor beneath every program; correct-by-verification pushes the wall in from the side, sealing specific stretches of code. The screen passes through what remains between floor and wall.
Correct by construction raises the floor. The language refuses to compile programs that could violate a universal property, so the property holds for every program the compiler accepts. Classical type systems raise the floor by forbidding misapplication of code to inappropriate classes of data. Rust raises the floor against memory bugs. Hydro raises it against Heisenbugs in distributed programs. Every universal correctness property we migrate into the compiler is another layer on top of the floor, pushing it a bit higher.
Correct by verification pushes a wall in from the side. For arbitrary properties about your specific program, you write proofs. Verus and Stainless let you annotate real code with specifications and "discharge the obligations" (i.e. prove what needs to be proved) with an SMT solver. Where they succeed, floor meets ceiling for the stretch of code they cover—bugs are eradicated in that part of the room. This is the beautiful, impossible dream of a research community that has been at it for more than half a century: prove an arbitrary program meets its full specification. The impossibility-in-general is a mathematical fact going back to Turing, but the progress toward useful-in-many-cases has been real, and the wall is further in than you might expect. And LLMs are helping steer these formal tools to drive the wall a bit further.
The two moves aren't fully distinct. Distributed safety is a universal property in Hydro (correct by construction) but a bespoke "proof obligation" in plain Rust (correct by verification). The boundary between the two has been shifting toward "universal" for decades: a property that researchers first learned to prove by hand on specific programs eventually gets captured by someone's new type system, at which point every future program gets the property for free. So the two correctness strategies aren't technically orthogonal, but the general framing is useful.
Whatever is left over—the uncovered space above the raised floor and within the inward wall—we solve with some form of disciplined-but-incomplete testing. Techniques like model checkers and fuzzers pass a screen through the gap, catching bugs that happen to land in the weave. The screen keeps getting finer, but it is also fundamentally holey, and not in a divine way.
Raising the floor
The floor has not been bare assembly for a very long time. We've been layering on top of it for decades.
The first serious layer is types. A type system refuses programs that mix integers with strings, dereference nulls that the compiler can't locate, or reference fields that do not exist. The errors it rules out are not minor—they are, historically, among the most common things people got wrong. Once a language insists on static types, those bugs stop being possible to write.
The second is memory safety. Rust's borrow checker guarantees, at compile time, that programs don't dangle pointers, double-free, or race over shared memory in the primitive C/C++ sense. Microsoft reported in 2019 that about 70% of their security CVEs fell in the memory-safety bucket; Rust takes that whole bucket off the table. (Not for free: you spend time arguing with the borrow checker instead of debugging segfaults. But many of us happily make that trade, especially now that LLMs do a lot of the arguing with the borrow checker for us.)
The third, and the one my team spends most of its time on, is distributed safety. This is what Hydro is after. Distributed programs misbehave because they make silent assumptions about message ordering, delivery, retries, failures. Hydro refuses to compile programs that use those assumptions without declaring them. Collections carry their ordering and retry guarantees in their types. The few places where the program's behavior genuinely depends on the environment are tagged with a nondet! keyword; everything else is deterministic by construction. Hydro makes an entire category of distributed Heisenbugs un-expressible—e.g., races induced by false assumptions about possible execution orders—in the same spirit that Rust made use-after-free un-expressible.
Each of these layers is laid down by the language designer. They ensure programmers will never see a class of bugs. If the code compiles, the bugs that would live below the floor are not in the room. The programmer's budget—and the testing budget—can be spent on what's left.
Pushing the wall in from the side
Universal properties aren't everything you want to prove. Most program correctness is application-specific: perhaps a data structure must preserve an invariant, services need to follow a protocol, or an algorithm has some numerical property to maintain. No language can bake those into its type system without becoming the application itself.
For those, we push a wall in from the side. One family of tools lets you annotate your real code with assertions about what it should do, and the verifier mechanically proves the code satisfies them — the build fails if it can't. Verus and Prusti do this for Rust; Dafny is a long-running project in this family; Stainless does it for Scala. When they succeed, the stretch of code they cover is sealed: floor meets ceiling outright, and no bug can appear in that program's part of the room.
A second family of verification tools asks you to write a separate specification in a dedicated language and checks the spec on its own terms, with no mechanical tie to the deployed code. We'll come back to that family in a moment; the "no mechanical tie" caveat is where its trouble lives.
The cost is the usual cost of real verification: writing the actual specifications, discharging proof obligations, waiting on the solver. Walls can only move so fast (modern solvers sometimes resort to exponential algorithms); the general problem is undecidable as shown by Rice's Theorem, and not every program is practical to verify at the current state of the art. But verification often does work, and every piece of code that lands "behind the wall" is a piece the screen doesn't have to cover, and the testing budget doesn't have to pay for.
Fancy Tests: Screening the middle
For whatever is still in the room, we throw a screen at it. There are different kinds of these screens: model checking, fuzzing, property-based testing. All pick an invariant, pick a search strategy in "the room", and try to find a trace that violates it. Anything caught in the screen is a bug we found before production did.
The screens have gotten remarkably good. TLA+ and P have been the model checkers of record for protocol work, although they have issues I'll point out in a moment. Jepsen pummels distributed databases with faults and then checks whether the resulting histories still satisfy application-level consistency invariants like linearizability and isolation. Shuttle, Turmoil, and HydroSim are simulation testers that hook into your actual code's scheduler, network, and clock, so unlucky interleavings can be replayed deterministically. Antithesis generalizes the idea further: it runs your entire system as a black box in a deterministic hypervisor, giving the same replay guarantees without requiring language-level hooks. Each of these tightens the weave in its own patch of the room.
Despite the formal-sounding name, model checkers are just brute-force testing machines that exhaustively look for bugs in a finite slice of your program's state space. You bound the parameters—say, five nodes, ten in-flight messages, two possible values per register—and the checker enumerates every reachable state within that bound to see if any violates your invariant. Within the bound, nothing escapes. The holes are everything outside the bound: the six-node case, the eleventh message, the value you didn't model. State explosion forces the bound to be small, though, and the smaller the bounds the bigger the holes.
Fuzzers and property-based testers come at it from the other direction: generate inputs or schedules at random, run the system, see what breaks. Classical fuzzers watch for the obvious failures—crashes, hangs, assertion violations, etc. Property-based testers (QuickCheck, Hypothesis, proptest) let you declare an invariant that should hold on every generated input, which catches wrong-answer bugs that don't crash. Coverage-directed fuzzers (like AFL and its descendants, including HydroSim in fuzzing mode) go further: they instrument the binary to see which code paths each input exercises, and preferentially mutate inputs that reach new ones. That turns fuzzing from blind sampling into something closer to guided search. The holes are the paths the generator never stumbles onto in a reasonable time budget: deep branches gated on improbable inputs, race conditions that need a very particular interleaving, and bugs the oracle doesn't recognize as bugs.
The mesh in these screens has been getting finer over time, but it's still holey. And because the gap between floor and ceiling is far wider than any one pass can cover, bugs lurk between the holes.
I'm a big fan of simulation testing and fuzzing. But I have issues with many of the most popular tools in the area, including some of the most famous ones like TLA+.
Screens and Ceilings in the wrong room
If your program is a room full of sneaky little bugs, there's little to be gained by looking for them in a neighboring room!
I recently had an engineer describe an off-by-one error that showed up in some tricky Java code for database recovery. They asked me if they should have written a spec for the recovery protocol in P—would they have caught the error? My answer: absolutely not! The odds that the P spec would faithfully capture every operational detail of the Java implementation would be near zero.
In model checkers like TLA+, P, or Alloy, the model is a spec written in a dedicated specification language, while the deployed system is written in a full programming language like Go, Rust, or Java. In interactive proof assistants like Lean, Rocq (formerly Coq), or Isabelle, you prove an algorithm correct by hand; what ships to production might be a C++ port written by someone who read the paper. In both cases the checking is being done on a careful, idealized spec of the system. The real system is a different artifact, and nothing in the tool enforces that the two agree.
Over time the gap gets worse, because implementations drift. The implementation might gain a retry path that wasn't in the model; later, someone tightens a timeout to meet an SLA or adds a feature the TLA+ spec never heard about. Every one of those changes opens a seam between the spec and the code. The model checker keeps happily reporting no violations in the spec, which is true. The system the spec describes stopped existing six months ago.
This is a practical failure mode, not just a theoretical caveat. A proof can remain valid while the production code evolves away from the program it describes.
(The drift problem is specific to tools that check a separate model. The simulation testers mentioned earlier — Shuttle, Turmoil, HydroSim, and Antithesis — all work on your actual deployed system and don't have this problem.)
Testing the real room
The fix is to make the deployed code be the thing the screen passes through.
That is the bet in Hydro. The program is written in Rust, with Hydro's extensions. The very same code is what runs in production and what HydroSim—Hydro's built-in model checker—explores. The screen doesn't walk a translation of the code; it walks the code.
The invariants are unit tests. You already write those! HydroSim upgrades a standard unit test from "does this pass in one scheduling?" to "does this pass under every scheduling, every delivery order, every message loss the Hydro type system said was legal?", up to some bound of model checking. Because the type system has already pushed the floor up, every path not marked nondet! is deterministic by construction—there is nothing in those paths left to search. The screen spends its entire budget on the few places where the program genuinely has to confront non-determinism.
If the code changes, the thing being sampled changes with it. There is no model drifting away from the production system, because there is no separate model. The screen is being passed through the room you actually ship.
This approach is especially well-suited to the hardest category of bugs: the heisenbugs that depend on uncontrolled environment randomness. The comparison with runtime-level simulators like Shuttle, Turmoil, and Antithesis is substantial enough to deserve its own post, which is up next.
Where the room is heading
A complete solution to removing bugs will probably have to await a major shift in popular programming paradigms, which is the subject of a future post. Meanwhile, we have three complementary moves to make in our bug room. Most tools fit neatly into one of the three categories, so mixing and matching is needed. Hydro is an example that integrates across multiple categories: it raises the floor with new types, and offers a screen—HydroSim—designed to fit perfectly with that floor. We're also contemplating Hydro-Verus integrations that bring in the wall on the right as well. More on that as it emerges!