Correctness proofs of distributed systems with Isabelle/HOL