What are executable specifications?

Why this matters

Executable specs help when the risk lives in behavior of the system:
ordering, retries, stale reads, crashes, partial failure, and recovery paths.

1. 01

   Rare paths cause real incidents

   Production failures often happen on paths nobody wrote tests for:
   message interleavings, retries, timeouts, stale reads, crashes, and partial failures.

2. 02

   AI-generated changes need a reference

   AI can produce stateful code faster than reviewers can prove the behavior is intact.
   A runnable spec gives humans and agents expected behavior to test against.

3. 03

   Reviews need runnable evidence

   Important “must never happen” rules become checks you can rerun before a launch, migration, audit, or external review.

Example: a DNS balancer control plane

This example models a DNS load balancer control plane with garbage collection of stale DNS plans.
The full model has several actions; this snippet shows just one of them.

In this kind of system, bugs often come from a sequence of valid actions that creates an invalid state: an old plan is deleted too early, a retry observes stale data, or a recovery path leaves the root DNS record pointing somewhere it should not.

The spec models those actions at the level where the bug can appear, then checks the rule the system must always preserve.

@action(inline=False)
def deployer_gc(c: Context[DnsBalancerState], deployer: Annotated[Expr, str]):
    """Deployer cleans up old plans."""
    s = c.state
    next_plan = s.deployer_next_plan[deployer]
    old_indices = s.planner_updates.keys.filter(
        lambda i: next_plan > i + s.MAX_PLAN_AGE
    )
    old_plan_entries = Set(
        s.planner_updates[i].creates for i in old_indices
    ).flattened

    # avoid unrealistic no-op cleanups
    c.assume(~(old_plan_entries & s.zone_records).is_empty)

    # implementation may do this in a loop;
    # the spec models the abstract effect
    s.zone_records -= old_plan_entries


@invariant
def no_inconsistent_root(s: DnsBalancerState):
    """Root must always point to an existing plan."""
    cnames = SetIf(r.kind == CNAME for r in s.zone_records)
    plans = Set(r.value[0] for r in SetIf(r2.name == ZONE for r2 in cnames))
    return ~((plans & Set(r.name for r in cnames)).is_empty) & (plans.size == 1)

What is in an executable spec?

An executable spec is a code-level reference for the behavior you care about. It captures the parts that decide whether the system behaved as expected.

1. 01

   State

   The information that matters for the behavior under test: plans, versions, balances, leaders, locks, queues, records, or pending work.

2. 02

   Actions

   The operations that can change that state: requests, retries, failovers, reconciliations, commits, rollbacks, timeouts, or background jobs.

3. 03

   Failures and observations

   The messy parts that ordinary examples tend to skip: stale reads, delayed messages, duplicate requests, crashes, partial failure, and recovery.

4. 04

   System invariants

   The rules that must keep holding after every generated scenario. These become executable checks, not comments in a design doc.

How Much Do You Model?

An executable spec is not a second implementation of the whole system. It leaves out details that do not affect the behavior under review.

It is also not a static design document. The spec runs: it can generate scenarios, check invariants, produce counterexamples, and provide expected behavior for tests or review.

One executable model, four uses

Who This Is For

Book a 30-minute fit call