Probably proofs matters, as well as formal matters, are insufficient. The solution lies trying to choose small perception that are adequate set of test cases and test the software using these test cases. Of course the crucial issue is the sufficient and adequate set of test cases. If the test cases are not adequate, then the testing is not complete, the quality of the software would be very poor. If we wanted to see that is adequate and sufficient, the issue is: how do we know what is sufficient and what is adequate? Of course we can look at the test cases, we can classify them according to the criteria of the adequacy.