Comment by Taikonerd
3 years ago
I'm really excited to hear that this is being used in industry. I think I heard that AWS also used TLA+ to find some very subtle bug in S3, too.
3 years ago
I'm really excited to hear that this is being used in industry. I think I heard that AWS also used TLA+ to find some very subtle bug in S3, too.
They've also developed a library that plugs into their actual Rust code to verify it (rather than writing a secondary model in TLA+ or P, it's easier to verify the actual system source code).
See https://github.com/awslabs/shuttle and a whitepaper at https://www.amazon.science/publications/using-lightweight-fo...
Disclaimer: used to work at AWS and had some involvement in this stuff
Yes, indeed. We talk about it here https://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-... (or here https://lamport.azurewebsites.net/tla/formal-methods-amazon.... if you can't access that).