There's no perfect answer and it's always been a limitation to take into account. There are model-checking solutions which take a spec and generate code, but yo

There's no perfect answer and it's always been a limitation to take into account. There are model-checking solutions which take a spec and generate code, but you don't get this with TLA+. In a way, you could make the same argument about writing tests: the code paths you exercise in your CI environment are not quite the same as what's running in prod, and neither is the environment in which the code is running (e.g. the load your process or host is under, the memory pressure, etc). That said, don't let this small gap and the lack of a perfect solution discourage you from using model checking, there is still a lot to gain from adding it as one more tool in your toolbox.