[inaseer]

Writing tests to prove you've a correct implementation is indeed a very hard problem. I toyed with an interesting idea last year where I began to write a simple (but intentionally incorrect) Paxos implementation using P# (now known as Coyote) and wanted to see if P#/Coyote's systematic exploration of the state space will show me the various race conditions which violated the protocol's correctness. To my surprise, the technique was quite effective. P#/Coyote was able to point out to a number of bugs after I specified the safety and liveness properties which weren't too hard to do. In effect, after specifying the safety/liveness properties, I was able to use P#/Coyote's state-space exploration to ensure the implementation had solid test coverage. More details are at https://github.com/imnaseer/DiscoveringPaxos where the project starts out with a simple naive implementation, uses P#/Coyote to find bugs, makes incremental modifications till we finally have a working version faithfully following the Paxos description.