The best part was the section about finding a bug that took 35 steps to show up which got through both code reviews and testing. The ability to catch such obscure stuff is a benefit of formal methods that's been in the literature a long time. Model-checkers like TLA+ and SPIN let it get done with less skill and time than full, formal verification. Further, the properties can be combined with methods like Design-by-Contract and static analysis to knock out problems that show up 80-90% of the time.
Hardly any justification anymore to not be using these tools for most critical software. Even a mainstream company has figured it out. Hopefully, we'll see more adoption. :)
Hardly any justification anymore to not be using these tools for most critical software. Even a mainstream company has figured it out. Hopefully, we'll see more adoption. :)