The main difference between Coq and TLA+ is that Coq is a research tool, intended and designed for use by researchers, while TLA+ is intended as an industry too

The main difference between Coq and TLA+ is that Coq is a research tool, intended and designed for use by researchers, while TLA+ is intended as an industry tool, and designed for use by engineers. They are essentially equivalent in their power when it comes to specifying and verifying software (although Coq is more suitable for proving general mathematics), but Coq is used almost exclusively by researchers. The learning curve is very different (one could get productive to the point they specify real nontrivial systems after learning TLA+ within a few days or a couple of weeks, while with Coq this takes many months), and TLA+ has much more automation.