Telltale

This repo contains three related projects. A Rust library for writing composable multiparty session-typed choreographies, an extensible Lean proof system, and a three-paper series describing MPST theoretical contributions.

For Reviewers

Run just artifact-check. Then inspect papers/artifact_manifest.json and Artifact Reproduction Guide.

Project Surfaces

1. Rust Library

The rust/ project implements the operational model from the paper series. Protocols are written once with the tell! macro and projected to local session types, typed effect interfaces, and authority/evidence constructs for each role. The DSL features the following features:

• Protocol machine for deterministic execution with session type enforcement
• Declared effect boundaries where host logic implements generated Rust traits
• Typed failure, timeout, and cancellation paths with explicit evidence flow
• Native and WASM targets from the same protocol specification
• Simulation, replay, and cross-target conformance tooling against Lean reference traces

2. Lean Proof System

The Lean project is an active mechanized proof stack. It covers session foundations, semantics, protocol coherence, runtime adequacy, and bridge theorems. Main code is in lean/. The toolchain pin is lean-toolchain. A typical proof-facing gate is just verify-protocols.

3. Papers + Artifact Supplement

The three papers establish a mechanized metatheory for asynchronous buffered multiparty session types. Paper 1 defines an operational coherence invariant enabling compositional preservation proofs. Paper 2 adds quantitative Lyapunov bounds and decidability results. Paper 3 proves a harmony theorem for dynamic reconfiguration. Together they connect choreographic specifications to protocol-machine runtime adherence. All results are mechanized in Lean 4.

The papers/ directory contains manuscripts and reproducibility documentation. PDFs: Paper 1, Paper 2, Paper 3. Citation metadata is in papers/CITATION.cff.

Formal Verification

Telltale is formally verified for the declared shipped surface documented in docs/902_verification_inventory.md, under the listed public assumptions and trusted base.

The claim covers the Lean semantics and theorems, the theorem-defined Rust↔Lean core protocol-machine runtime correspondence, the shipped first-party handler and transport contract boundary, and the shipped first-party crate artifacts through the audited artifact-correspondence pipeline. Compiler, macro, and third-party integration paths are excluded unless the verification inventory says otherwise.

Quick Start

# Rust library health
cargo test --workspace --all-targets --all-features

# Lean/proof-facing protocol verification lane
just verify-protocols

# Paper supplement reproducibility + paper build + manifest
just artifact-check

This command set validates the Rust library, proof-facing protocol checks, and paper supplement workflow.

Repository Layout

License

Licensed under the MIT license.