[l_dopa]

This is exactly why a lot of formal methods work isn't, imho, terribly compelling.

Something like http://vst.cs.princeton.edu/ has a much, much stronger case for enabling "100% correct software".