Виталик Бутерин считает, что ИИ-верификация повысит безопасность кода Ethereum

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

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

Основные моменты

  • Бутерин опубликовал статью об использовании формальной верификации для безопасности блокчейна.
  • В рамках передовых исследований Ethereum разрабатывается подход, при котором код можно писать непосредственно на байт-коде EVM, ассемблере или Lean.
  • Бутерин считает, что ИИ может повысить как эффективность разработки, так и безопасность кода.

Код, корректность которого можно доказать

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

Суть этого подхода заключается в том, чтобы заменить часть традиционной зависимости от разработчиков, аудиторов и тестов строгой верификацией свойств программы. Если доказательство правильно написано и проверено, система получает более весомую гарантию того, что код делает именно то, что от него требуется. Исследователь Йоичи Хираи называет эту модель «конечной формой разработки программного обеспечения».

Где может помочь ИИ

Бутерин считает, что формальная верификация с использованием ИИ может повысить как эффективность кода, так и его безопасность. Это особенно важно для тех частей Ethereum, где одна ошибка может стоить сотни миллионов долларов или подорвать доверие к инфраструктуре. Среди таких модулей он выделяет STARK, ZK-EVM, постквантовые подписи и алгоритмы консенсуса.

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

Грань между ядром и периферией

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

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

Как мы сообщали ранее, Виталик Бутерин предлагает упростить архитектуру узлов Ethereum.

Этот материал может содержать мнения третьих лиц, никакие данные и информация на этой веб-странице не являются инвестиционным советом в соответствии с нашим Отказом от ответственности. Хотя мы придерживаемся строгих Редакционных стандартов, этот пост может содержать ссылки на продукты наших партнеров.
Топ бонусов недели
до $2,500
бонус за депозит для всех клиентов
ПОЛУЧИТЬ БОНУС
Ваш капитал находится под угрозой.