Виталик Бутерин: AI-верификация — финальная форма безопасной разработки
Сооснователь Ethereum Виталик Бутерин опубликовал 18 мая программное эссе, в котором обосновал тезис: AI-ассистированная formal verification способна стать главным инструментом кибербезопасности в эпоху, когда искусственный интеллект делает поиск уязвимостей кратно дешевле для атакующих. Текст вышел на фоне растущей тревоги по поводу того, что AI ускоряет именно сторону атаки, а не защиты.
Суть подхода — в том, что разработчик пишет не просто код, а математическое доказательство, гарантирующее: программа ведёт себя именно так, как задумано, при любых входных данных. Метод известен с 1960-х, но всегда оставался нишевым из-за чудовищной трудоёмкости ручного написания доказательств. Бутерин аргументирует, что AI меняет это уравнение радикально — модели могут одновременно генерировать и код, и проверочные доказательства, оставляя человеку лишь проверку постановки задачи.
В эссе Бутерин цитирует исследователя Йоичи Хираи, называющего связку AI + formal verification «финальной формой разработки софта». Сооснователь Ethereum перечисляет несколько направлений, где этот подход уже встраивается в экосистему — от верификации EVM до доказательств корректности криптографических примитивов. По его словам, итог может быть экстремально эффективным и кардинально более безопасным, чем нынешняя практика «писать код и надеяться».
Параллельно сама Ethereum Foundation проходит через волну уходов: 18 мая о выходе из организации объявили исследователи Карл Бик (после 7 лет работы) и Джулиан Ма (после 4 лет). Это продолжение многомесячного оттока, который уже включал Барнабе Монно, Тима Бейко, Трента Ван Эппса и Алекса Стокса — на фоне внутренней реорганизации фонда и пересмотра его роли в экосистеме.
Контекст показателен: пока сообщество спорит о направлении фонда, технический фронт Ethereum двигают не институциональные структуры, а отдельные исследователи и разработчики. Эссе Бутерина — попытка задать долгосрочную повестку безопасности для всего Web3, а не только для ETH. Если связка AI-генерации и математической верификации действительно станет стандартом, это меняет экономику аудита смарт-контрактов — направления, где сейчас ежегодно теряются сотни миллионов долларов.
