Spin is my new favorite thing. It
helped me learn Paxos by model checking the algorithm.<p>My writeup/getting started guide here (for checking Paxos)
<a href="https://github.com/glycerine/spin_paxos">https://github.com/glycerine/spin_paxos</a><p>It is kind of awesome that you can alter the
algorithm and immediately look at the
counter example (problem you just created).