Comment by philix001

People that can write proofs in Coq and Isabelle might prefer that over the TLC approach of exhaustively checking all the possible states allowed by a TLA+ spec. But writing proofs in Coq/Isabelle/Lean/HOL is a more sophisticated skill and requires even more training on the multiple theories available in these provers. The brute force approach of TLA+/TLC is more dependable as part of an engineering process. Some specs can be really hard to prove, but easy to exhaustively check.