Formal verification of distributed systems