I meant most successful uses of verification tech, not proof, for SPIN. I shoudve worded that better. There is a version of it in a proof assistant called Favel

I meant most successful uses of verification tech, not proof, for SPIN. I shoudve worded that better. There is a version of it in a proof assistant called Favela if I recall. TLA+ has a proof system (TLAPS) and a model checker. Finally, if state and transitions are small, then a model-checker can give you similar assurance as a proof by essentially checking everything. These days, that's rarely the case, though. ACL2 was designed for real hardware and software. That's what many use it for. Rockwell-Collins builds CPU's, separation kernels, and low-level software for NSA with it. I agree author maybe dodged cuz it's not type theory.