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+.

The architect of AWS, James Hamilton, is a huge fan of formal verification and has spoken about it at length.

https://perspectives.mvdirona.com/2014/07/challenges-in-desi...

http://lamport.azurewebsites.net/tla/amazon-excerpt.html

Indeed. As I recall, he was really happy to hear my team was using it for the component.

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.

You can find some big deductive proofs here: https://members.loria.fr/SMerz/papers.html

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.

Cosmosdb is Microsoft multi model, multi master, geo database with five consistency levels for performance.

https://github.com/Azure/azure-cosmos-tla

For the first question, there you go: https://lamport.azurewebsites.net/tla/formal-methods-amazon....

SPIN has long been used for similar stuff in academia and industry. They have published a lot of their specs and results.

http://spinroot.com/spin/whatispin.html

http://www.imm.dtu.dk/~albl/promela.html

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.

Which model checkers use Pi Calculus? I've thought about learning Pi Calculus but an much less interested if there's no checker.

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

Yup, here's some good ones! https://github.com/elastic/elasticsearch-formal-models

Along with someone fixing a bug well before someone found the bug in the wild: https://github.com/elastic/elasticsearch/issues/31976#issuec...

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.