Proof of correctness of the Paxos consensus protocol. This is an early effort, based on the presentation of the protocol in the OOPSLA'2017 paper "Paxos Made EPR: Decidable Reasoning about Distributed Protocols", by Padon et al.
Although the proofs require multiple asserts and a few proof transformations, this self-contained module gives a good illustration of how Why3 and SMT solvers can be used to verify distributed algorithms.
A more recent, refinement-based formalization can be found in folder paxos.
- paxos.mlw: formalization of Paxos consensus