Didn't they find a vulnerability like this in the official MD5 implementation when they tried to port it to SPARK/Ada and the proofs didn't work? I wasn't able to just find it with web search, but here's a release about something similar happening with another one of the SHA3 candidates (Skein), before Keccak was chosen:

https://www.adacore.com/press/spark-skein

See also: https://www.adacore.com/papers/sparkskein