4 ms·

Have any cloud providers or open source projects started publishing their proofs of correctness yet? Is it cheaper to hire someone who knows TLA+ or to find a

Have any cloud providers or open source projects started publishing their proofs of correctness yet? Is it cheaper to hire someone who knows TLA+ or to find a consultant?

Twirrim 8y ago
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+.
- SEJeff 8y ago
  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-designing-at-scale-formal-methods-in-building-robust-distributed-systems/ https://perspectives.mvdirona.com/2014/07/challenges-in-desi... http://lamport.azurewebsites.net/tla/amazon-excerpt.html http://lamport.azurewebsites.net/tla/amazon-excerpt.html
  - Twirrim 8y ago
    Indeed. As I recall, he was really happy to hear my team was using it for the component.
nickpsecurity 8y ago
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://spinroot.com/spin/whatispin.html http://www.imm.dtu.dk/~albl/promela.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.
- Karrot_Kream 8y ago
  Which model checkers use Pi Calculus? I've thought about learning Pi Calculus but an much less interested if there's no checker.
- pron 8y ago
  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 https://www3.hhu.de/stups/prob/index.php/TLA
Sorrop 8y ago
For the first question, there you go: https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon....
uluyol 8y ago
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.
- pron 8y ago
  You can find some big deductive proofs here: https://members.loria.fr/SMerz/papers.html 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.
pron 8y ago
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/ 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.
ashish_negi_ 8y ago
Cosmosdb is Microsoft multi model, multi master, geo database with five consistency levels for performance. https://github.com/Azure/azure-cosmos-tla https://github.com/Azure/azure-cosmos-tla
hwayne 8y ago
Yup, here's some good ones! https://github.com/elastic/elasticsearch-formal-models 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#issuecomment-404722753 https://github.com/elastic/elasticsearch/issues/31976#issuec...

Have any cloud providers or open source projects started publishing their proofs of correctness yet? Is it cheaper to hire someone who knows TLA+ or to find a consultant?

Twirrim 8y ago

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

SEJeff 8y ago
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-designing-at-scale-formal-methods-in-building-robust-distributed-systems/ https://perspectives.mvdirona.com/2014/07/challenges-in-desi... http://lamport.azurewebsites.net/tla/amazon-excerpt.html http://lamport.azurewebsites.net/tla/amazon-excerpt.html
- Twirrim 8y ago
  Indeed. As I recall, he was really happy to hear my team was using it for the component.

nickpsecurity 8y ago

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://spinroot.com/spin/whatispin.html http://www.imm.dtu.dk/~albl/promela.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.

Karrot_Kream 8y ago
Which model checkers use Pi Calculus? I've thought about learning Pi Calculus but an much less interested if there's no checker.
pron 8y ago
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 https://www3.hhu.de/stups/prob/index.php/TLA

Sorrop 8y ago

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

uluyol 8y ago

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.

pron 8y ago
You can find some big deductive proofs here: https://members.loria.fr/SMerz/papers.html 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.

pron 8y ago

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

ashish_negi_ 8y ago

Cosmosdb is Microsoft multi model, multi master, geo database with five consistency levels for performance. https://github.com/Azure/azure-cosmos-tla https://github.com/Azure/azure-cosmos-tla

hwayne 8y ago

Yup, here's some good ones! https://github.com/elastic/elasticsearch-formal-models 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#issuecomment-404722753 https://github.com/elastic/elasticsearch/issues/31976#issuec...