Continuous Quality and Deterministic Verification

6.1 Property-Based Testing at Scale

An example-based test asserts that one input produces one output. It documents a case and it explores nothing. The bugs it finds are the bugs the author anticipated, which are not the bugs that reach production.

A property-based test asserts something that must hold for all inputs, and a framework generates many inputs to try to break it. The generator explores the space, including the boundaries and the degenerate cases that nobody writes down.

Finding the properties

The difficulty is not the tooling, it is identifying a property. Five patterns cover most cases, and they are worth learning as patterns because the first one is always the hardest to see.

A round trip asserts that decoding an encoding returns the original. It applies to serialization, compression, parsing, and any transformation with an inverse, and it is the single highest-yield property in most code bases.

An invariant asserts that something is true of every output regardless of input: a sorted list is ordered and is a permutation of the input, a balanced tree satisfies its balance condition, an account balance never goes negative.

An oracle compares the implementation against a simpler one known to be correct. The simple version is slow or has the wrong complexity, which is why it is not the implementation, and it is obviously correct, which is why it is a good reference.

A metamorphic relation asserts a relationship between two runs without knowing either answer. Sorting a list twice gives the same result. Searching a superset returns at least as many results. Adding a constant to every input shifts the mean by that constant. This pattern covers code where no oracle exists, which includes most numerical and machine learning code.

An algebraic law asserts that an operation is commutative, associative, idempotent, or has an identity. Any merge function claims one of these, and Volume II's conflict-free replicated data types depend on all three.

from hypothesis import given, strategies as st, settings

# Round trip. Finds encoding bugs on empty input, on the maximum value,
# on surrogate pairs, and on anything the author forgot.
@given(st.binary())
def test_encode_decode_round_trip(data):
    assert decode(encode(data)) == data

# Invariant. Two assertions, because "sorted" alone passes for a
# function that returns an empty list.
@given(st.lists(st.integers()))
def test_sort_invariants(xs):
    result = my_sort(xs)
    assert all(a <= b for a, b in zip(result, result[1:]))
    assert sorted(result) == sorted(xs)

# Metamorphic. No oracle needed, and it catches non-determinism.
@given(st.lists(st.floats(allow_nan=False, allow_infinity=False)))
def test_ranking_is_stable(xs):
    assert rank(xs) == rank(xs)

# Algebraic law. Any CRDT merge must satisfy all three.
@given(st.builds(CounterState), st.builds(CounterState))
def test_merge_is_commutative(a, b):
    assert merge(a, b) == merge(b, a)

Stateful testing

Most real bugs need a sequence. A single operation on a data structure is usually correct, and the fifth operation after a particular third one is not.

Stateful property testing generates sequences of operations against a model. The framework picks operations subject to preconditions, applies each to both the real system and a simple model, and asserts that the observable state matches after each step.

from hypothesis.stateful import RuleBasedStateMachine, rule, invariant, precondition

class CacheModel(RuleBasedStateMachine):
    """The model is a plain dict plus an insertion order list.
    The real cache is a concurrent LRU with eviction and expiry."""

    def __init__(self):
        super().__init__()
        self.real = LruCache(capacity=8)
        self.model = {}
        self.order = []

    @rule(k=st.text(min_size=1, max_size=4), v=st.integers())
    def put(self, k, v):
        self.real.put(k, v)
        if k in self.model:
            self.order.remove(k)
        self.model[k] = v
        self.order.append(k)
        while len(self.order) > 8:
            del self.model[self.order.pop(0)]

    @precondition(lambda self: self.model)
    @rule(data=st.data())
    def get_existing(self, data):
        k = data.draw(st.sampled_from(sorted(self.model)))
        assert self.real.get(k) == self.model[k]
        self.order.remove(k)
        self.order.append(k)          # a read is a use, for LRU purposes

    @invariant()
    def never_exceeds_capacity(self):
        assert self.real.size() <= 8

That machine finds the bugs that matter in a cache: an eviction that removes the wrong entry, a read that fails to update recency, an off-by-one at capacity, and a key whose collision behavior differs from the model.

