The Quint (specification language based on TLA+) team just launched Choreo: a framework to get started writing specs for distributed systems, leveraging some known techniques such as the message soup. This should help more people get started with formal specifications without having to study so much about non-determinism and state space optimization.