3 ms·
Yes, since we published this (I'm one of the authors), the Automated Reasoning Group have done amazing work applying formal methods to a broad range of problems
by mjb 7y ago
Yes, since we published this (I'm one of the authors), the Automated Reasoning Group have done amazing work applying formal methods to a broad range of problems at AWS. We're also still using TLA+ in many places for the reasons the paper describes.
One aspect of TLA+ (and formal specifications in general) that I under appreciated when we wrote this was how useful they are as a communication tool. I've found well-commented TLA+ to be an excellent medium for reviewing and documenting protocols, and having high-bandwidth conversations about them. Complex protocol interactions can be hard to describe clearly in text, but the mix of text and TLA+ (or PlusCal) seems to work well.
- exdsq 7y agoIs TLA+ only ever used as a tool by developers or do you have "formal methods" engineers who are only involved with that step of the process?
- amortize_ 7y agoDoes your team hire PhDs with formal verification backgrounds? If so, what is the interview process like? Do you make them go through the standard leetcode type interviews?