Shrinking

  The reachable state space of a small concurrent queue.
  Each dot is a reachable state. X marks the states that violate
  the invariant.

  EXAMPLE TESTS                      PROPERTY TESTS
  . . . . . . . . . . . . .          o o . o . . o . o . . o .
  . . o . . . . . . . . . .          . o . o o . . o . o o . .
  . . . . . . X . . . . . .          o . . o . . X . o . . o .
  . . o . . . . . . . . . .          . o o . o . . o . . o o .
  . . . . . . . . . X . . .          o . . o . . o . . X . . o
  12 states, chosen by the author    ~180 states, chosen by a generator
  found: 0 of 2 bad states           found: 2 of 2, this run

  MODEL CHECKING                     FUZZING (a different axis)
  # # # # # # # # # # # # #          explores the INPUT space, not the
  # # # # # # # # # # # # #          state space, at millions of
  # # # # # # X # # # # # #          samples per hour, looking for a
  # # # # # # # # # # # # #          crash rather than a wrong answer
  # # # # # # # # # X # # #
  every reachable state, within
  the bound. found: 2 of 2, always

  Property testing samples widely and gives no guarantee. Model
  checking is exhaustive within a bound and costs a specification.
  The two find the same bugs at very different prices, which is why
  the bound matters: a protocol checked at 3 nodes and 2 messages
  says nothing about 5 nodes and 4 messages.

Shrinking is what makes the technique usable rather than merely effective. When a property fails, the framework does not report the 400-element list of random integers that broke it. It searches for the smallest input that still fails.

The algorithm tries structurally simpler candidates repeatedly: shorter lists, smaller numbers, earlier characters, fewer operations. It keeps any candidate that still fails and continues. The result is usually two or three elements, and the cause is often visible immediately.

Two practices keep shrinking effective. Write generators that shrink well, which means building them from the library's primitives rather than from raw random draws, because the library knows how to simplify its own structures. And always record the failing seed and add the minimized case as a permanent example-based test, so that the same bug can never return silently.

6.2 Continuous Fault Injection and Fuzzing

Property testing explores the input space with structure. Fuzzing explores it without structure, at enormous volume, looking for a crash rather than a wrong answer.

Coverage-guided fuzzing

A naive fuzzer generates random bytes and almost never gets past a length check. A coverage-guided fuzzer instruments the target, keeps any input that reaches a new code path, and mutates the interesting ones. That feedback loop is the entire idea, and it turns an impossible search into a tractable one.

The loop runs continuously: pick an input from the corpus, mutate it, run the target, and if the coverage bitmap has a new entry, add the mutated input to the corpus. Over hours the corpus evolves into a set of inputs that collectively exercise most of the reachable code.

Sanitizers are what turn a silent bug into a crash the fuzzer can detect. An address sanitizer catches out-of-bounds access and use after free. A memory sanitizer catches uninitialized reads. An undefined behavior sanitizer catches signed overflow and misaligned access. Without them a fuzzer finds only the bugs that happen to segfault, which is a small fraction of the memory safety bugs present.

/* A libFuzzer target. Three properties make it effective:
   it is fast, it is deterministic, and it exercises a real parser
   rather than a wrapper. */
#include <stdint.h>
#include <stddef.h>

int LLVMFuzzerTestOneInput(const uint8_t *data, size_t size) {
    if (size < 4 || size > 65536)
        return -1;                 /* -1 tells the fuzzer not to keep it */

    struct config *cfg = config_parse(data, size);
    if (cfg) {
        /* Exercise the round trip too: a serializer bug is as real
           as a parser bug, and this costs almost nothing. */
        uint8_t buf[65536];
        size_t n = config_serialize(cfg, buf, sizeof(buf));
        struct config *again = config_parse(buf, n);
        config_free(again);
        config_free(cfg);
    }
    return 0;
}

Kernel and system fuzzing

Fuzzing a system call interface needs a different approach, because the input is a sequence of structured calls rather than a byte buffer, and because the target cannot be restarted in microseconds.

The established design uses templates that describe each system call's arguments and the relationships between them, so that a generated file descriptor from one call is used by a later call. Coverage feedback from the kernel guides the search, and the whole thing runs against virtual machines that are reset when they crash. That is the shape of syzkaller, which has found thousands of Linux kernel bugs.

The newer direction uses language models to generate the templates and the harnesses, which is the part that previously required a human with deep knowledge of the target. Reported work extends existing kernel fuzzers this way, and the equivalent for user-space projects generates fuzz harnesses automatically for code bases that never had one. The honest framing is that this is an amplifier rather than a replacement: it expands coverage into projects that lacked the human hours, and the coverage feedback loop remains what finds the bugs.

Continuous fault injection

Fuzzing attacks the input. Fault injection attacks the environment, and it tests the code that only runs when something goes wrong, which is the code that is never exercised and therefore never correct.

The targets are the ones a normal test never reaches. An allocation returns null. A write returns a partial count. A read returns fewer bytes than requested. A system call returns an interrupted-call error. A disk reports a write error, and a network call times out.

Deterministic simulation is the strongest form, and Volume II describes it. Run the whole system in one process with a simulated clock, a simulated network, and a seeded random number generator that decides every injected fault. A failing seed reproduces the bug exactly, every time, which turns an unreproducible failure into an ordinary one.

