На Software Engineering Stack Exchange спросили о барьерах для внедрения формальных методов. Вопрос закрыли как субъективный, а ответы свелись к «дорого» или «это не самолёт». Проблема глубже. В сообществе формальных методов нет единства терминов. Автор делит область на спецификацию кода (CS) и его верификацию (CV), а также на спецификацию дизайна (DS) и его верификацию (DV), и сразу замечает: разговор пойдёт о полной верификации обычного софта, а не только критического, где формальные методы тоже почти не применяются.
С кодом главная беда — получить спецификацию и доказать её. Спеки записывают отдельными теоремами (Isabelle, ACL2), вшивают в код утверждениями (Hoare Logic, Euclid, Design by Contract, SPARK, Dafny) или выражают через зависимые типы (Coq, Agda). Но доказательства чудовищно трудоёмки. Нужно строго формализовать даже ассоциативность сложения, а переполнение в C++ ломает доказательство на корню. Ранние верификаторы работали с урезанными подмножествами языков вроде Lisp и Pascal. Ситуацию улучшили SMT-решатели, превращающие творческую задачу в вычислительную: в 1998 появился Stanford Validity Checker, в 2002 — CVC, а революцию произвёл Z3 от Microsoft Research, сделавший автоматическое доказательство доступнее. Однако даже с продвинутыми решателями проект IronFleet на Dafny выдал 5000 строк верифицированного кода за 3,7 человеко-года — четыре строки в день.
Полная верификация кода почти никому не нужна: типы, тесты и практики вроде Cleanroom снижают плотность дефектов ниже 1 бага на тысячу строк кода без всяких доказательств. Частичная верификация реальнее — например, доказательство отсутствия неопределённого поведения в C или встроенные гарантии в Rust (безопасность памяти) и Pony (безопасность исключений), но такие языки создаются скорее экспертами по языкам, а не формальными методами.
С дизайном иначе. Верификация дизайна (DV) оперирует не строками кода, а взаимодействием компонентов. Здесь правят model checker’ы — они перебирают пространство состояний и выдают контрпримеры без написания доказательств. Памела Заве с помощью Alloy нашла фундаментальную ошибку в Chord, а AWS отлавливает 35-шаговые баги спеками на TLA+. Главный враг — комбинаторный взрыв, но его лечат оптимизациями и железом. Технически модель-чекинг проще, однако тормозит его социальный барьер: программисты не доверяют артефактам, которые не являются кодом, и считают свои псевдокод и диаграммы достаточными. Поэтому верификация кода останется нишевой, а верификацию дизайна сдерживает культурная инерция, которую, впрочем, можно преодолеть.