Ethereum: ИИ делает формальную верификацию обязательной

Ethereum опубликовал гостевую серию постов от ведущего разработчика языка Vyper, выступающего под псевдонимом big_tech_sux. Первая запись появилась в аккаунте сети 5 августа 2026 года, развёрнутая версия материала датирована 6 августа 2026 года.

В серии автор описывает формальную верификацию как математический метод доказательства правильности программы для всех возможных сценариев выполнения, в отличие от тестов, которые охватывают лишь часть случаев. В качестве простого примера приводится функция f(x) = x/2, для которой можно математически доказать, что результат никогда не превышает входного значения.

В публикации отмечается, что формальная верификация способна выявлять крайне редкие ошибки, которые не проявляются при обычном тестировании и могут вызвать серьёзные сбои. По словам автора, «формальная верификация может выявить один случай из квадриллиона, который никогда не проявится во время тестирования, но именно он может привести к катастрофическому сбою».

Развитие крупных языковых моделей (LLM) упрощает некоторые этапы работы с формальными доказательствами, считает автор. Он указывает, что ИИ может помочь в создании формальных моделей и выборе инвариантов, однако сам процесс остаётся сложным и требует значительных вычислительных и человеческих ресурсов.

Автор предупреждает о риске ошибок при преобразовании исходного кода в формальную модель: неточности на этом этапе могут привести к неверным выводам и снизить надёжность результатов верификации. В материале подчёркнуто, что применение формальной верификации требует дополнительной валидации и контроля качества модельных представлений программ.

Также в серии обсуждается влияние ИИ на защиту и атаку. Приводится пример, когда экспериментальная модель одной компании обнаружила уязвимости нулевого дня, способные обходить несколько уровней защиты. На этом фоне формальная верификация рассматривается как инструмент, который позволяет доказать устойчивость системы ко всем возможным входным данным, тогда как нападающим достаточно одной последовательности данных для атаки.

Автор делает вывод, что для критического программного обеспечения, включая смарт‑контракты, управляющие большими суммами пользовательских средств, формальная верификация перестаёт быть «опцией, а необходимой предпосылкой». В тексте также напоминается, что тема использования ИИ для верификации кода обсуждалась ранее сооснователем Ethereum Виталием Бутериным.

В публикации содержится предупреждение о том, что массовое внедрение формальной верификации потребует ресурсов и тщательной проверки результатов, и автор призывает учитывать эти ограничения при масштабировании практик верификации для смарт‑контрактов.