"Correctness proofs of distributed systems with Isabelle" by Martin Kleppmann