This is great stuff. I did something similar in a 2020 paper[1] using Coq. I did not find Coq particularly suited for this type of work. Isabelle/HOL looks promising.
One thing to note is that these types of verifications can become difficult when the systems are layered. Even the simplest real world systems are layered, when you factor in the underlying transport for the messages. The TLC paper provided a way for distributed systems to be composed in a way that reduces the complexity of the proofs for each distributed component.