Our company uses memcached to store short-lived pieces of user-specific data for one of our (web) products. The way this was architected, any time a user visite

Our company uses memcached to store short-lived pieces of user-specific data for one of our (web) products. The way this was architected, any time a user visited a page, a request would be made to memcached with the user, check to see if memcached had data, fetch the data, and then clear the cache. This feature had always been a bit buggy, but then we decided to start adding more things to this user-specific data store. And it blew up. Data we wanted to store for the user wasn't being stored at all, data was being fetched many requests after they should have been fetched. Sometimes stale user data was being fetched days after the data should have been cleared, and the data was not being cleared. After being pulled into the war room for this, I started looking into the code and architecture of the issue and was appalled. Code for the feature was designed piecemeal, tests were nonexistent, and of course only certain cases of the code were tested. The whole thing was a concurrent nightmare and would not hold up to concurrent reads/writes. Rather than sit there and make sense of it all (I started sketching it out on paper because it was so convoluted), I ended up writing the spec out in TLA+. Just forcing myself to write the spec out made me consult the implementation dozens of times, to verify the exact behavior in a way that TLA+ could model it. And then after I did that, it was obvious that the code was broken. So in my TLA+ model I shored up what I thought were the problems, ran the model checker, and was expecting a fix. Nope. The model checker found another bug. I tried a different strategy, and it found another bug. I iterated with the model checker dozens of times, and slowly changed the model entirely, making it simpler and clearer to understand. Finally the model checker couldn't find any bugs. I converted the model to real code and, after some code review, I shipped the fix. It worked. I wish more people would spec their code with something like TLA+, but as I've seen in my own teams, the mantra is ship first think later.