3 ms·
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 "a
by 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 agoThe 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 agoIndeed. As I recall, he was really happy to hear my team was using it for the component.