[crote]

I fear it'll just move the problem one layer up. Sure, you've now proven that the code matches the specification - but how do you ensure the specification is watertight?