A Formal Proof of The Chandy-Lamport Distributed Snapshot Algorithm You can build this theory using Isabelle2020 and the following command: isabelle build -D .