In most domains you're always going to have the possibility of a gap.

The real thing though, is that if you have a verified formal model and a buggy implementation, then _you know_ your problem is at that model <-> implementation level.

Could be the implementation is wrong. Could be that the "bug" is in fact not a bug according to your model. But your model isn't "wrong". If your model says that A happens in condition B, then that is what should happen!

You can avoid second guessing a lot of design patterns with models, and focus on this transitional layer.

If someone came up to you and said "I built a calculator and with this calculator 1/0 becomes 0" you don't say "oh... maybe my model of division is wrong". You think the calculator is wrong in one way or another.

Maybe the calculator's universe is consistent in some way but in that case its model is likely not the same model of division you're thinking of. This eliminates entire classes of doubt.

There are two DIFFERENT gaps here. You're talking about the gap where what you have verified is a model, and the actual code and the model may diverge. But there is another, subtler gap: how good are you at coming up with properties? Because your verification is only as good as the properties you come up with, and the average programmer is not great at coming up with properties. (Before people attack me, I should make clear I've been working in formal methods for 3 decades now.)

That's called specification-, model-, or property-based test generation. Google those terms. If older security or verification papers, always try adding "citeseerx" and "pdf" to the search to find research publications.

The papers will describe the strengths and weaknesses of those tools.