Спецификаций не существует: почему формальная верификация не спасёт мир

Specifications Don't Exist (2025)

Статья Майка Доддса из Galois о том, что формальная верификация упирается не в стоимость доказательств, а в отсутствие самих спецификаций. Автор объясняет, почему компиляторы и криптобиблиотеки поддаются верификации, а веб-браузеры и PDF — нет. На примере проекта DARPA SafeDocs он показывает, что даже для такого стандартизированного формата, как PDF, невозможно создать точную и непротиворечивую спецификацию. В итоге он приходит к выводу, что с развитием ИИ, когда доказательства станут дешёвыми, главной проблемой станет формулировка требований.