That doesn't sound right. Automatic proof assistants/verifiers won't approve your proof unless it really is a proof for the model, right?
> there are always errors in the model, at least initially
Agreed.
> There's always an iterative process of refining the model until you are confident in its being good enough. When are you confident it is good enough?
It's true that bugs in the model are a possibility.
More broadly, it's possible for defects to get through a formal software-development methodology. There was an interesting case study done on this. [0] Vastly fewer than if formal methods are not used, but you're still right that ultimately it's not a completely rock-solid guarantee. (And that's not counting things like bugs in the proof-assistant, or bugs in the non-verified compiler you end up using.)
[0] https://www.adacore.com/tokeneer ('Analysis' section is on page 59 of PDF)
See also https://blog.adacore.com/tokeneer-fully-verified-with-spark-... , https://github.com/AdaCore/spark2014/tree/master/testsuite/g...
It is very easy to complete a proof on the wrong model, and there are always errors in the model, at least initially.
There's always an iterative process of refining the model until you are confident in its being good enough. When are you confident it is good enough? That's quite similar to asking "If you don't use formal methods, how do you know when your work is done?"