> I'm kind of skeptical of formal verification. This doesn't stand up. In the software world, both the Sel4 [0] and CompCert [1] projects have surprised resear

> I'm kind of skeptical of formal verification. This doesn't stand up. In the software world, both the Sel4 [0] and CompCert [1] projects have surprised researchers unaccustomed to encountering bug-free software. The non-verified alternatives to both systems were always found to be buggy. For an interesting case-study on the use of formal methods, and their effectiveness, take a look at [2]. > your spec can still be incomplete or buggy Spec bugs are possible, but empirically they're much less of a problem than ordinary implementation bugs. [2] has good discussion of this topic. > At the end of the day, there's no substitute for extensive real-world testing. That's backward. Testing is no substitute for formal methods. Testing is never exhaustive. I don't think formal methods are often used in the complete absence of testing. [0] https://www.newscientist.com/article/mg22730392-600-unhackable-kernel-could-keep-all-computers-safe-from-cyberattack-2/ https://www.newscientist.com/article/mg22730392-600-unhackab... [1] https://compcert.org/motivations.html https://compcert.org/motivations.html [2] https://www.adacore.com/tokeneer https://www.adacore.com/tokeneer