How Resonate is tested

How Resonate is tested — an executable Lean 4 specification checked at build time, differential random testing of the server against an independent oracle, and deterministic simulation testing (DST) of the TypeScript SDK.

Resonate's correctness story rests on three layers, each covering a different surface: an executable formal specification of the protocol in Lean 4, differential random testing of the server against an independent in-memory oracle, and deterministic simulation testing of the TypeScript SDK. Unit, integration, and end-to-end suites across all five SDKs sit alongside these. Deterministic simulation currently covers the TypeScript SDK; the other SDKs are tested conventionally, against a live server.

Determinism is a protocol feature#

Resonate's determinism hooks live in the protocol itself, not in a simulator wrapped around the code under test.

When the server runs with debug = true in its config, every request envelope may carry a resonate:debug_time field, and the handler uses that value as "now" instead of the wall clock (src/util.rs, src/server.rs). Handlers take time as a parameter rather than reading an ambient clock, so a test controls every time value the handler path observes — timers, timeouts, and schedules fire exactly when the test drives them to. With debug = false (the default), the field is stripped and the server runs on wall-clock time.

Deterministic tests therefore run against the real server binary, over its real HTTP interface, with no separate simulator build to keep in sync with production code. And because the hook is part of the protocol rather than any one codebase, a harness built on it can drive any server that implements the protocol — the conformance testbed below leans on exactly this.

The Lean 4 abstract machine#

The Distributed Async Await protocol — the protocol every Resonate server and SDK speaks — is specified twice, on purpose. resonatehq/resonate-specification is the executable abstract machine in Lean 4 — the normative, machine-checkable definition of the protocol's handlers and state transitions: promises, tasks, and schedules. The prose specification is the human-readable companion that explains the same protocol. Where prose and Lean disagree, the Lean model wins.

The model encodes each protocol handler as a pure, deterministic function:

-- every handler has this shape: "now" is the only input that carries time
def promiseCreate (req : PromiseCreateReq) (now : Nat) : H PromiseCreateRes := do
  ...

Handlers read state and emit named effects — setPromise, setTask, setSchedule, outbox writes — and nothing else, which keeps the model directly auditable (spec/02-abstract). It builds with a single command:

lake build spec    # the specification — the fast loop
lake build valid   # the trace checker
lake build         # everything, including the decide sweeps (minutes)

The model specifies 18 of the 21 handlers a client can reach in full: five promise handlers (promiseCreate, promiseGet, promiseSettle, promiseRegisterCallback, promiseRegisterListener), ten task handlers (taskGet, taskCreate, taskAcquire, taskFence, taskHeartbeat, taskSuspend, taskFulfill, taskRelease, taskHalt, taskContinue), and three schedule handlers (scheduleGet, scheduleCreate, scheduleDelete). The three search handlers are stubbed at 501 while their specs are being written. Alongside these sit six internal steps — the transitions background jobs fire: promise timeout, listener drain, callback drain, lease timeout, retry dispatch, and schedule firing (spec/02-abstract/internal.lean).

The property catalogue#

The model carries a catalogue of 95 decidable properties — invariants over server state, stated as executable predicates in spec/02-abstract/properties.lean. They're checked two ways.

First, by exhaustive sweep: spec/04-theorems/properties-check.lean evaluates the full catalogue over every script of length up to three drawn from an eleven-step adversarial alphabet — 1,464 scripts in total — and the sweep is a theorem proved by decide, meaning Lean's kernel runs the entire check during lake build. A green build is the certificate; there's no separate test run to forget. What the sweep certifies is bounded — every behavior reachable in three steps; beyond that it says nothing — which is why the catalogue is checked a second way.

Second, by proof: 32 of the 95 properties are proved as theorems that hold along all reachable traces, at any depth (spec/04-theorems/holds.lean). The remaining 63 are backed by the sweep alone so far, and the file says so.

The protocol's central liveness property — settle a promise, and its awaiters come back — is stated in spec/04-theorems/liveness.lean:

