I choose tools that maximize signal: reproducible bugs, meaningful coverage, and verification of critical invariants.

If you are evaluating your options for distributed systems testing, here is how the landscape looks and where executable specs fit in.

Jepsen (chaos and fault injection). If you want someone to find bugs in a running system by injecting faults, Kyle Kingsbury's Jepsen is the gold standard (Kafka, Redis, MongoDB, etcd). Jepsen's hand-crafted tests tell you that something failed. A spec tells you what the correct behavior should have been. Most teams benefit from both.

Antithesis (deterministic simulation testing). Deterministic simulation as a service, well-funded and gaining traction with exactly the same buyers. It helps you reproduce failures reliably. It does not tell you what correct looks like, and complex properties are hard to express.

Property-based testing. Hypothesis, fast-check. The right starting point at the unit level, and the lowest-friction option if your system is not yet distributed. Does not compose naturally across nodes or network failures.

TLA+ and classical formal methods. TLC, Apalache, Lean. The highest-expressiveness option. Most teams will not invest in learning TLA+ without tooling that lowers the barrier significantly. My work sits on top of this toolchain and makes it accessible without requiring your team to become TLA+ experts.

FizzBee. Python-like MBT targeting distributed systems teams. Worth looking at if Python syntax is a hard requirement. Uses a bespoke language without TLA+ semantics, so you lose interop with tools like Apalache or TLC.

Quint. Modern TypeScript-like syntax over TLA+ semantics, from Informal Systems. I was part of the original dev team. Strong theoretical foundation, but the toolchain is still maturing and there is no native test generation. A solid choice if staying close to TLA+ semantics matters and you have the patience to work around rough edges.

Formal verification consulting. Certora, Runtime Verification, Galois, Informal Systems. Right for high-assurance systems where you need full proof. High-touch and expensive. My engagements are faster, more targeted, and leave your team with tools they can continue using.

In-house simulation (TigerBeetle, FoundationDB). If your team has already built a simulation layer, you are ahead of most. I can help you get more out of what you have built by pairing it with a specification-based oracle.