> 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.