Developing distributed algorithms such as Paxos or 2PC is incredibly challenging. Veil is a novel tool that helps with modelling and automatic verification of such protocols. Compared to previous works it promises to combine strong automation combined with the power of manual interactive proofs in Lean 4.
In this seminar, you will read the Veil paper and present your findings to us and the other students. Furthermore, you will try out the Veil tool and attempt to verify a small example protocol of your choice.