I'm sorry but I don't see why the TLA+ modeling was necessary. You said that you noticed the lack of coordination before that. From your description, it seems like the mutex thing was a diversion. Anyway, a mutex would not necessarily be adequate for coordination (and many types of mutexes will not work between processes at all).
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.
Sorry for what? It was my first time using such a tool. I found it useful for understanding the system. I've improved my understanding of TLA+ since then and it has been valuable.
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.