This is the best TLA+ specification of the Paxos algorithm I can find, for anyone interested. I was surprised that although Leslie Lamport has published a TLA+ spec for Paxos consensus¹, he has not published one for his Paxos algorithm itself, aka multi-Paxos. These Stony Brook academics did, complete with improved TLAPS machine proof and the added feature of preemption. Their digressions to existing Paxos proofs with other tools and the history of this algorithm's formal specification are also interesting.
¹ Paxos consensus refines specs for consensus and voting. See the spec and accompanying material here: https://lamport.azurewebsites.net/tla/paxos-algorithm.html