They have these things called "proofs": 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/p...

jepsen, quickcheck, interleave testers like concuerror; or, by implementing directly in a proof assistant/language like coq, as was recently done with raft.

TLA+ model checking and an implementation that follows the spec as closely as possible.