Resonate: durable execution built on a formal specification in Lean 4

Durable functions that persist their own results

Resonate is described as a durable execution platform and a durable execution factory, built on an open, formal specification of distributed async await. The concrete API is small enough to grasp in one sitting. A durable function receives a context and its inputs, and inside it you call context.run to invoke a function whose result is persisted, and context.rpc to call a function on another worker, possibly in another language. The README's example is a research agent: it accepts a question, plans a set of searches, fans them out in parallel, and synthesises a cited report.

async function research(context: Context, question: string) {
  // Plan the searches
  // context.run calls a function and persists its result
  const queries = await context.run(agent,
    `Plan the searches for: ${question}`
  );
  // Fan out the searches
  // context.rpc calls a function on another worker, even in another language
  const results = await Promise.allSettled(
    queries.map((q) => context.rpc(search, q))
  );
  // Synthesize the results
  return await context.run(agent,
    `Write a cited report. ${question}: ${results}`
  );
}

The framing in the README is that the same program is location transparent and failure transparent, and can be written in any Resonate compatible SDK and run on any Resonate compatible server. The audience is backend engineers whose workflows run longer than a single request, where a crash mid-way would otherwise mean losing the work already done.

The spec directory holds a Lean 4 machine and a trace checker

The unusual part of this repository is the spec/ directory, and it is the part that distinguishes Resonate from an ordinary workflow framework. It contains an executable abstract machine written in Lean 4, a catalogue of properties that every run has to satisfy, a TLA+ model, and a trace checker. The mechanism for holding a server to the specification is described concretely: the server's traffic is recorded, and the checker is asked whether the abstract machine can account for it. That is a different kind of assurance from unit testing. A test suite checks the cases its author thought of, while a checker asks whether an observed execution is consistent with the model at all. The README also says each directory has its own README, build, and tests, with no root level build, so the specification is maintained as a first class artifact rather than as documentation that drifts.

One server, three deployment shapes

The server itself is described as a single binary, and it comes in three implementations that target different infrastructure. impl/server/core/ is the Resonate server as a single binary. impl/server/postgres/ is the same server expressed as one SQL file on Postgres 16 or later, which is a striking claim: the durable state model is expressed declaratively enough to live in a database. impl/server/s3/ is the server written in Zig, whose only durable state is objects in an S3 bucket, so the runtime can be deployed onto object storage with nothing else. The architecture section makes the same point from the other direction, saying Resonate sits in the middle of the stack you already run: your language, your compute, your storage, your transport, and a plugin for everything it does not natively support yet. For an engineering team, the practical question is which of the three you can operate, and the answer determines whether this is a service you run or a library you embed.

Five SDKs, one protocol

The client side is split into five directories, one per language: TypeScript, Python, Go, Java, and Rust. The README states that the SDKs speak the protocol to a server, so the languages are interchangeable peers rather than one primary language with bindings around it. The remark about context.rpc being able to call a function on another worker even in another language is the concrete consequence, since the call crosses a language boundary rather than an in-process call. That also sets the limit of the design: cross worker calls are RPCs against a durable promise, so the receiving side has to be a Resonate compatible worker, not an arbitrary HTTP endpoint. Five SDKs is still early coverage, and the repository does not claim otherwise, but for a polyglot shop it removes the objection that your model service has to be written in the same language as your orchestration code.

Getting the server and the CLI onto your machine

Installation is a single command through a Homebrew tap, which installs both the Resonate server and the CLI. The README then points you at the quickstart for whichever SDK you picked, and the documentation site is the third step. The choice of deployment target is presented as a fork in the road rather than an advanced option.

brew install resonatehq/tap/resonate

The quickest paths are the TypeScript, Python, Go, and Java quickstarts, and the Rust SDK links to an installation section instead. If you intend to run on Postgres rather than the default, the README points at impl/server/postgres/, and if you intend to run on nothing but an S3 bucket, impl/server/s3/. Two supporting links are also given for evaluating a fit, an evaluate page for the next project and a separate site that explains the concepts behind distributed async await.

Where the project stops short

Several boundaries are visible from the repository itself. There is no root level build, so nothing installs with a single command from the top of the tree, and each of the seven or so subdirectories has to be handled separately. The specification guarantees are only as good as the trace checker, and the README describes the checker as holding a real server to the properties, which means the assurance covers behaviour the server actually produced, not every possible schedule. The version numbering also signals where the project sits: the recent releases are v0.9.8, v0.9.7 and v0.9.6, all in 2026, so this is pre 1.0 software whose interfaces may still move, even though the last push was on 2026-10-20. On the licensing side the project is Apache-2.0, which is permissive for a platform you intend to run in production, and the README adds that the logos in the architecture diagram are trademarks of their owners and appear only to identify the systems Resonate integrates with.

Editorial conclusion

Adopt Resonate if you are building long running workflows that fan out to other workers and need to survive a crash without losing completed steps, and if you can accept working inside the durable function and durable promise model rather than writing your own retry and checkpoint logic. Do not adopt it for a request that completes in a single function call, where the runtime buys you nothing. Verify first that your language SDK exists in the list of five, and read the trace checker behaviour in spec/ before you rely on the guarantee, since the conformity argument rests on that tool rather than on a test suite.

Frequently asked questions

Official sources

1. License: Apache-2.0
2. Project website
3. README
4. Releases
5. resonatehq/resonate on GitHub