> [citation needed] Watch Xavier Leroy's talks. > IMO, sel4's really cool part isn't that it just was formally verified, but it's total design specifically f

> [citation needed] Watch Xavier Leroy's talks. > IMO, sel4's really cool part isn't that it just was formally verified, but it's total design specifically for verifiability. Well, they were very selective with their algorithm choices, so that only very simple algorithms were used. Whether that's cool or an unaffordable restriction depends on your perspective. > The argument reminds me of all the people in the late 90s talking about how unit tests would never take off because they tried to introduce it in their legacy spaghetti codebase, and it wasn't amenable to testing. Except that I've been both practicing and evangelizing formal methods for some years now. I argue in favor of using them, not against, but as someone with some experience in that field I want to make sure people's expectations are reasonable. Unreasonable expectations all but killed formal methods once before.