An executable specification is a second implementation that exists to be run — typically slow, obvious, and short. Sometimes it lives in the source language as a reference function; sometimes in a spec language like PlusCal or TLA+. Its job is to be the oracle the optimized implementation is checked against.

What it catches

• Optimization regressions. An optimization that changes behavior on a tested input shows up as a disagreement with the slow reference.
• Spec ambiguity at design time. Writing the obvious version forces the cases the optimized version would resolve by accident — null inputs, edge boundaries, what happens at limits.
• Cross-version drift. A new release that diverges from the previous one on recorded traffic; the previous version is the spec for the new one.
• Contract gaps for API design. An executable spec for the API forces decisions the documentation would otherwise leave to the implementation: error semantics, ordering, idempotence, pagination edges.
• Communication. Engineers, product, and ops can read 30 lines of Python that is the spec where they cannot read 3,000 lines of optimized code that implements it.

Executable specs do not catch bugs in the spec itself. A diff against the spec proves the implementation matches the spec — never that the spec matches the requirement. Example tests of the spec's known cases catch that, as does model-checking it against separately-stated properties.

What an authored oracle adds

A found oracle (GCC, Postgres) is a strong reference but an opaque one, and it cannot be handed to a prover. The author can keep the spec small and clean enough to model-check in TLA+ or Alloy, or to prove invariants about, and then reuse the same artifact unchanged as the diff oracle. That is why the technique sits in the formal-methods family: one simple spec bridges proving a property and checking the fast path against it at runtime.

Tools

Write the spec in the source language

• The recommended baseline. A Python function is the specification, and a property test asserts that the faster production implementation agrees with it.

Spec languages with executable semantics

• PlusCal — TLA+'s pseudocode dialect; compiles to TLA+. Useful as a bridge between executable specs and full model checking.
• Alloy — finite model finder; it explores the spec's properties interactively.
• P (Microsoft) — async-distributed-system DSL; the spec is executable in a simulator.

PBT frameworks as runners

• Hypothesis (Python), fast-check (TypeScript), proptest (Rust), QuickCheck (Haskell/Erlang). The PBT framework generates inputs; the assertion impl(x) == spec(x) is the entire test.
• See property-based testing for the wider technique.

When to use, when not

Use:

• When optimizing a function whose correctness is non-obvious from the optimized code.
• When porting code across languages or rewriting it. The original is the spec; the new one matches.
• When the system spans services and the contract matters more than the implementation. Executable specs become the source of truth.
• For algorithm-heavy code where the spec is much shorter than the implementation — compilers, planners, schedulers, solvers.

Don't:

• For features where the spec and the implementation are essentially the same. The duplication earns nothing.
• As a substitute for testing the spec itself. The spec can be wrong; pair with example tests of known cases.
• When the spec is computationally infeasible at the input scale that PBT explores. Constraining the input space is one option, and accepting a Heuristic guarantee is the other.

Evidence

• AWS practice. Property-based testing against developer-provided correctness specifications is one of the lightweight methods AWS adopted to bring formal methods closer to its engineering teams (Brooker and Desai 2024)¹.
• ShardStore. Reference models under property-based testing, with stateless model checking for the concurrency cases, caught sixteen production-bound bugs in the S3 storage-node code (Bornholt et al. 2021)².

Related

Differential oracle

These all answer the same question — does the candidate match a trusted reference? — and differ in how rigorously you compare, and in what the reference is. By rigour:

• Equivalence checking — prove they agree on every input.
• Differential testing — test them on sampled inputs before release.
• Parallel run — observe them side by side on live production traffic.

The reference itself varies too: a trusted implementation (a peer, the previous version, a gold-standard library), or a deliberately simple executable spec authored to be the reference.

Classification

• Quality dimensions: Functionality.
• Area: Algorithm optimization (slow obvious → fast optimized), executable API and policy contracts, reference implementations, cross-version regression gates, AWS-style lightweight FM at fleet scale.
• Guarantee: Empirical — a property test compares spec and implementation across many generated inputs.

Referenced by

• Contracts as specifications · Methods
• Formal methods · Methods
• Model checking · Methods
• Requirements quality checking · Methods
• How AI fits into software quality · AI

References

---

1. Brooker, Marc, and Ankush Desai. 2024. "Systems Correctness Practices at Amazon Web Services." Communications of the ACM, ahead of print. https://doi.org/10.1145/3729175. ↩

2. Bornholt, James, Rajeev Joshi, Vytautas Astrauskas, et al. 2021. "Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3." Proceedings of the 28th ACM Symposium on Operating Systems Principles (SOSP '21), 836–50. https://doi.org/10.1145/3477132.3483540. ↩