Spin is a great learning tool. Spin is
so much more accessible than TLA+ Toolbox, for instance.
But for really serious work, there are
much more modern approaches that exploit
SMT solvers like Z3 (as TLA+ does) for vastly more
powerful model checking than Spin offers.
Also, the creator of Spin has retired it seems;
email to the spin list bounces. The "community"
forum has not accepted registrations for
several years. Basically it seems Spin was
a one man show, and he has not passed the
torch onto anyone else. The tool is still
incredible though, and a great place to start.
Just don't expect any help if you get stuck.
Get the Spin book if you want to understand
all the options.
Here, for example, EPR is a vastly more powerful formalism:
I just watched this video from 2017 work,
and was blown away. They can model check
FULL Vertical Paxos (not just a single round
of Synod) in that same couple of seconds;
that was done for the first time in this paper.
Paxos Made EPR: Decidable Reasoning about Distributed Protocols
Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham. OOPSLA 2017.
My writeup/getting started guide here (for checking Paxos) https://github.com/glycerine/spin_paxos
It is kind of awesome that you can alter the algorithm and immediately look at the counter example (problem you just created).