How Resonate is tested

Testing approach across the Resonate server, each SDK, and the Lean 4 executable specification.

Resonate's correctness story rests on three foundations that reinforce each other: an executable formal specification of the protocol in Lean 4, differential random testing of the server implementation against a pure in-memory reference model, and deterministic simulation testing of the TypeScript SDK. Unit, integration, and end-to-end test suites across all five SDKs sit alongside these.

The Lean 4 abstract machine#

The Distributed Async Await protocol 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 core 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 Lean model encodes each protocol handler as a pure, deterministic, total function:

-- every handler has this shape:
-- M = StateM ServerState, so "now" is the only input that carries time
def promiseCreate (req : PromiseCreateReq) (now : Nat) : M PromiseCreateRes

State is touched only through named atomic effects — getPromise / setPromise, getTask / setTask, getSchedule / setSchedule / delSchedule, timeout management, and outbox writes. Handlers compose these effects and nothing else, which makes the model directly auditable and buildable with a single command:

cd spec && lake build

The model currently covers twenty handlers in full: five promise handlers (create, get, settle, register_callback, register_listener), ten task handlers (get, create, acquire, fence, heartbeat, suspend, fulfill, release, halt, continue), three schedule handlers (get, create, delete), and the two internal transitions (resume, timeouts). The three search handlers return a placeholder 501 response while their specs are being written.

The model also states the protocol's central safety property — the durable-execution guarantee — as an executable predicate, in spec/02-actions/04-guarantee.lean:

def durableExecutionGuarantee (s : ServerState) : Bool :=
  s.tasks.all (fun t =>
    match t.state with
    | .pending | .acquired | .halted | .fulfilled =>
      true
    | .suspended =>
      match s.promises.find? (·.id == t.id) with
      | none => true
      | some tP =>
        if tP.state != .pending || tP.timeoutAt <= tP.createdAt then
          true
        else
          let awaitedIds := t.resumes
          let anySettled := s.promises.any (fun p =>
            awaitedIds.contains p.id && awaitedSettledLive p tP)
          if !anySettled then
            true
          else
            hasExecuteInOutbox t.id s.outbox)

In words: if a task has suspended on awaited promises, and one of those promises settles while the task's own promise is still pending and unexpired, an execute message must be queued. The same file checks the predicate against concrete scenarios; a general theorem over all reachable states is not yet proven, and the file says so.

Having the protocol in two representations is the point: the Lean model is the definition the compiler checks, and the prose specification explains the same rules for human readers. Anyone can audit one against the other.

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 the same randomly-generated sequence of API operations through multiple backends at once — always an in-memory SQLite instance and an in-memory Oracle reference model; optionally Postgres and MySQL when environment variables supply connection URLs. After every operation the test asserts two things: that every backend returned the same HTTP status and response body, and that the complete server state (promises, tasks, messages, timeouts) matches across all backends.

The Oracle is a pure Rust in-memory implementation of the protocol state machine, derived from the same handler rules encoded in the Lean 4 model. A disagreement between the Oracle and any concrete storage backend is an immediate test failure, with a precise field-level diff showing the divergence.

Coverage is enforced: the test runs until all twenty-two operation kinds in the API have each produced at least one 2xx response, then continues until no new operation signatures appear for twenty consecutive batches of two hundred steps. CI runs this against all three storage backends — SQLite, Postgres, and MySQL — as a matrix on every pull request.

To run it 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 conformance testbed is checked out and run in the server's CI matrix on every pull request (visible in ci.yml): state-machine transition tests, randomized fuzz runs, 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 goes inactive. Configurable probabilities — dropProb, duplProb, randomDelay, deactivateProb, activateProb — default to values drawn from the same PRNG so the entire run is reproducible from the seed alone.

A default run executes 10,000 steps. Three simulated worker processes and one simulated server process receive and process messages inside the harness, exercising recursive fan-out patterns (Fibonacci with local and remote calls) and multi-step chained functions.

Determinism is verified explicitly: CI runs each seed twice and diffs the two log files. Different output from the same seed is a failing run. 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, filed by the harness with the seed, commit, and command included:

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 (R1), that settled promise records never retreat to pending (R2), 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. 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.