While that parallel is genuine, it's hard to compare Coq and TLA+ since the mechanism and style of proof they embody is very different. TLA+ tries to ensure that you can exhaustively check implied models as its basis of proof (I believe) while Coq recognizes that types syntactically represent logics and we can thus construct programs in those logics to represent proofs.
So, one layer deeper they're dramatically different beasts.
The TLA+ tools can do exhaustive model checking, as well as mechanically checked proofs. The proofs typically use an SMT solver to verify them. Of the two I've only used model checking in a serious way, but you can find Lamport's proofs of things like paxos and have it turn all the theorems green.
you are correct. There is a huge difference between the two and as you say only coq is able to express proofs in themselves and not just a coarse grained summary of their structure.
So, one layer deeper they're dramatically different beasts.