A proof of incorrectness of a program can be given by
showing a single input on which the program fails
to give the correct output.

Some mathematical proof techniques operate by looking for counter-examples.
When combined these with the published ProofOfCorrectness for programs
you have a way to ''uncover'' bugs.

This is in tight relation to the falsification theory of philosophy of science.  Also, in its refined forms, it models "positive heuristics" (knowledge of what is good, so where the problem should not be) to know where to look when you have a proof of incorrectness.