4 ms·
>complex distributed systems amazon has been using TLA+ to prove/check correctness of production distributed algorithms and systems for about a decade
by Palomides 7y ago
>complex distributed systems
amazon has been using TLA+ to prove/check correctness of production distributed algorithms and systems for about a decade
- dekhn 7y agoSure, here's an example: https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon.... They still have to let users know about rare bugs that led to data corruption. You'll generally formal proof checking applied to simplified model systems of individual components, while interesting failures tend to involve ten or more components.
- redis_mlc 7y ago> amazon has been using TLA+ to prove/check correctness of production distributed algorithms and systems for about a decade Such an in-your-face, smug and flippant comment but ... On some projects. In some teams. And Aurora lost a lot of data initially in spite of whatever TLA+ they were using, somewhere at Amazon.