Known methods

Correctness is an old problem with a deep toolbox. Long before durable execution existed, people built ways to say what “correct” means and to check that a system meets it — model checkers, type systems, proof assistants, simulation testers, whole design disciplines that make bugs impossible instead of merely rare.

Durable-execution workflows don’t get a new toolbox. They inherit this one. The value is in knowing which tools reach which problems — and where the gap still is. This page maps that landscape: the vocabulary to reason about correctness and the families of approaches SpecCraft draws from. (For the problems these approaches target, see The problems.)

The anatomy of a solution

Every approach to correctness is some arrangement of three things. Naming them cleanly is what lets you compare tools that otherwise look nothing alike.

Implementation

The code — the actual Temporal workflow and activities. The concrete system, and usually the only place the intended behavior is really written down.

Spec

What “correct” means — invariants, temporal-logic properties, pre/post-conditions, a reference oracle. It doesn’t run; it judges.

Model

An abstract, executable stand-in for the system — a state machine you can explore exhaustively. Small enough to check, faithful enough to trust.

The relationships are the whole game:

   Model ──────checked against──────▶ Spec   ◀── the judge
     ▲    ╲                            ▲
     │     ╲                           │
 abstracted  trace                 checked
 from code   validation            against
     │          ╲                     │
   Implementation ────────────────────┘

A check is always one artifact measured against the spec. You can check the model against the spec (cheap to explore, but it’s not your real code), or check the implementation against the spec directly (real, but harder to explore exhaustively). Any artifact can be hand-authored, extracted from code, or LLM-generated — and that authoring cost, not the checking, is usually what makes correctness expensive. Two families (TLA+, Quint) even collapse spec and model into one language.

The families of approaches

1. Verify the model

Build an abstract model and check it against the spec by exploring every reachable state. Model checking — TLA+/PlusCal, Quint + Apalache, P, stateright. Exhaustive within bounds, which is its strength and its ceiling: you pay by hand-building a faithful model, and only bounded instances are checkable.

2. Verify the implementation

Check the real code against the spec — no separate model to maintain.

• Dynamically — run the code. Interleaving exploration (Coyote, Shuttle, Loom), deterministic simulation testing (Antithesis, FoundationDB-style), fault and consistency testing (Jepsen/Elle). Finds real races reproducibly, but samples orderings rather than proving their absence.
• Statically — analyze without running. Race detectors and linters (Infer/RacerD, CodeQL, Semgrep), symbolic execution (KLEE, CBMC), abstract interpretation (Astrée, Frama-C), type-based checks (session types, typestate).

3. Trace validation — the bridge

Instrument the real code to emit spec-shaped traces, then check each trace conforms to the spec. This is the industrially-proven way to connect a checked model to the code that actually runs — it closes the model-vs-code gap. Coverage-bound (only observed runs), so it pairs with model checking rather than replacing it.

4. Deductive verification

Prove the code or model meets the spec — discharge proof obligations with an SMT solver and interactive proof, instead of searching states or running the system. Unbounded guarantees, at the cost of heavy manual annotation. Dafny, Verus, F*, Why3 for code; Coq, Isabelle/HOL, TLAPS for models.

5. Prevent by design

The separate family: don’t verify — make the hazard class unrepresentable by construction, so there’s nothing to check.

• Non-reentrancy / serialization — mutexes, runExclusive, queue-and-process-one.
• Order-insensitivity — idempotent/commutative operations, CRDTs.
• Statecharts — XState, eliminating invalid state combinations.
• Structured concurrency — no leaked or orphaned tasks.
• Single-writer entities — virtual actors, entity-per-key.
• Workflow nets — decidable soundness (no deadlock, orphan, or improper completion).
• Declarative models — AWS Step Functions, where free-form shared-state races simply aren’t expressible.

Families 1–4 judge a design after it exists; family 5 removes the hazard up front. They compose: prevention dissolves the intra-workflow classes cheaply, and verification handles the residual it can’t reach.