Can you instantiate this claim with an example? I'm somewhat knowledgable in both math and computer science theory but have yet to feel as though my math background has helped me in practical CS.
We tracked it down to a race between two services in the data plane. It turns out the VM controller wouldn't wait for the network controller to unplug a virtual interface before requesting the interface to be plugged back in. There was a lack of co-ordination happening. However it only happened when the network component was under heavy enough load that it would take too long to respond before the VM service finished rebooting the VM -- usually it was fast enough and the error wouldn't appear.
I managed to model this interaction at a high level in TLA+. From there I had suspected that the error was in the mutex locking code in the async library this system depended on so we refined the model pretty close to that implementation. As I recall we found that the mutex code wasn't the culprit -- a fine result. We ended up implementing some light-weight co-ordination mechanism to ensure that the VM service waits to acknowledge the progress of the network service.
Since then I've continued to use TLA+. I find that programming languages are insufficiently expressive enough to describe high-level interactions between other processes, network events, and humans.
So to me it seems that you could have gone straight to the lightweight coordination mechanism without the TLA+ model. And anyway, if there was a problem with the mutex, you could test that theory by doing additional logging or an experiment around the mutex functionality.