Specification
The Distributed Async Await specification — protocols, definitions, and models for durable execution.
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. These pages are the prose specification: the human-readable companion that explains the same protocol. Where prose and Lean disagree, the Lean model wins.
For working code that implements the protocol, see the reference implementations: the Resonate Server and the TypeScript, Python, Rust, Go, and Java SDKs.
The specification is structured into three parts:
- Programming model — the intended structure of distributed programs and the developer interface.
- Execution model — how distributed programs reliably make progress.
- System model — the environment in which distributed programs exist, and a way of thinking about them.
A glossary defines the load-bearing terms.
Programming model
Functions and promises lifted to span processes, machines, and time. Defines the developer interface.
Execution model
Coordination, recovery, and message-passing protocols that make distributed programs make progress.
System model
The first-principles model of processes, executions, and messages that grounds the rest of the specification.
Glossary
Load-bearing terms used throughout the specification.