TLA+ is used for model checking, right? Do Isabel and Coq do model checking, or are they optimized for model checking? I haven't tracked the area for years. I thought popular model checking systems were like SPIN and nuSVM. Didn't know the industry has shifted to using a proof system like Coq.