Даже формально верифицированный компилятор может ошибаться
В 2011 году исследователи тестировали CompCert случайно сгенерированными C-программами и нашли wrong-code баг в таком выражении:
return -1 <= (1 && x);
Правильный результат — 1, но CompCert 1.6 для PowerPC возвращал 0.
Ошибка оказалась не в доказанно корректном оптимизаторе, а в неверифицированном фронтенде.
Формальная верификация защищает только те части системы, для которых действительно построено доказательство.
3
2
2
1July 31, 2026 3.2K 8
