I did a lot of distsys work With tla+. I still think it’s the best use. It’s really hard to make sure your code matches what you prove.