Yes the people I am referring to are in the business of designing and proving new distributed algorithms and proving/disproving the correctness of existing existing well-known algorithms for which only handwavy proofs have been provided. In particular it goes beyond just model checking.
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.
