Specification
The Distributed Async Await specification — protocols, definitions, and models for durable execution.
Distributed Async Await is a collection of protocols, sub-specifications (definitions), and models. This section is the canonical home for the formal specification — for working code that implements it, see the TypeScript, Python, and Rust SDKs.
The formal models underlying this spec are expressed as a Lean 4 abstract machine in resonatehq/resonate-specification. The promise, schedule, and task state transitions there are the machine-checkable ground truth for the system model.
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.