When I was working with CompCert, I had no problems producing a formally verified compiler that miscompiled its (meager) test suite. Tests are necessary for "formally verified" systems! You might mess up parts of the specs or the model you are verifying against. You can only catch these problems through testing.