> amazon has been using TLA+ to prove/check correctness of production distributed algorithms and systems for about a decade Such an in-your-face, smug and flip

> amazon has been using TLA+ to prove/check correctness of production distributed algorithms and systems for about a decade Such an in-your-face, smug and flippant comment but ... On some projects. In some teams. And Aurora lost a lot of data initially in spite of whatever TLA+ they were using, somewhere at Amazon.