What TLA+ and other languages give you is an automated theorem prover or model checked that usually is built on some form of temporal logic and predicate calculus. This is especially good at modelling multiple communicating processes. Taking a logical approach to discrete maths has a few benefits here.

> Even if your TLA proof checks out, it may be a false positive because it doesn't accurately reflect your production code.

This is something one needs to be concerned with when writing high-level, abstract specifications. There's no way yet that I know of where we can synthesize the program from the specification although I am aware of research in that regard. However we can still gain the benefit of well-defined invariants and pre/post-conditions that we can use in testing our implementation. For now your implementation will be separate from your spec but you gain insights from the spec you would not otherwise if you had only written code.

update as to whether it is an efficient use of time to use a model checker or automated theorem prover... Well I think the reason for their invention was to specifically to handle the tedious task of proofs in formal maths. Some operations are tedious and mechanical and computers are better suited to the task than humans.

One area I find interesting is languages with dependent type systems like Agda and Idris. It seems like we're not too far away from being able to model and prove our specifications directly in the type system alongside the program that implements it.