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.
Right now some people have a theory that Uncle Bob is noise in the sea of architectural opinion, and we can't move forward because we don't have enough data. The call for more data is welcome by me.