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

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 https://www.adacore.com/press/spark-skein See also: https://www.adacore.com/papers/sparkskein https://www.adacore.com/papers/sparkskein