> But in practice, it's easy to make a simple mistake in implementation and accidentally throw your proof out the window.

But that's not how a proof of correctness works. You have an implementation (of an algorithm, say) and you prove mathematically that it is correct with respect to a formal specification. The implementation and proof aren't separate things.