to be fair it's not just the problem with formal methods work - if you start off with a spec with a bug and implement it faithfully in a non-verified context, y

to be fair it's not just the problem with formal methods work - if you start off with a spec with a bug and implement it faithfully in a non-verified context, you'll still have the bug due to the buggy spec, along with a whole bunch of implementation bugs that you make due to not verifying things...