I have implemented consensus algorithm (based on Paxos). I have added some random test cases and it seems fine. To be sure, I want to do testing via model checking. I couldn't find a correct article for it. Are there any standard references on how to do model checking for Paxos?
You can find a formal model and proof of Paxos and Byzantine Paxos written by L. Lamport et al at http://research.microsoft.com/en-us/um/people/lamport/tla/byzpaxos.html.
The model can be checked using the TLA+ toolbox.
Notice that the author of the Paxos algorithm, the formal model above, and even the TLA+ modeling language is the same person:)