For some of the Amazon engineers mentioned in the paper that training took 1 to 2 weeks. The trade off for that training is that you know the those properties

For some of the Amazon engineers mentioned in the paper that training took 1 to 2 weeks. The trade off for that training is that you know the those properties it describes are correct. For some systems the trade off is worth it and for a few, required. I didn’t say you should use TLA+ for simple projects. It is incredibly useful for specifying systems where correctness, liveness, etc matter greatly and the complexity of the project is sufficiently high that you’d be uncomfortable describing it with boxes and arrows. I think it’s rather reckless to design a complex system of the sky-scraper magnitude without some sort of verification tool like TLA+. It’s a matter of degrees.