[tyu2]

> as well as the fact that the inventor of TLA+, Leslie Lamport, is very well-known for his work in distributed systems, led to TLA+

But didn't lead him to come up with decent distributed algorithms. PAXOS is a negative example here for example, where Leslie said that formalization naturally derives such algorithms, but in reality many years and many iterations on the idea from many different researchers and engineers is what led to something actually useful in practice, as PAXOS wasn't, and formalization was by far the least important thing ever.

[pron]

I'm not sure how you're getting this. In what way is Paxos a negative example? Raft, which is also a take on Paxos, was also formalised in TLA+ by its inventor, as were many other variations on Paxos; in fact, it is hard to derive any non-trivial distributed algorithm, based on Paxos or otherwise, without formalisation. This is true for most subtle algorithms, and distributed algorithms are prime examples of those. Algorithms that had not been formalised on inception, Chord being a famous example of one thought to have been "proven" correct without formalisation were often found to be incorrect once formalised [1]. Not to mention that that work won Lamport the Turing Award.

[1]: https://brooker.co.za/blog/2014/03/08/model-checking.html