Yes, but there really aren't too many good solutions to that that aren't either extremely language or domain specific. And if you're careful you can get a lot of direct mileage out of it. For example, MongoDB (yes, that one!) used it in the development of their Atlas system and has a paper about using TLA+ to model the system, characterize behaviors, then generate compilable-code test cases from those minimal set of behaviors -- which are then directly linked against the core internals of the Atlas codebase as a client library. They then run those tests and re-generate them when the model changes. "Model based test case generation" is the strategy here. So you can characterize what happens in split brain scenarios, state machine transition failures (conflicting transactions), etc.

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...