I would also add that, although there is no algorithm that proves the correctness of software, if you use correctly the right tools you can have very tight software. The first thing that comes to my mind is SPARK ( http://en.wikipedia.org/wiki/SPARK_(programming_language) ) a subset of Ada that can be used to formally prove the correctness of software.
Of course, you could make a mistake in the formal specs of your code, but I expect that the probability of making two complementary mistakes (in the code and in the spec) so that they pass the formal check, is quite low...
Authored Comments
I would also add that, although there is no algorithm that proves the correctness of software, if you use correctly the right tools you can have very tight software. The first thing that comes to my mind is SPARK ( http://en.wikipedia.org/wiki/SPARK_(programming_language) ) a subset of Ada that can be used to formally prove the correctness of software.
Of course, you could make a mistake in the formal specs of your code, but I expect that the probability of making two complementary mistakes (in the code and in the spec) so that they pass the formal check, is quite low...