def EventuallyAwaiterResumed : Prop :=
  ∀ tr : Trace, Valid true tr → ClockAdvances tr →
    WeaklyFairOn tr isSettlementStep → WeaklyFairOn tr isCallbackStep →
    ∀ (t : Nat) (a x : String),
      (∃ p, promiseAt (tr t).state a = some p ∧
              p.state ≠ .pending ∧ p.callbacks.contains x = true) →
      ∃ u : Nat, t ≤ u ∧
        (∀ p, promiseAt (tr u).state a = some p → p.callbacks.contains x = false) ∧
        (∀ w, taskAt (tr u).state x = some w →
           w.state = .fulfilled ∨ (w.state ≠ .suspended ∧ w.resumes.contains a = true))

In words: on any valid trace where the clock keeps advancing and the settlement and callback steps are treated fairly, once a promise settles, every task awaiting it is eventually resumed — or the task's own timeout won the race first, in which case the timeout path owns the cleanup. The statement quantifies over infinite traces, so it can't be proved by enumeration; what the repo proves instead are its bounded shadows — boundedWakeSweep checks the wake obligation over the full 1,464-script corpus, and a companion theorem, wake_requires_fairness, shows the fairness assumptions aren't decorative: drop them and the obligation genuinely fails.

Holding real servers to the model#

The spec repo also ships a trace checker, valid/: capture real traffic from a running server as newline-delimited JSON, one event per external call, and ask whether the abstract machine can account for it. Two implementations answer that question — valid/lean, which searches for an accepting run of the Lean machine, and valid/porc, a Go port of the same machine wired into the Porcupine linearizability checker. They're ports of one model, so agreement between them catches drift and translation errors; a regression test pins the exact event at which both checkers refute a known-bad capture. Conformance here is an instrument, not a per-build gate: a server is held to the model when its traffic is captured and run through the checker.

Resonate Server#

The Resonate Server (resonatehq/resonate, written in Rust) is tested in several layers on every pull request.

Differential random testing#

diff/differential.rs defines a test named differential_random. It drives one randomly-generated sequence of API operations through multiple backends at once — always an in-memory SQLite instance and the Oracle reference model; Postgres and MySQL too, when environment variables supply connection URLs. Every operation must produce the same HTTP status and response body from every backend. State is cross-checked as well: narrower checks around each operation, and a comparison of the full snapshot — promises, tasks, callbacks, listeners, messages, timeouts — at every 200-step batch boundary. The test is sequential, one operation at a time; concurrent histories are the linearizability checker's job below.

The Oracle (src/oracle.rs) is a second, independent, in-memory implementation of the protocol state machine, written separately from the storage backends rather than derived from them. When implementations that share only the protocol agree on every response and every snapshot, agreement is evidence; a disagreement is an immediate test failure with a field-level diff of the divergence.

Generation is steered: uncovered operations are forced first, and the run ends only after all twenty-two operation kinds are covered and twenty consecutive 200-step batches produce no new (operation, status, state-shape) combination — a stopping heuristic over the protocol surface, not a code-coverage measure — capped at 200,000 steps. In CI the test runs on every pull request as part of cargo test --all-features, against SQLite and the Oracle; the Postgres and MySQL backends are exercised locally:

# SQLite + Oracle only (no external database required):
cargo test --test differential -- --nocapture

# All backends:
TEST_POSTGRES_URL=postgres://<USER>:<PASSWORD>@localhost:5432/resonate \
TEST_MYSQL_URL=mysql://<USER>:<PASSWORD>@localhost:3306/resonate \
  cargo test --test differential -- --nocapture

Unit tests#

The server's unit tests run with cargo test --all-features and cover configuration parsing, transport message handling, and individual processing modules. CI gates every pull request on format (cargo fmt), compilation (cargo check), and linting (cargo clippy --all-features -- -D warnings) before tests run.

