[zozbot234]

There's plenty of real-world production use of TLA+, including by Amazon. The "toy model" approach may have limitations of a sort but it's far from purely academic - building simplified models of a complex system is routine practice.

The obvious difference with PowerPoint design is that non-trivial failure modes can be surfaced automatically if they're reflected in the toy model - PowerPoint slides don't do this.

You don't even have to use TLA itself for this purpose, a Lean development could also do this - but then you would have to put together much of the basic formalism (which ultimately works by combining the "modalities" of time, state and non-determinism) on your own.

[pjmlp]

We have all seen how well it gets surfaced automatically at AWS.

[zozbot234]

There might be plenty of potential failures that we haven't all seen, simply because the problems were fixed after TLA+ modeling brought them up.

[pjmlp]

Or it might be that the model doesn't really avoid all possible human failures when translating TLA+ into Java, C++ metatemplate programming, or whatver.