Five verification methods
Proving It Correct — Theory Plus Experiment
Neither alone is enough: pair a proof with a fault.
Formal proof
math on paper
writes the algorithm
as math, proves the
property holds
limit:
misses the real
code entirely
finds hidden timing
assumptions early
Model checking
TLA+, FizzBee
explores every state
of the model,
systematically
limit:
state space is infinite:
bound it, approximate
used by CockroachDB,
Kafka, and friends
Fault injection
Chaos, Jepsen
kills real nodes,
cuts real networks,
drops real disks
limit:
hard to write well;
no fine control
found many critical
production bugs
Simulation (DST)
FoundationDB style
mocks net, disk, clock;
replays the exact
event order
limit:
must control every
nondeterminism source
every failure repeats
bit-for-bit
Fuzz, property
random inputs
throws random inputs
at forgotten corners;
checks properties
limit:
no guarantees;
a complement only
pairs well with DST
and model checking
Determinism is the thread: replayable logs, durable workflows, simulated time.
Control every nondeterminism source — even hash iteration order.