Соучредитель сети Ethereum Виталик Бутерин обозначил перспективный вектор развития индустрии: интеграция инструментов искусственного интеллекта в процессы поиска уязвимостей и написания кода способна фундаментально укрепить защищённость блокчейн-инфраструктуры и децентрализованных приложений.
В своей публикации «Краткий обзор формальной верификации» Бутерин констатировал растущий интерес к методологиям программирования на языках экстремально низкого уровня — в частности, к байт-коду Виртуальной машины Эфириума (EVM) и функциональному языку Lean. Ключевая особенность подхода — использование автоматически верифицируемых математических доказательств, сформулированных на Lean, для строгой проверки корректности кода.
По убеждению предпринимателя, при грамотной имплементации данный метод способен обеспечить качественно более высокий уровень безопасности по сравнению с традиционными практиками разработки. Бутерин подчёркивает: формальная верификация — то есть математическое доказательство отсутствия ошибок до момента их эксплуатации злоумышленниками — может стать эффективным щитом для Эфириума и иных распределённых реестров.
Современные ИИ-инструменты, отмечает сооснователь Ethereum, демонстрируют растущую способность обнаруживать латентные дефекты кодирования и критические уязвимости в смарт-контрактах, которые могут остаться незамеченными при ручном аудите. При этом ИИ не позиционируется как замена разработчику, а рассматривается как мультипликатор эффективности: аналитики и инженеры уже используют алгоритмы не только для идентификации угроз, но и для ускоренной генерации безопасного кода.
Бутерин сослался на оценку бывшего инженера Ethereum Foundation Йоичи Хираи, охарактеризовавшего подобную парадигму как «финальную форму разработки программного обеспечения». Хираи, ранее занимавшийся безопасностью смарт-контрактов Эфириума, покинул фонд в 2018 году на фоне дискуссий вокруг стандарта EIP-867, который, по его мнению, мог вступать в противоречие с японским законодательством.
Вместе с тем Бутерин предостерёг: в случае использования аналогичных ИИ-инструментов злоумышленниками, последние получат возможность выявлять программные ошибки в сжатые сроки, что создаст новые векторы атак для всей блокчейн-экосистемы. В связи с этим сооснователь Эфириума призвал разработчиков придерживаться более строгих стандартов: применять надёжные методы верификации, осваивать безопасные языки программирования и внедрять усиленные протоколы контроля качества кода.