Защита от ИИ-багов

Виталик Бутерин опубликовал большой разбор формальной верификации — подхода, при котором корректность программы проверяется через математические доказательства. Его главный тезис: по мере того как ИИ ускоряет поиск уязвимостей, защитникам нужен не только более быстрый аудит, но и более строгий способ доказывать, что критический код делает именно то, что должен.

Для широкой AI-повестки это важно не из-за Ethereum как такового. Бутерин описывает более общий сдвиг: языковые модели могут стать ускорителем для метода, который десятилетиями оставался нишевым, потому что писать машинно-проверяемые доказательства было слишком сложно и дорого.

Что значит «доказать код»

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

Бутерин приводит пример с Lean — языком и средой для машинно-проверяемых доказательств. ИИ здесь полезен не как магический ревьюер, а как помощник в рутинной и сложной работе: переводить человеческую интуицию в форму, которую может проверить детерминированная система. Если доказательство проходит, доверять нужно уже не всей массе кода глазами, а проверенному утверждению о его поведении.

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

Почему это всплыло именно сейчас

Контекст у Бутерина жёсткий: сильные модели уже помогают искать баги, строить цепочки атак и ускорять работу исследователей безопасности. В последние месяцы вокруг Claude Mythos, GPT-5.5 и AI-assisted vulnerability research возникла новая тревога: если атака дешевеет, защита не может оставаться только ручной.

Его ответ не сводится к «запретить ИИ» или закрыть open source. Наоборот, Бутерин спорит с пессимистичным сценарием, где открытые и децентрализованные системы становятся слишком уязвимыми. Он считает, что после болезненного переходного периода защитники могут получить преимущество: уменьшать проверяемое ядро системы, строже ограничивать доверенную часть кода и доказывать свойства самых опасных компонентов.

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

Где граница оптимизма

Бутерин отдельно подчёркивает, что формальная верификация не является панацеей. Можно доказать не то свойство, забыть важное допущение, оставить непроверенной соседнюю часть системы или получить ошибку на уровне железа. Даже проверяющая среда вроде Lean не существует вне риска.

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

Если такой подход станет дешевле благодаря ИИ, последствия выйдут за пределы криптовалют. Он пригодится в платежах, браузерах, мессенджерах, медицинских системах и в самом AI-написанном коде — везде, где «кажется, работает» уже недостаточно.