Бутерин утверждает, что формальная верификация ИИ повышает безопасность криптовалюты

Бутерин публикует новый пост о ИИ и безопасности кода

Сооснователь Ethereum Виталик Бутерин опубликовал блог 18 мая 2026 года на vitalik.eth.limo. В нем он утверждает, что формальная верификация с помощью ИИ станет одним из самых важных инструментов кибербезопасности. Формальная верификация — это метод, который использует математические доказательства для подтверждения того, что программное обеспечение ведет себя именно так, как задумано. Бутерин утверждает, что сочетание ИИ и формальной верификации поможет разработчикам находить уязвимости до того, как это сделают злоумышленники.

Клод Мифос назван примером силы ИИ

Бутерин называет Клода Мифоса, модель ИИ, разработанную Anthropic, примером все более мощных систем ИИ. Он утверждает, что такие системы могут ускорить обнаружение и эксплуатацию уязвимостей. Клод Мифос — это реальная модель. Anthropic подтвердила его существование после случайной утечки данных в марте 2026 года. Превью модели было выпущено для избранных партнеров в апреле 2026 года.

Бутерин перечисляет ограничения формальной верификации

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

Проект Arklib нацелен на верифицированную реализацию STARK

Бутерин выделяет Arklib как конкретный пример применения формальных методов к Ethereum. Arklib — это проект с открытым исходным кодом, который нацелен на создание полностью формально верифицированной реализации системы доказательства STARK. STARK — это тип криптографического доказательства, используемого в инфраструктуре масштабирования Ethereum. Фонд Ethereum профинансировал Nethermind для расширения Arklib с формализацией протокола FRI в помощнике доказательства Lean. Бутерин также упоминает формально верифицированные реализации Ethereum Virtual Machine, написанные непосредственно на ассемблере RISC-V.