> TLA+ is just a tool which basically does its job by exhaustively searching a space of possible solutions trying to find counterexamples. It works in some limited cases but doesn't work generally for any mathematical theorem.

Nope. TLA+ is a rich mathematical formalism, that includes a full-fledged proof assistant. It is, however, focused on verifying software rather than arbitrary mathematical theorems. There is also a model checker for TLA+ that can check your theorems (about finite cases of programs) at the push of a button. In practice, model checkers works in more cases than manual proofs, as manual proofs "fail" much more often, simply by being far too laborious; a model checker would verify in days what may take you months or more to manually prove.