escrow-budget-mpst

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.

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.

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.

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.

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.

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.

make check

Findings drawn from this artifact are on the evidence ledger.