Conformance and linearizability#

A separate CI job (visible in ci.yml) runs the conformance testbed against the server on every pull request, as a matrix over all three storage backends — SQLite, Postgres, and MySQL. The testbed drives the server over HTTP: state-machine transition tests, randomized fuzz runs against a reference model, and linearizability checking of concurrent operation histories with Porcupine. The testbed itself is not yet public — the CI steps that fetch and run it are.

TypeScript SDK#

The TypeScript SDK (resonatehq/resonate-sdk-ts) carries a conventional Jest test suite and a dedicated deterministic simulation test.

Deterministic simulation testing#

The DST harness lives in sim/ and runs on a schedule via .github/workflows/dst.yml — every twenty minutes, across Ubuntu, Windows, and macOS, against Node 18, 20, and 22.

The harness uses a seeded linear-congruential PRNG. From a single integer seed, it derives the full behavior of the run: which function to invoke at each step, whether a message is dropped, duplicated, or delayed, and whether a worker process drops out and comes back. A default run executes 10,000 steps across three simulated worker processes and one simulated server process, exercising recursive fan-out patterns and multi-step chained functions. The simulation wraps the SDK's real core logic in a simulated network: the code under test is the code you'd ship. The transport standing in for the network is not — transport-level bugs are the end-to-end suites' job.

Determinism is verified explicitly: CI runs each seed twice and diffs the two logs. Same seed, different output is a failing run — a check that exists to catch nondeterminism itself, the one bug class that would quietly destroy the reproducibility everything else depends on. When a run fails, a GitHub issue is filed automatically with the seed, the commit SHA, and the exact command to reproduce it — issue #414 is one such report:

npm run dst -- --seed <seed> --steps 10000

Jest unit and integration suite#

The Jest suite covers the core execution engine, coroutine scheduling, retry policies, network transport, codec, encryption, and function registry. It runs via npm test in CI alongside linting and type checks.

Python SDK#

The Python SDK (resonatehq/resonate-sdk-py) runs pytest with branch coverage on Python 3.12, 3.13, and 3.14 across Ubuntu, macOS, and Windows.

The suite includes tests/test_invariants.py, which formalizes the structural replay contract of the SDK's execution tree model. The invariants capture properties from the internal tree.md specification — among them that a node's settler type is fixed across replays, that settled promise records never retreat to pending, that the execution tree reaches a fixed point after the first replay under an unchanged cache, and that the frontier shrinks monotonically as steps settle. Each invariant is driven across a battery of workflow shapes, and the test asserts the property at every step of the settle-to-done trajectory rather than only at the final state.

CI also runs the Python SDK's examples end-to-end against a live Resonate server binary, downloaded from the public release page.

Rust SDK#

The Rust SDK (resonatehq/resonate-sdk-rs) runs cargo test --workspace for its unit suite and cargo test -p resonate-sdk --test e2e for end-to-end tests against a live server. The e2e suite runs in CI against a server container on every pull request and covers durable function execution, fan-out/fan-in, promise resolution, retry behavior, and heartbeating.

Go SDK#

The Go SDK (resonatehq/resonate-sdk-go) runs go test -race -timeout 5m ./... — the Go race detector is enabled on every test run. End-to-end tests in e2e_test.go target a live Resonate server and cover the full execution lifecycle: durable sleep, fan-out, promise resolution, and load balancing across worker groups. Without RESONATE_URL set, the e2e tests skip cleanly so go test ./... works without a server.

Java SDK#

The Java SDK (resonatehq/resonate-sdk-java) compiles against Java 21 and runs its test suite against Java 21, 24, and 25 via ./gradlew test. The suite includes InvariantsTest.java, a port of the Python SDK's replay-invariant suite — the same structural contract, checked in a second language. CI also runs the SDK's examples end-to-end against a live server.

Where to go next#

To see the system these tests protect, the quickstart gets a durable function running in a few minutes. Questions about the testing approach are welcome in Discord.