Формальная верификация — звучит как святой Грааль программирования. Доказано математически, что программа работает правильно — значит, она безошибочна, верно? Увы, реальность сложнее. В своей статье “Three ways formally verified code can go wrong in practice” исследователь Хиллел Уэйн показывает, почему даже “доказанный” код может падать, и не просто из-за плохих программистов, а из-за самой природы доказательств.
🧠 Ошибка первая — недействительное доказательство
Иногда «верифицированный» код оказывается ошибочным просто потому, что доказательство некорректно.
🧩 Бывает, что формальный инструмент — Coq, Lean, Isabelle — сам содержит баг. Редко, но случается.
⚙️ Чаще — программист добавляет в доказательство “заглушку”: admit или sorry, обещая доказать позже. Компилятор пропускает её, и код выходит с дырой.
📚 На бумаге всё красиво, но в бинарнике — бомба замедленного действия.
Это напоминает ситуацию, когда тестировщик пишет “TODO: добавить тест на границы” — и через год на продакшне ловит undefined behavior.
📜 Ошибка вторая — неправильные свойства
Формальная верификация всегда проверяет, что код соответствует спецификации, но не гарантирует, что спецификация правильна.
Возьмём простой пример:
inc :: Int -> Int
inc x = x - 1
Функция доказанно корректна — ведь она соответствует типу Int -> Int. Но явно делает не то, что мы хотим.
📏 Формально всё верно, но по сути — бессмысленно.
Такая ловушка особенно часто встречается в системах, работающих с Unicode, сетевыми протоколами и интерфейсами пользователя. Как доказать, что «строки визуально выровнены», если ширина символов зависит от шрифта, ОС и даже языка?
🧩 И это не шутка: один из примеров в статье — “доказанный” leftpad, который ломается на ивритских символах. Unicode — это ад, где формальная логика бессильна.
🌍 Ошибка третья — неверные предположения
Самая тонкая и коварная категория.
Любое доказательство говорит: “Если условие Y выполняется, то свойство X верно”.
Но что, если Y — это «входной список отсортирован», а кто-то подал на вход хаос?
✅ Код доказанно корректен при правильных входных данных.
💥 В реальности — падает, потому что предположение нарушено.
Формальная верификация часто строится на таких допущениях:
🧮 “ОЗУ достаточно” — но система на Raspberry Pi;
🧵 “Нет гонок между потоками” — но кто-то добавил асинхронный вызов;
💾 “Компилятор не изменит поведение” — но обновление LLVM внесло оптимизацию.
И вот — “доказанный” код начинает чудить, хотя формально он по-прежнему идеален.
🔍 Моё мнение
Формальная верификация — это как страховка: она защищает от известного круга рисков, но не от падения метеорита.
Она незаменима в системах, где ошибка стоит жизни — авионика, ядерные реакторы, криптография.
Но когда её переносят в повседневное программирование, нужно помнить: доказательство — не истина, а контракт. И если одна сторона (например, окружение) нарушает условия, всё рушится.
На мой взгляд, будущее в гибридных методах — сочетании формальной логики с машинным обучением и динамическим анализом, где система не просто “доказывает”, а понимает контекст и проверяет допущения в реальном времени.
🔗 Источники
📘 Three ways formally verified code can go wrong in practice
💡 Let's Prove Leftpad — проект, упомянутый автором
📙 Logic for Programmers (книга Хиллела Уэйна)
⚡ Формальная верификация не отменяет ошибок — она просто делает их более интеллектуальными.