Re: coq, Alloy and TLA+ (to an extent) are built around model checking and SAT solvers, which are better at finding problems in specifications.

Coq is a proof assistant (and dependently typed programming language); more aimed at theorems.