Rust, tla+, 2 phase commit, 3 phase commit

For those who have implemented 2 phase commit, 3 phase commit:

  1. was Rust's type system useful in catching errors ?

  2. did you use tla+ / other model checkers ? are any of them good for auto generating Rust code ?

EDIT: More generally, there is the question of: Rust's type system is great at helping prevent errors when we have multiple threads accessing the same memory.

However, is there a way to use / abuse the type system to help verify correctness of distributed algorithms. If so, how. If not, are there tools for verifying distributed algorithms that can also synthesize Rust code ?

Rust is very helpful in this regard I would say (rustdb::pstore - Rust). I don't see it as particularly significant in implementing distributed algorithms, apart from being generally a good systems programming language, so the right tool for the job. But I haven't yet implemented distributed algorithms.