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 paper/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 paper project contains the three manuscripts and submission-focused reproducibility tooling. The sources are paper/paper1.tex, paper/paper2.tex, and paper/paper3.tex. The reproducibility guide is Artifact Reproduction Guide. Citation metadata is in paper/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-checkThis command set validates the Rust library, proof-facing protocol checks, and paper supplement workflow.
| Path | Purpose |
|---|---|
rust/ |
Rust library and runtime system |
lean/ |
Lean proof development and verification stack |
paper/ |
Paper sources, supplement metadata, citation |
scripts/ |
Verification/repro automation scripts |
docs/ |
Extended technical documentation |
Use the Nix flake for reproducible builds with pinned toolchains. See Artifact Reproduction Guide for the full workflow and expected outputs.
Licensed under the MIT license.