Introducing stateful-check: generate programs, not values

A stateless property looks for an input that breaks an invariant: a string the parser chokes on, a number that overflows. Generate enough inputs and you find it. But a whole class of bugs never shows up in a single input — it lives in the sequence of operations. The read that runs before the write. The setter that quietly clobbers an unrelated field. The retry that applies the same change twice. You can't reach those by generating more values. You have to generate programs.

I ran into this building content-credentials. I'd hand-rolled a few stateful tests there — draw a sequence of operations, run them against the real thing and against a simple model of what should happen, and compare after every step. One of them caught a bug that a green unit test had hidden (that's its own story). The tests worked. But they were hand-rolled: no shrinking, no reuse, tangled into that one project.

Erlang has had this properly since 2006; Clojure, Python and TypeScript followed. PHP hadn't. So I pulled the pattern out into its own package.

How it works

You describe each operation as a command with four methods: when it may run, how to run it against the real system, how it advances a shadow model of the expected state, and whether the system still agrees with the model afterwards. The model is the oracle — deliberately simpler than the system, so it can't hide the same bug the system has.

$deposit  = Gen::map(fn (int $n) => new Deposit($n),  Gen::integers(1, 100));
$withdraw = Gen::map(fn (int $n) => new Withdraw($n), Gen::integers(1, 100));

$result = (new StatefulProperty(
    alphabet: [$deposit, $withdraw],
    initial: Gen::integers(0, 1000),          // a starting balance, drawn per run
    setup: fn (int $opening) => new Setup(
        model:  new LedgerModel($opening),    // the shadow model
        system: new Account($opening),        // the real thing
    ),
))->check();

stateful-check generates sequences of these commands, runs them, and checks the model after every step. When it finds a failure, the part that earns its keep is the shrinker: it takes a twelve-command sequence that fails and reduces it to the two commands that actually matter — and the smallest arguments that still break it. You get a minimal reproduction, not a haystack. And because generation is seeded, that reproduction is deterministic: same seed, same failure.

What it doesn't do

I'd rather say this up front than have you find it out.

• No parallelism, no race detection. PHP is share-nothing and request-scoped. The Erlang original's headline feature — finding races — isn't available here, and I won't pretend otherwise.
• A local minimum, not a global one. The shrinker guarantees that no single further reduction still fails. It does not search exhaustively for the smallest possible counterexample.
• Command choice isn't shrunk. It drops commands and shrinks their arguments, but won't swap a complex command for a simpler one that would have failed too.

There's also a stateless runner for ordinary one-value properties, and an opt-in edge bias that makes generation hit the boundaries — 0, the minimum, the maximum — where off-by-one bugs cluster and uniform random almost never lands. Both are in the README.

Where it is

provemark/stateful-check on GitHub. No runtime dependencies beyond PHP 8.2 — generation is built on the Random extension, which is what makes shrinking reproducible. Spec-driven throughout: every change starts from an approved spec, every acceptance criterion maps to a test, and every one of those tests is proven to fail when the behaviour it checks is broken.

If you've ever watched a green suite sail past an ordering bug, this is the shape of test that catches it.