Also, I believe there is no substitute for testing, regardless of how the program itself was derived. Failures can arise in a provably correct program if the input specification itself was misinterpreted! So verify all you want. As someone who cares about software quality, you've got to test the heck out of it.