Download River's slides here.
Property-based testing is a subject near and dear to me. Where a normal example-based test asserts that one specific input produces one specific output, a property-based test asserts something about the behaviour of the system - an invariant that must hold for all inputs - and then lets an adversarial generator go hunting for the inputs that break it.
I’ve leaned on this frequently in my work on XTDB. So much of a database is long sequences of stateful operations that can interact in surprising ways, and our polymorphic type system fans out into far more combinations of cases than anyone could sit down and enumerate by hand. Properties let us test enormous amounts of that ground quickly and cheaply, in a way that example tests never could.
River Keefer (of Antithesis) picked this thread up in his XT26 talk, “Extracting Reliable Software from Unreliable Machines”. He opened with an observation from computing history: “We know from history that it’s possible to build reliable systems from unreliable components”. Whatever else is true about LLMs, their unreliability is hard to argue with (“Fundamentally unreliable tools, in some sense”) - but the concept of unreliable components is not a new one. We build dependable storage on failure-prone disks and distributed systems on unreliable networks, and the same thinking, he argued, applies to large language model output. The question is what the reliability layer looks like when the unreliable component is the thing writing your code.
As development velocity increases, verification becomes the single most important task we can undertake - and a property is exactly the kind of verification that scales: a specification the model can be held to, not a handful of examples it can pattern-match its way past. River went further, describing property-based tests as “a beautiful form of specification for LLMs” - like a high-level programming language for working with them.
While writing good properties is a job best suited to humans with deep knowledge of a system’s semantics, River showed an LLM can do it effectively too: he demonstrated a case where an LLM generated some simple property tests against well-known open source repositories and uncovered complicated bugs - proof that “you don’t have to have complicated properties to find complicated bugs”. Whether the properties are written by a human or generated by the LLM itself, they give you a good way to verify that LLM-generated code changes don’t affect the behaviour of the system.
River then turned to what happens when a property fails. Shrinking kicks in: the framework doesn’t just report the failure, it automatically searches for the smallest possible counterexample, without extra work on your behalf. This has been invaluable in our work on XTDB - going from a failed property to an immediately minimised example strips away unnecessary context and drills straight to the heart of a bug. And that shrunk output is just as useful to both humans and LLMs: a minimal counterexample gives a far clearer picture of a failure case than a sprawling test log, making the underlying bug much easier to both understand and fix.
Thanks to River for a fantastic talk!
Want to be the first to know when the XT26 talks drop? Register here and we’ll send the link straight to your inbox.
