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.