If your understanding of the domain isn't thorough, is TLA+ going to be much help?
1) You have to specify your system, right? With TLA+, you can just wave you hands and say "okay this part does something, I guess." You have to force yourself to understand what, exactly, you want your system to do and what you want out of it.
2) Most systems have edge cases, side effects, and race conditions. Are you sure your design is robust against them? You might think you have good arguments for that, but wouldn't it be better to rigorously _check_?
Tests and types and stuff help you find bugs in your implementation. TLA+ helps you find bugs in your blueprints.
Writing unit tests before code can help avoid mistakes in the interface design.
Perhaps similarly, writing formal specification could expose the holes in your domain understanding.
Did you mean something different from that?
Though I think the "and don’t care to" part is a little harsh. I do care, though mostly fail. Sometimes I find it difficult to get useful information from the domain experts, and it doesn't help that domain experts often keep subtly changing the meaning of the concepts we've been working with, until nothing is left of the original and the whole system is a bit of a mess.
I suspect it could, actually, because it lets you formalize and work with the implications of the understanding you do have without getting bogged down in the details of actual coding. Seems like this could give you the opportunity to debug your mental model much earlier in the process. (I confess I haven't actually tried TLA+, but I plan to.)