I haven't seen Amazon publish any, but various teams in AWS use TLA+ for critical parts of their infrastructure.
A service I worked for there used it for an "absolutely must not make a mistake" component. Even with the initial learning curve of TLA+, two engineers were able to define the application logic, identify bugs and come to a final model in comparatively short order. Once they'd got that final model they found it relatively easy to translate that in to the final service code.
By the time they were done, they realised they'd actually spent less time in total, TLA & coding, than they'd anticipated just building the component from scratch without TLA+.
My understanding is that TLA+ is primarily used for model checking not correctness proofs. I've dug around for TLA+ proofs and found only simple examples.
That being said, model checking alone is really powerful and can uncover serious design flaws.
But you're right that deductive proofs are hardly ever worth the effort when you have a model checker. If you can get 99.99999% confidence for essentially free, most people wouldn't pay extra months of work to get to 99.999999% confidence.
There were many projects using Pi Calculus, too. One of my project ideas is something that converts TLA+ to SPIN and Pi Calculus to use their tools and works. Or just otherwise integrates them.
I don't think TLA+ is far too expressive to translate to Promela. There are, however, tools that translate subsets of TLA+ to ProB: https://www3.hhu.de/stups/prob/index.php/TLA
1. You can find plenty of examples, some for production systems (Elasticsearch, some algorithms in the Linux kernel) on the TLA+ subreddit: https://www.reddit.com/r/tlaplus/
2. Learning TLA+ from available tutorials until you can write serious specs of real systems takes 2-4 weeks (part time); achieving the same competence level in a full-time workshop takes 3-5 days.
Is it cheaper to hire someone who knows TLA+ or to find a consultant?