Some of us (read... one of us, and not me, yet) uses TLA+ when theorizing changes to parts of M3DB, which is a distributed time series database. You can see th

Some of us (read... one of us, and not me, yet) uses TLA+ when theorizing changes to parts of M3DB, which is a distributed time series database. You can see the specs here, the current TLA+ models the consistency model of data being persisted to disk (flush, snapshot), there was at some point TLA+ for describing the quorum writes/reads along with the background tick event loop but that must be elsewhere now. https://github.com/m3db/m3/tree/master/specs https://github.com/m3db/m3/tree/master/specs