[tyu2]

You can look into TLA+ without any specific reason, it's relatively easy to grasp and doesn't take much time. And it isn't actually that popular in distributed systems, as it demands certain software development process most real world distributed systems can't benefit from, the only examples of distributed systems are literally distributed cloud services made at megacorps no less, like in the video. But mostly it's purely people who are into formal proofing who play with it, regardless of whether there are actual benefits. I don't like doing it and was never able to justify using it on any real project, I was always able to find more beneficial ways to spend this time on instead. And tiny cases where I really needed to make sure of something I just covered the whole state space with tests and simulations. Maybe if it wasn't written in java and all the tooling was some portable C easily integratable anywhere things could be different, but as it is I can't even accept having jvm everywhere.