EXACTLY this. It'll be like - oh we proved it using X, but wrote code using Y and ooops, there is some difference so this doesn't count as a break in the proof.

EXACTLY this. It'll be like - oh we proved it using X, but wrote code using Y and ooops, there is some difference so this doesn't count as a break in the proof. If that's the case, you have not in fact proved the contract, you've proved a different contract or code base.