They have these things called "proofs": http://cstheory.stackexchange.com/questions/25851/correctness-proofs-of-classic-paxos-and-fast-paxos http://cstheory.sta

They have these things called "proofs": http://cstheory.stackexchange.com/questions/25851/correctness-proofs-of-classic-paxos-and-fast-paxos http://cstheory.stackexchange.com/questions/25851/correctnes... Jokes aside, there are two ways out: huge simulators or writing very very simple code that matches 1-to-1 the steps of the proof. And Lamport's writing style for proofs [1] lends itself to simple matching implementations. [1] "How to Write a 21st Century Proof" http://research.microsoft.com/en-us/um/people/lamport/pubs/proof.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/p...