The table has no redundancy in it. Each row finds a class the rows above do not, which is why a mature code base runs several of them rather than choosing one.

6.3 Automated Continuous Regression Prevention

Correctness regressions are caught by tests. Performance regressions are not, because no test asserts that a function is still fast. They arrive one percent at a time and are noticed a year later, when the aggregate is 40 percent and the cause is untraceable.

Making a benchmark trustworthy

The obstacle is variance. A benchmark that varies by 10 percent between runs cannot detect a 3 percent regression, and cloud instances vary by more than that.

Five controls bring the variance down to where small regressions are visible. Pin the CPU frequency and disable turbo, because thermal behavior differs between runs. Pin the process to specific cores and isolate them from the scheduler. Run on bare metal or a dedicated instance rather than a shared one. Run enough iterations to reach a stable distribution, and report a percentile rather than a mean. And interleave the baseline and the candidate rather than running them in sequence, which removes any drift in machine conditions from the comparison.

Compare against the merge base rather than against a stored number. A stored baseline goes stale and encodes the conditions of the machine that produced it. Building both the base and the candidate in the same job, on the same machine, in an interleaved order, removes the largest sources of error at the cost of doubling the build.

Differential profiling

A benchmark says that something got slower. A differential profile says what.

Collect a profile for the baseline and the candidate under the same workload, fold both into the same stack format, and compute the difference per stack. The result is a differential flame graph where each frame is colored by whether it consumed more or less time, and the culprit is usually visible in seconds.

# Profile both revisions under an identical workload, then diff.
perf record -F 99 -g -- ./bench-base      && perf script \
  | stackcollapse-perf.pl > base.folded
perf record -F 99 -g -- ./bench-candidate && perf script \
  | stackcollapse-perf.pl > cand.folded

# Red frames grew, blue frames shrank, width is the magnitude.
difffolded.pl base.folded cand.folded | flamegraph.pl \
  --title "candidate vs base" > regression.svg

# The counters that name the mechanism rather than the location.
perf stat -e cycles,instructions,cache-misses,branch-misses \
          -r 10 -- ./bench-candidate

The hardware counters answer a different question from the profile, and the pair is what identifies the mechanism. Instructions up with instructions per cycle flat means more work was added. Instructions flat with instructions per cycle down means the same work became slower, which points at cache behavior, branch prediction, or contention. Cache misses up with instruction count flat means a data layout change, which is a common and non-obvious consequence of adding a field to a struct.

Isolating the commit

When a regression appears across a range of commits, bisection finds it. The mechanics are standard and the difficulty is the test.

A bisection test must be deterministic, or the search converges on a random commit. For a performance regression that means running enough iterations, using a percentile, and choosing a threshold well outside the noise band. Skip a commit that does not build rather than marking it bad, because a marked-bad build sends the search down the wrong half.

# The test script returns 0 for good and 1 for bad. It must be
# deterministic, or the search lands on an arbitrary commit.
cat > /tmp/bisect-perf.sh <<'SH'
#!/bin/bash
make -s build || exit 125          # 125 means "skip", not "bad"
p50=$(./bench --iterations 200 --report p50-ns)
# Threshold sits well outside the measured noise band.
[ "$p50" -lt 1450 ] && exit 0 || exit 1
SH
chmod +x /tmp/bisect-perf.sh

git bisect start HEAD v2026.02.0
git bisect run /tmp/bisect-perf.sh

Canary as the last line

A benchmark measures a synthetic workload on one machine. Production is a different workload on different hardware with a different data distribution, and some regressions appear only there.

A canary deployment carries the load. Volume II covers the mechanics, and the points specific to regression detection are three. Compare the canary against a concurrent baseline running the old version rather than against a threshold, because a platform-wide change moves both. Compare distributions rather than means, since a regression often shifts the tail while leaving the median alone. And exclude a warm-up window, because a cold cache, a JIT that has not compiled yet, and a connection pool that is still filling all make the first minutes unrepresentative.

6.4 Formal Verification Foundations

Testing samples the state space. For a sequential program the sample can be good. For a concurrent or distributed protocol it cannot, because the number of interleavings is astronomical and the bugs live in the rare ones.

Formal methods take a different approach. Describe the system as a mathematical object and prove properties over every reachable state, rather than sampling some of them.

Specification and model checking

TLA+ describes a system as a state machine: an initial predicate, a next-state relation, and a set of properties. The model checker explores every reachable state within specified bounds and reports a counterexample trace when a property fails.

The counterexample is the practical payoff. It is not "your system is wrong", it is a specific sequence of steps that reaches a bad state, which a human can read and reason about.

