Erratum: testing, of course, exercises every layer you depend on, whereas proof methods typically assume that the things below conform to their contracts. That is where proofs are weak. A proof will show that your code is correct; a test will reveal a compiler bug, CPU bug, faulty RAM, ...