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.

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

The Rust project implements the operational model from the paper series. It includes the choreography pipeline, VM runtime behavior, admission checks, and simulation tooling.

• Choreographic DSL with projection and compiler pipeline
• Virtual machine for safe execution of asynchronous buffered protocols
• Runtime theorem-pack and capability-guarded admission interfaces
• Reconfiguration-facing checks for link, delegation, and transition steps
• Simulation and cross-target conformance tooling for Rust VM and Lean reference traces

Main code is in rust/. Workspace configuration is in Cargo.toml. A typical health check is cargo test --workspace --all-targets --all-features.

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.

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 VM 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.

# 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.

Licensed under the MIT license.