My beef with TLA+ is that it's not the same code, so while you're testing the design yes, you aren't testing the implementation of the design, which is just as important (if not harder too) to get right.
In reality the design stage is a pretty critical phase so you need all the help you can get, so even if you don't like TLA+ you're way better off than not modeling at all.
As an example of the language specific thing, though, there's a library for Haskell I like that's very cool, called Spectacle, which also implements the temporal logic of TLA+ along with a model checker, but as a Haskell DSL. An interesting benefit of this is that you can model check actual real Haskell code that runs e.g. in your services, but I haven't taken this very far. There are also alternative solutions like Stateright for Rust. But again, not everyone has the benefit of these...
Unfortunately I got the product wrong; it was not Atlas, it was Realm Sync. All of the test-case generation stuff is in Section 5.
Using https://github.com/awslabs/shuttle which works on our real Rust code.
Documentation is still generally useful, and so is a model. You have to be committed to keeping both up to date as the code evolves.