Mathematically correct is not enough.

Java's byte code verification algorithm had a proof. This was important for running untrusted java in the browser. If it said the byte code was ok, it was.

Turns out, nobody made a proof for the verifier actually finishing. So it could return true, or false, or run longer than the universe has time. So around Java 6(?), someone wrote some bytecode that basically took forever to validate, DOSing the validator. Sun had to change the file format and add extra information to get the guarantees back.