Даже верифицированный компилятор может допускать ошибки. В 2011 году…

Даже верифицированный компилятор может допускать ошибки. В 2011 году исследователи тестировали CompCert с использованием случайно сгенерированных C-программ и обнаружили ошибку "wrong-code" в следующем выражении:

return -1 <= (1 && x);

Правильный ответ — 1, но CompCert 1.6 для PowerPC выдал 0. Ошибка оказалась не в корректном оптимизаторе, а в неверифицированном фронтенде. Формальная верификация защищает только те части системы, для которых есть доказательства.