One of my coworkers used TLA+ to prove a change to a service my teams runs was correct. The service was essentially a key/value store. If one region didn't kn

One of my coworkers used TLA+ to prove a change to a service my teams runs was correct. The service was essentially a key/value store. If one region didn't know about a key, it would recursively ask the other regions in parallel for the data. Eventually we needed to add support for deleting data. We deleted data that hadn't been read in a few months. We used TLA+ to prove our region-sync code and deletion code interacted properly along with regular get/put operations.