This is exactly why a lot of formal methods work isn't, imho, terribly compelling. Something like http://vst.cs.princeton.edu/ http://vst.cs.princeton.edu/ has

This is exactly why a lot of formal methods work isn't, imho, terribly compelling. Something like http://vst.cs.princeton.edu/ http://vst.cs.princeton.edu/ has a much, much stronger case for enabling "100% correct software".