------------------------------ MODULE TwoPhase ------------------------------
EXTENDS Integers, FiniteSets
CONSTANT RM                          \* the set of resource managers

VARIABLES rmState, tmState, tmPrepared

TPInit == /\ rmState    = [r \in RM |-> "working"]
          /\ tmState    = "init"
          /\ tmPrepared = {}

Prepare(r) == /\ rmState[r] = "working"
              /\ rmState' = [rmState EXCEPT ![r] = "prepared"]
              /\ UNCHANGED <<tmState, tmPrepared>>

RcvPrepared(r) == /\ tmState = "init"
                  /\ rmState[r] = "prepared"
                  /\ tmPrepared' = tmPrepared \cup {r}
                  /\ UNCHANGED <<rmState, tmState>>

Commit == /\ tmState = "init"
          /\ tmPrepared = RM
          /\ tmState' = "committed"
          /\ UNCHANGED <<rmState, tmPrepared>>

Abort == /\ tmState = "init"
         /\ tmState' = "aborted"
         /\ UNCHANGED <<rmState, tmPrepared>>

\* SAFETY: no resource manager commits while another has aborted.
Consistent ==
  \A r1, r2 \in RM : ~ /\ rmState[r1] = "aborted"
                       /\ rmState[r2] = "committed"

\* LIVENESS: if every manager prepares, the transaction eventually
\* resolves. This is the property that fails when the coordinator
\* can crash, which is exactly the blocking behavior of 2PC.
Terminates == (\A r \in RM : rmState[r] = "prepared") ~> (tmState # "init")
=============================================================================

The distinction between the two properties at the bottom is the one worth carrying away. A safety property says that something bad never happens, and a counterexample is a finite trace. A liveness property says that something good eventually happens, and a counterexample is an infinite trace, usually a cycle where the system loops without progressing. Most engineers specify safety and forget liveness, and a system that is perfectly safe and never makes progress is a real and common failure.

Where it pays

Formal specification is expensive, and it pays in a narrow and identifiable set of places.

It pays on a protocol where a bug is catastrophic and hard to find by testing: consensus, replication, cache coherence, a distributed lock, a membership change. Amazon Web Services reported using it on S3, DynamoDB, and EBS and finding bugs that testing did not find, including one requiring 35 steps to reach. No test suite finds a 35-step interleaving by chance.

It pays on a lock-free data structure, where the linearization argument is subtle and the failure is silent corruption. Chapter 4 of Volume I describes the ABA problem and the reclamation schemes, and both are exactly the kind of thing that a model checker examines exhaustively and a test does not.

It pays at design time rather than after implementation. The specification is a tool for finding design errors before code exists, which is when they are cheapest to fix. Specifying a finished system finds fewer bugs and costs the same.

It does not pay on business logic, on user interfaces, or on anything whose correctness is a matter of judgment rather than of invariants.

The gap between specification and code

A model-checked specification proves the design. It says nothing about whether the implementation matches, and the gap is real.

Three techniques narrow it. Refinement mapping proves that the implementation's state machine refines the specification's, which is rigorous and expensive. Trace checking records production traces and checks them against the specification as a model, which catches divergence with modest effort. Model-based testing generates test cases from the specification, which transfers the exploration into the ordinary test suite.

Most teams get the majority of the value from the specification alone, because the design bugs are the expensive ones. A specification never connected to the code still paid for itself if it found one of them.

Lighter-weight formal methods

Full specification is not the only option, and several techniques give part of the benefit at a fraction of the cost.

A type system is a proof, and a stronger type system proves more. Making illegal states unrepresentable in the type, rather than checking for them at run time, eliminates a class of bug entirely.

Contracts state preconditions, postconditions, and invariants in the code. They are checked at run time in test builds and they document the intent precisely enough that a reader can reason about a function without reading its body.

Static analysis proves specific properties: no null dereference, no unchecked error return, no data race on a shared field. The Rust borrow checker is the most widely deployed example, and Section 9.1 covers what it proves.

Bounded model checking on a small critical function proves a property for all inputs up to a size bound, which is often enough for a parser or an arithmetic routine and needs no specification language.

Sources and further reading

John Hughes on QuickCheck and on property-based testing in practice. The Hypothesis documentation for stateful testing and for shrinking. Leslie Lamport, "Specifying Systems", and the TLA+ Video Course. Chris Newcombe and others, "How Amazon Web Services Uses Formal Methods", CACM 2015. The libFuzzer, AFL++, and OSS-Fuzz documentation, and the OSS-Fuzz research pages on language-model-generated fuzz targets. The syzkaller documentation for system call description templates. Brendan Gregg on differential flame graphs. The FoundationDB talks on deterministic simulation testing.