Every LRU cache bug I have ever seen looked like this in the bug report:
Sometimes it returns the wrong value under load.
And like this once someone found it:
put("a", 1); put("b", 2); get("a"); put("c", 3)
# expected "b" to be evicted; "a" was evicted
Four operations. Trivially reproducible. Obvious in hindsight. And nobody writes that test, because writing it requires already suspecting that get fails to refresh recency — which is the thing you were trying to find out.
This is the structural limit of example-based testing on stateful objects. The bug is not in an operation; it is in an interaction between operations, and the space of interactions grows exponentially while your imagination does not.
The idea
Hypothesis’s RuleBasedStateMachine inverts the work. You describe the operations and the things that must always be true; it generates sequences of operations, runs them, and when something breaks it shrinks the sequence to the shortest one that still breaks it.
from hypothesis import strategies as st
from hypothesis.stateful import RuleBasedStateMachine, rule, invariant, precondition
class LruCacheMachine(RuleBasedStateMachine):
def __init__(self) -> None:
super().__init__()
self.cache = LruCache(capacity=3)
self.model: dict[str, int] = {} # a plain dict, insertion-ordered
@rule(key=st.sampled_from("abcd"), value=st.integers(0, 5))
def put(self, key: str, value: int) -> None:
self.cache.put(key, value)
self.model.pop(key, None)
self.model[key] = value
while len(self.model) > 3:
del self.model[next(iter(self.model))]
@rule(key=st.sampled_from("abcd"))
def get(self, key: str) -> None:
got = self.cache.get(key)
want = self.model.get(key)
assert got == want, f"get({key!r}) -> {got!r}, model says {want!r}"
if want is not None:
self.model[key] = self.model.pop(key) # touching refreshes recency
@invariant()
def never_exceeds_capacity(self) -> None:
assert len(self.cache) <= 3
@invariant()
def lru_order_matches_model(self) -> None:
assert self.cache.keys_in_lru_order() == list(self.model)
TestLruCache = LruCacheMachine.TestCaseThat last line is what pytest collects. Everything else is a description of the contract.
Model-based is the technique that matters
The two @invariant methods compare the cache against self.model — a second, deliberately naive implementation. This is model-based testing, and it is the highest-leverage form of stateful testing because the model is allowed to be slow, memory-hungry and stupid. A plain dict with an explicit eviction loop is obviously correct in a way an optimised doubly-linked-list cache never is.
The rule that makes or breaks it: write the model from the contract, not from the implementation. A model derived by simplifying the code under test agrees with it perfectly, including where the code is wrong. If you find yourself opening the implementation to remember what put does on an existing key, stop — that question is the specification, and you should be answering it from the docstring or asking the person who owns it.
💡@invariant() runs after every rule. @rule methods can also assert. When does each belong?
click to reveal
A postcondition is a claim about the operation you just performed: get returned what the model says it should. It belongs in the rule, right next to the call, because that is where the arguments are in scope and where the failure message can name them.
An invariant is a claim about the object’s state that must hold at every observable moment, independent of what happened last: size never exceeds capacity, the LRU order matches the model, no key appears twice. It belongs in @invariant because you want it checked after every rule, including rules that were written later by someone else who did not think about it.
The practical difference shows up when you add a fifth rule six months from now. A postcondition in get says nothing about the new evict_expired rule. An invariant checks it automatically — and that is precisely how invariants find bugs in code written after the test.
There is a cost to be aware of: invariants run after every single step, so an expensive one (a full structural validation of a large tree) multiplies your runtime by the sequence length. The usual compromise is a cheap invariant that runs always and an expensive @rule named check_deeply that Hypothesis schedules occasionally, which gives you full validation at a sampled rate rather than never.
Preconditions and bundles
Two more pieces of vocabulary handle the shapes real state machines have.
@precondition guards a rule that only makes sense in some states — you cannot pop an empty queue, or commit without an open transaction:
@precondition(lambda self: self.transaction is not None)
@rule()
def commit(self) -> None:
...
Without it, half your generated sequences fail on an operation the API never promised to support, and you spend your afternoon adding if statements to the test.
Bundles let one rule consume what another produced, which is how you model handles, ids and sessions:
keys = Bundle("keys")
@rule(target=keys, key=st.text(min_size=1, max_size=3))
def insert(self, key: str) -> str:
self.cache.put(key, 1)
return key
@rule(key=keys)
def lookup(self, key: str) -> None:
assert self.cache.get(key) is not None
lookup now only ever receives keys that were actually inserted, so the generated sequences spend their budget on interesting interleavings rather than on lookups of random strings that were never there.
Why the shrunk sequence is the entire payoff
Suppose the machine finds a failure after 47 operations. That artefact is worthless — you cannot read it, cannot reason about it, and cannot put it in a commit message. Hypothesis then does the work that makes the technique usable: it removes operations, simplifies arguments, and re-runs, keeping any variant that still fails, until nothing further can be removed.
What lands in your terminal is four lines. Four lines you can paste into a unit test, attach to a ticket, and hand to whoever owns the cache. A minimal reproducing sequence is a different kind of object from a random failure — it is a specification of the bug.
This is also why exhaustive search over a small alphabet gets minimality for free, without any shrinking machinery. If you enumerate all sequences of length 1, then all of length 2, and so on, the first failure you hit is already minimal: any earlier-diverging prefix would have been found at a shorter length. Hypothesis shrinks because it samples rather than enumerates, and it samples because real state spaces are far too large to enumerate. The trade is explicit — exhaustive search gives you minimality and a tiny reachable space; random search plus shrinking gives you a huge reachable space and minimality after the fact.
💡A stateful machine has been running in CI for a month and has never failed. Your colleague says it proves the cache is correct. What is wrong with that, and what would strengthen it? click to reveal
It proves that the sequences Hypothesis happened to generate, over the alphabet you wrote, with the strategies you chose, did not violate the invariants you thought of. Every clause in that sentence is a limit.
Three specific gaps, in the order they usually matter.
The alphabet. If the machine has get and put but not delete, clear or resize, no sequence will ever exercise them. Whole methods can be absent from the model and the machine reports full health. The first thing to check when someone says a stateful test found nothing is which public methods are missing rules.
The strategies. st.sampled_from("abcd") cannot reach a capacity-overflow bug in a cache of size 10. st.integers(0, 5) will never produce the value that breaks a serialisation path. Sampling from a small key set is usually right — it forces collisions and evictions, which is where the bugs are — but it means the reachable state space is a deliberate choice you should be able to justify.
The invariants. The machine can only fail on a claim you wrote down. If nothing asserts that entries are removed on delete, a delete that silently does nothing passes forever.
What actually strengthens it: run the machine against a deliberately broken copy of the implementation and confirm it fails. Mutate the eviction to take the most-recently-used, mutate get to skip the recency refresh, mutate the capacity check to >=. If the machine catches all three within a few seconds, you have evidence about the test. If it catches none, you have learned something far more useful than another green run.
That is mutation testing applied to a property test, and it is the only way to distinguish “no bugs” from “no assertions”.
When to reach for it
Stateful testing pays off in direct proportion to how much internal state the object has and how many orderings are legal. Caches, connection pools, rate limiters, parsers with modes, transaction managers, undo stacks, any protocol implementation. It is overkill for a pure function — that is what plain properties are for.
The other signal is a bug report that contains the word “sometimes”. Any object whose failures are described that way has an interaction bug, and interaction bugs are exactly what a machine finds and a human does not.