You struggle to even do that. You can normally prove that some code conforms to a version of the specification that is explicitly formalised, but in practice, a large number of bugs are specification bugs and that will only increase the more you are forced to formalise the specification.