- Ethereum назвал технологию, которая может усилить безопасность смарт-контрактов в эпоху ИИ.
- Согласно разработчику Vyper, формальная верификация становится критически важной.
- Это помогает обнаруживать ошибки, которые пропускают тесты.
Команда сети Ethereum опубликовала серию гостевых постов ведущего разработчика Vyper под псевдонимом big_tech_sux, посвящённых роли формальной верификации в эпоху быстрого развития ИИ.
0/ По мере того как ИИ-системы становятся более мощными, формальная верификация — дисциплина, использующая математику для доказательства корректности компьютерных программ — демонстрирует все большую перспективу.
— Ethereum (@ethereum) 5 августа 2026
Гостевой пост от @big_tech_sux, ведущего разработчика @vyperlangpic.twitter.com/3T6H76AVrL
Автор утверждает, что прогресс в области LLM делает математические доказательства корректности программ более доступными, и для смарт-контрактов, управляющих миллиардами долларов, формальная верификация постепенно становится необходимостью.
Искусственный интеллект меняет подход к верификации программного обеспечения
Серия постов объясняет, что формальная верификация — это математический метод, позволяющий доказать корректную работу программы во всех возможных сценариях выполнения, а не только в тех, которые покрываются тестами.
В качестве примера автор привёл функцию f(x) = x/2, для которой можно математически доказать, что результат никогда не превысит входное значение.
По его словам, эта методология позволяет обнаруживать чрезвычайно редкие ошибки, которые практически невозможно выявить с помощью традиционного тестирования.
«Формальная верификация может выявить один случай из одного квадриллиона крайних ситуаций, которые никогда не возникнут во время тестирования — и именно этот случай может привести к катастрофическому сбою», — отметил автор.
В то же время он признал, что до недавнего времени использование этого подхода требовало больших команд экспертов, которые создавали математические модели программ и проводили сложные доказательства.
С точки зрения разработчика, современные ЯП значительно упрощают этот процесс по мере приближения к ИИ общего назначения.
В то же время автор подчеркнул, что даже с использованием ИИ формальная верификация остается сложным и ресурсоемким процессом. В частности, преобразование исходного кода в формальную модель может вносить неточности, влияющие на надежность результатов.
Развитие ИИ меняет баланс между атакой и защитой
Статья отмечает, что развитие искусственного интеллекта одновременно повышает эффективность как защитников, так и нападающих.
Автор вспомнил инцидент, в котором нерелизная модель OpenAI смогла обнаружить уязвимости нулевого дня, позволившие обойти несколько уровней защиты.
На этом фоне формальная верификация, по мнению автора, позволяет сдвинуть преимущество в пользу защитников.
«Пока атакующим достаточно найти одну последовательность входных данных, позволяющую им взломать систему, защитникам можно использовать формальную верификацию для доказательства устойчивости против всех входных данных», — подчеркнул он.
Поэтому для программного обеспечения, критически важного для работы, включая смарт-контракты, управляющие миллиардами долларов пользовательских средств, формальная верификация становится «не опцией, а необходимым условием».
Стоит отметить, что это продолжает обсуждение, ранее начатое сооснователем Ethereum Виталиком Бутериным относительно использования ИИ для формальной верификации кода.
Сообщение Ethereum Explained How AI Changes Approach to Smart Contract Security появились сначала на INCRYPTED.