Model Checking Paxos in Spin