They're complementary, IMO: unit tests show that your implementation works as expected, while a formal specification allows you to check that your approach is right to begin with.
That being said, TLA+ specifications have uncovered really hairy concurrency bugs which would be a nightmare to unit test - for instance, Amazon found bugs in DynamoDB which required 35 steps to reproduce [1].
unit testing (and any kind of testing for that matter) shows that your code works for a set of inputs. formal verification methods show that it works for all inputs. it’s the holy grail but comes with a really high price tag to actually do it (so unless you’re writing something critical or have a lot of resources you normally get your software to the point where it’s good enough through unit/etc testing)
Think of a process by which you start with a vague sketch of a system and end up with a concrete implementation in, say, C++. The latter is the highest level and least detailed. The latter is as detailed as the specification of your system will get. A prose design document of your model might sit somewhere on this spectrum very close to the vague sketch. A TLA+ spec sits somewhere in the middle. It's a refinement of the design doc with more details specified concretely, but not all of them (that's the actual implementation). But this mid-level specification is usually enough to make highly non-trivial assertions that invariants hold (safety properties) and also liveness properties are satisfied too. But keep in mind that the specification of your system is distinct from the model checking of that spec. The latter is like a test, albeit of your system not just some "unit" within your system.
