Amazon continues to use TLA+. I work there. It's not a tool needed every day, and it's not needed by everyone (really, not by almost _anyone_). But sometimes it

Amazon continues to use TLA+. I work there. It's not a tool needed every day, and it's not needed by everyone (really, not by almost _anyone_). But sometimes it's the best tool for the job. You won't be getting much data on this because companies are secretive. The way it's used is to ensure correctness of distributed systems. A classic example might be ensuring that a model for backing up customer data is unable to get into indeterminate state. It's important to get the model right. But the model isn't code - TLA is not a programming language, it's a tool for modeling state machines; yes, of course, one needs to also write software to deliver value.