John Regehr observed a proven-correct C compiler generating incorrect code.  The reason?  An error in a system header file.  The truth of the matter is that for most of the software systems formally proving every single piece of the system to be correct is too expensive.  Perhaps as the rate of change in the software industry inevitably slows, this will change, as slower change will increase re-usability, but at the moment it is the sad state of things.