Занятная статья про 2 основные аспекта формальной верификации: дороговизну и сложность формализации. И если первый аспект можно закидать деньгами, вычислительными ресурсами и теперь еще ИИ (который уже может нагенерить, например, формальное доказательство для теоремы Ферма), то понять, а как, собственно, система должна себя вести, все еще очень тяжело (за редкими исключениями). Спецификацию сейчас не для каждого языка программирования можно найти, а для чего-то более приближенного к бизнесу если что-то и будет задокументировано, то информация о поведении будет размазана по документации, тикетам, коду, презентациями, тестам и т.п. Но даже если собрать это все в одном месте и начать формализовывать, то появляется куча вопросов про сценарии. А бизнес на большинство и не знает ответа, или ему вообще пофиг, что будет в этом случае.

Еще одна проблема заключается в строго следовать спецификации тупо невыгодно. Это разобрано на примере PDF читалок: лучше как-то криво отобразить сломанный документ, чем сказать “ой, не по спецификации” и ничего не делать (закон Постела).

В общем, хотя формальная верификация и стала более доступной, она все еще слабо применима на практике.