You can prove the code correct against the spec. However you can't prove that the spec will do what you expect it to do because the spec is where the intersecti

You can prove the code correct against the spec. However you can't prove that the spec will do what you expect it to do because the spec is where the intersection with the real world occurs. Therefore, you must test the spec. Everything that falls under the spec can be formally verified to 100% correctness.