Ato: from source to verified continuation

Ato turns software on your machine into a Capsule: a sealed, resumable point in a computation, identified by what must be reproduced — not just the files that were used. Verification evidence records the attempt that satisfied the Contract.

The pipeline is:

Source / intent
       ↓
Contract K + Derivation D
       ↓
Formation
       ↓
execute D on a compatible Runtime
       ↓
candidate Continuation C'
       ↓
verify C' satisfies K
       ↓
Capsule (identity K) + verification evidence

A Capsule holds a Contract as its identity: what must be reproduced for a future computation to count as the same continuation point — not how it was built. A Derivation is one executable route toward that Contract. One Capsule can have many Derivations.

Start here

Follow the Getting started guide to build Ato from source and form a small app on your own machine with:

ato form <dir> --runtime local

Key terms

• Continuation C — the computation from its current point onward.
• Contract K — the observable conditions a continuation must satisfy; a Capsule's identity.
• Capsule — the sealed point plus its Contract and verification evidence.
• Derivation D — an executable route that attempts to reach a continuation satisfying K.
• Formation — the process that tries Derivations, observes candidates, and keeps what verifies.
• Run — a live continuation resumed from a Capsule.
• Runner / Runtime — where a Derivation executes (Phase 1 admits --runtime local).
• Binding — how a logical need (a port, a workspace path) maps to a concrete endpoint.

Read the Concepts page for the full definitions, and capsule.toml for the authoring format behind Contracts and Derivations.

Experimental areas such as the Runtime Network, browser verification, and model-guided decisions are intentionally out of scope for this overview.