Right. TLA+ has a proof assistant, just as Coq and Isabelle do, and it has been used to good effect. But because there is also a model-checker capable of checki

Right. TLA+ has a proof assistant, just as Coq and Isabelle do, and it has been used to good effect. But because there is also a model-checker capable of checking (a subset of) TLA+ (actually, two model checkers now), practitioners greatly prefer using that over a proof assistant. The reason is that if your goal isn't to publish a paper but to deploy a system, what you're optimising for is bugs found per hour of effort, and a model-checker has a higher ROI in that regard than deductive proofs.