Projects · Security engineering · Research prototype · PROVEN
escrow-budget-mpst
What this establishes
That the escrow transfer sub-protocol, expressed as a multiparty session type with crash-stop failures in Rust, is deadlock-free and communication-safe on all executions and leaves the surviving peer deadlock-free after a crash at any point, enforced by the Rust type system on every build.
What this does not establish
The budget bound: session types govern communication, not arithmetic state, and the Charge that consumes budget sends no message, so it is invisible to the type. It assumes reliable, ordered transport (loss, duplication and reorder are assumed away), and models crash-stop, not crash-recovery. It is complementary to the Lean and TLA+ method, not a confirmation of it. This method never touches the cap theorem.
Trusted base
The Rust compiler and the mpstthree session-types library, and the assumption of reliable ordered transport. The TCB additions are set out in GAPS.md.
Method
The global type is projected to local types realised as Rust types, so a type-violating implementation and a non-projectable global type are both rejected at compile time; crash-stop faults are injected at every protocol point.
Result
make check builds green; the properties-by-methods table in COMPARISON.md records exactly where the two methods overlap and where they do not, with explicit NOT APPLICABLE cells, MPST not applicable to the budget bound, Lean not applicable to communication safety.
Negative controls. nc1, a type-violating implementation, and nc2, a non-projectable global type, are both rejected at compile time.
Reproduce
make check- Toolchain
- Rust with Cargo, and the mpstthree multiparty-session-types library
- Verified at
- repowazdogz-droid/escrow-budget-mpst@59bbc08 (2026-07-20)
This pass. Confirmed by source read at 59bbc08 (COMPARISON.md, README, negative controls); make check was verified green at publish, not re-run this pass.
Independent reproduction
None known. The build was verified from a fresh public clone (make check, exit 0).
Prior art and positioning
Multiparty session types and crash-stop session-type failure handling; the mpstthree library. The contribution is the paired complementary-not-confirmatory account with the sibling budget proof and its explicit NOT APPLICABLE cells.