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 approa

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. (pdf) https://arxiv.org/pdf/1710.07191.pdf https://arxiv.org/pdf/1710.07191.pdf (video) https://youtu.be/_suyrSMJeCo https://youtu.be/_suyrSMJeCo (from the first author's homepage)