Yes indeed. Seen it in use in AWS across a number of critical components. The team I was on in AWS used it for the implementation of a particular component th

Yes indeed. Seen it in use in AWS across a number of critical components. The team I was on in AWS used it for the implementation of a particular component that needed to operate at large scale and had absolutely zero tolerance of failure. Two engineers learned TLA+, started writing up the logic and discovered various ways in which the logic would work on small scale but wouldn't scale up to parallel operation across multiple servers. It's fair to say TLA+ saved our bacon there before we'd written a single line of service code. In the end we actually got the component out to production faster than predicted. The TLA+ code gave solid shape for the actual production code, and we were quickly able to prove that the code was valid and that things were working correctly. In my current role in Oracle Cloud Infrastructure, there is actually a small dedicated team of engineers that help services use TLA+ for components, headed by Chris Newcombe, one of the authors of the TLA+ whitepaper that came out of Amazon (https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon....) My current team has just started exploring it for use for a component that similarly has little tolerance for error. It's not in the same territory of "if it fails it's catastrophic", thankfully, but if it fails it's a major inconvenience for customers.