Exactly - these formal methods have implicit assumptions in them. Within their axioms/priors they are proven correct. But the devil is in those assumptions. And that is disregarding the rather foggy notion of 'proof'. Is this proof written in a formal proof system that automates the proof? Because if it isn't you have another source of error. Even if it is in a formal proof system, who is to say that there is no error in the formal proof system? I admit that each layer adds more assurance - but appealing to 'formal proof' is a bit like appealing to god, it's an appeal to an unassailable authority. When in fact, once you know the details these things are never so clear cut.