Chlipala's book is a decent one, but it's oriented towards software verification, coq, and the use of tactics (which I would consider anti-pattern).

Software Foundations is a good introduction to Coq and proofs, but overall is quite basic, and it also hides many details of how type theory works, so it's more of a hands on tutorial.

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.

> 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.

I bring up TLA+ because many people have quit trying to learn Coq because it was so hard with little perceived benefit. TLA+ has a high ratio of benefit for work put in. It also shows that abstract modeling can knock out deeper errors than regular tests or sometimes review. That makes it a nice, intermediate step toward stuff like Coq. Just a hunch a few of us have. :)

Alloy was really helpful for me to grasp the ideas behind checking a system design. But it is not a tool to write verifiable code. Rather it is a modelling tool to find bugs in the design before implementing things in code.