Introduction

Telltale is a Rust framework for choreographic programming with multiparty session types. It enables writing distributed protocols from a global perspective with automatic projection to local implementations. The accompanying Lean 4 formalization provides mechanized proofs of preservation, progress, coherence, and harmony.

The framework includes a bytecode VM with deterministic scheduling and configurable buffer backpressure policies. Asynchronous subtyping uses SISO decomposition with orphan-free deadlock checks. Endpoint transfer semantics support ownership handoff at runtime with progress token migration. Content addressing assigns cryptographic identities to protocol artifacts. The same choreography compiles to native and WASM targets.

Core Concepts

Session types encode communication protocols as types. A type like !String.?Int.end sends a string, receives an integer, then closes the channel. The compiler checks that implementations follow the protocol contract.

Multiparty session types extend this to protocols with three or more participants. Global types describe the full protocol. Projection transforms global types into local types for each participant. The type system tracks dependencies between participants to prevent deadlocks.

Choreographic programming builds on global types. A choreography describes computations and message flow from a neutral perspective. Endpoint projection generates the local implementation for each role.

Effect Handlers

Communication operations are algebraic effects. Sending and receiving messages are abstract operations that handlers implement concretely. Programs specify what to communicate.

Handlers determine how messages are delivered. In-memory channels work for testing. TCP connections work for deployment. The protocol logic remains unchanged across execution strategies.

Bytecode VM

The VM compiles local types to bytecode instructions. It manages scheduling, message buffers, and session lifecycle. The concurrency parameter N controls how many coroutines advance per round. Per-session traces are invariant over N.

Lean Verification

The Lean 4 formalization spans roughly 624 files and 127k lines in the core libraries (generated metrics in lean/CODE_MAP.md). It covers global types, local types, projection, and operational semantics. Deadlock-freedom claims are assumption-scoped with explicit premises for well-typedness, progress reachability, and fair scheduling.

The telltale-lean-bridge crate provides JSON export and import for cross-validation between Rust and Lean. See Lean Verification for the verification pipeline.

Document Index

Paths by Role

Library Users

Start with Getting Started. Then read Choreographic DSL. Continue with Examples and API Reference.

VM Integrators

Start with Architecture. Then read Effect Handlers and Session Types and VM Architecture. Continue with Bytecode Instructions and Session Lifecycle. See VM Simulation for testing.

Paper Reviewers

Start with Architecture and Theory. Then read Lean Verification and Lean-Rust Bridge. Continue with Capability and Admission and Theorem Program. See Distributed and Classical Families and Glossary and Notation Index for reference.

Further Reading

For MPST theory, see A Very Gentle Introduction to Multiparty Session Types. For asynchronous subtyping, see Precise Subtyping for Asynchronous Multiparty Sessions.

For choreographic programming, see Introduction to Choreographies. For integration with session types, see Applied Choreographies.

See Glossary and Notation Index for shared terminology.