The author does start talking about model checking in the third paragraph and go on using "SPIN", so there's a significant part that is interested in model chec

The author does start talking about model checking in the third paragraph and go on using "SPIN", so there's a significant part that is interested in model checking, anyway. I can see where the parent is coming from. I think you can both be right - it can be valuable in any case.