I think the hard part about distributed systems is the combinatorial explosion of possible system states, which is also common to any concurrent program. Really distributed systems is just concurrency on hard mode, where failures are basically guaranteed instead of being very rare.

I wouldn't particularly say I'm a TLA+ promoter (it's a FOSS project), any more than anyone who has a great fascination with a language/framework/algorithm/viewpoint is a promoter. We're all promoters of the memes that live inside our heads!