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?
Is it cheaper to hire someone who knows TLA+ or to find a consultant?
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+.
https://perspectives.mvdirona.com/2014/07/challenges-in-desi...
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.
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.
Along with someone fixing a bug well before someone found the bug in the wild: https://github.com/elastic/elasticsearch/issues/31976#issuec...
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.