Lamport has published a TLA+ spec of the Paxos consensus algorithm¹, but none I could find of the Paxos algorithm itself (aka multi-Paxos). In 2016 some academ

Lamport has published a TLA+ spec of the Paxos consensus algorithm¹, but none I could find of the Paxos algorithm itself (aka multi-Paxos). In 2016 some academics at Stony Brook University did, along with a machine-checked TLAPS proof, updated in 2019: https://arxiv.org/abs/1606.01387 https://arxiv.org/abs/1606.01387 ¹Paxos consensus refines specs for consensus and voting. See the spec and accompanying material here: https://lamport.azurewebsites.net/tla/paxos-algorithm.html https://lamport.azurewebsites.net/tla/paxos-algorithm.html