Would I be right in saying Promela and SPIN are at a higher level than what is being described in the article?
I (one of the authors) did some distributed systems work with Promela about a decade ago, but it never felt like the right fit in the domain. It's got some cool ideas, and may be worth revisiting at some point.