I am not a "TLA+ promoter" but think it is a very valuable tool for anyone building distributed systems. The value of TLA+ is that it forces you to carefully consider your algorithm, which is certainly important if the algorithm is complex but equally important if the algorithm is simple. Most people will struggle to correctly specify even a simple algorithm in TLA+ because they will miss a lot of things they had assumed without ever thinking about.

Real world systems need to handle all the things you mention. TLA+ helps you consider all these issues with spelling them out individually. There is no point in building a complex system if you haven't taken the time to validate the correctness of the target system in the first place.