I used TLA+ to design a locking strategy around memcached (well, it's a lot messier than that, I used TLA+ to debug a race condition we encountered in productio

I used TLA+ to design a locking strategy around memcached (well, it's a lot messier than that, I used TLA+ to debug a race condition we encountered in production which led eventually to a locking strategy). It's a fantastic tool for designing concurrent routines.