# Executable specifications 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+](https://lamport.azurewebsites.net/tla/tla.html). 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](https://lamport.azurewebsites.net/tla/pluscal.html)** — TLA+'s pseudocode dialect; compiles to TLA+. Useful as a bridge between executable specs and full [model checking](https://quality.stereobooster.com/model-checking.md). - **[Alloy](https://alloytools.org/)** — finite model finder; it explores the spec's properties interactively. - **[P](https://github.com/p-org/P)** (Microsoft) — async-distributed-system DSL; the spec is executable in a simulator. ### PBT frameworks as runners - **[Hypothesis](https://hypothesis.readthedocs.io/)** (Python), **[fast-check](https://fast-check.dev/)** (TypeScript), **[proptest](https://github.com/proptest-rs/proptest)** (Rust), **[QuickCheck](https://hackage.haskell.org/package/QuickCheck)** (Haskell/Erlang). The PBT framework generates inputs; the assertion `impl(x) == spec(x)` is the entire test. - See [property-based testing](https://quality.stereobooster.com/property-based-testing.md) 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)[^brooker2024]. - **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)[^bornholt2021]. ## 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](https://quality.stereobooster.com/equivalence-checking.md) — *prove* they agree on every input. - [Differential testing](https://quality.stereobooster.com/differential-testing.md) — *test* them on sampled inputs before release. - [Parallel run](https://quality.stereobooster.com/parallel-run.md) — *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](https://quality.stereobooster.com/contracts-as-specifications.md) · Methods - [Formal methods](https://quality.stereobooster.com/formal.md) · Methods - [Model checking](https://quality.stereobooster.com/model-checking.md) · Methods - [Requirements quality checking](https://quality.stereobooster.com/requirements-quality-checking.md) · Methods - [How AI fits into software quality](https://quality.stereobooster.com/ai.md) · AI ## References [^brooker2024]: Brooker, Marc, and Ankush Desai. 2024. "[Systems Correctness Practices at Amazon Web Services](https://cacm.acm.org/practice/systems-correctness-practices-at-amazon-web-services/)." *Communications of the ACM*, ahead of print. . [^bornholt2021]: Bornholt, James, Rajeev Joshi, Vytautas Astrauskas, et al. 2021. "[Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3](https://www.cs.utexas.edu/~bornholt/papers/shardstore-sosp21.pdf)." *Proceedings of the 28th ACM Symposium on Operating Systems Principles (SOSP '21)*, 836–50. . ## Acronyms - DSL — domain-specific language - FM — formal methods - PBT — property-based testing