Comment by jldugger

Presumably that one guy at AWS who promotes TLA+ is furiously modeling all this himself in more detail for internal analysis.