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 implementa

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.