Сооснователь Ethereum Виталик Бутерин 18 мая опубликовал углублённый анализ, посвящённый текущему состоянию и перспективам технологии формальной верификации (Formal Verification). Он считает, что формальная верификация с помощью ИИ станет «конечной стадией» разработки ПО, и указывает, что Ethereum станет важной частью будущей архитектуры «безопасного ядра».
Ключевые принципы формальной верификации и области применения
Как подтверждается в статье Виталика, формальная верификация особенно подходит для сценариев, где «цель намного проще реализовать, чем» — он явно перечисляет четыре ключевых компонента технологий, которые станут частью следующего этапа обновления Ethereum:
Квантоустойчивые подписи: уже ведутся работы по формальной верификации вариантов подписей SPHINCS
Система доказательств STARK: проект Arklib нацелен на создание полностью формально верифицируемой реализации STARK
Алгоритм консенсуса с византийской отказоустойчивостью: в настоящее время ведётся работа по формальному заданию и доказательству безопасностных свойств консенсуса Lean
ZK-EVM: проект evm-asm стремится построить полностью формально верифицируемую реализацию EVM (непосредственно используя RISC-V ассемблер)
Виталик цитирует высказывание Ёити Хираи и называет этот подход «конечной стадией разработки ПО».
Направления эволюции «безопасного ядра», описанные Виталиком
Как подтверждается в статье Виталика, он описывает модель эволюции будущей программной архитектуры:
Безопасное ядро: посредством формальных методов его безопасность постоянно усиливается, и оно несёт максимальный уровень доверия; Виталик прямо отмечает, что Ethereum, ядро операционных систем и связанные с IoT приложения станут «безопасным ядром».
Небезопасная периферия: периферийные компоненты работают в песочнице, получая минимальные полномочия, необходимые для выполнения задач; если периферийный компонент выходит из строя, безопасное ядро обеспечивает защиту.
Ограничения подтверждения и сценарии провала формальной верификации
Виталик признаёт, что формальная верификация не является панацеей. Ссылаясь на работы исследователей, включая Надима Кобейси (Cryspen), он подтверждает три основные категории сценариев провала: неполное верифицирование (верифицируется только часть кода, а не верифицированная часть содержит критические дефекты); упущения в спецификации (ошибки в самой безопасностной спецификации или неверные допущения внутри доказательства); атаки по побочным каналам (атаки через побочные каналы на границе между программным и аппаратным обеспечением сложно выявлять существующими моделями).
Виталик подчёркивает, что «доказуемая корректность» по своей сути верифицирует внутреннюю согласованность между различными способами выражения намерений, а не абсолютное соответствие намерениям реальных людей.
Инструменты подтверждённой AI-помощи для формальной верификации
Как подтверждается в статье Виталика, доступные инструменты: Lean (язык математических доказательств, который позволяет автоматически верифицировать теоремы); Claude и Deepseek 4 Pro (Виталик подтверждает, что их достаточно, чтобы использовать для написания Lean-доказательств); Leanstral (модель с открытыми весами на 119 млрд параметров, специально дообученная под написание на Lean, которую можно запускать локально; результаты бенчмарков превосходят многие универсальные модели большего масштаба).
Частые вопросы
Почему Виталик считает, что Ethereum должен стать «безопасным ядром»?
Согласно статье Виталика, Ethereum похож на ядро операционной системы: он несёт в себе высочайший уровень доверия в процессе цифровизации общества. Он отмечает, что цель проектирования безопасного ядра — добиться уровня безопасности, при котором не допускается разрастание потока багов в коде, и направить всю дополнительную вычислительную мощность, привнесённую ИИ, на повышение безопасности безопасного ядра.
Почему формальная верификация особенно подходит для STARK, ZK-EVM и подобных технологий?
Согласно анализу Виталика, у этих технологий есть общая особенность: «цель намного сложнее реализации» — их свойства безопасности можно чётко определить математическим языком, но конкретная реализация крайне сложна, и именно в таких условиях формальная верификация проявляет себя сильнее всего.
Как Виталик советует разработчикам использовать AI-помощь для формальной верификации на практике?
Согласно статье Виталика, он рекомендует поручить ИИ написание Lean-кода и математических доказательств, а пользователю в итоге нужно лишь проверять, что доказанные утверждения соответствуют ожиданиям, без необходимости самостоятельно писать громоздкий нижнеуровневый код доказательств. Он подтверждает, что Claude, Deepseek 4 Pro и Leanstral — это основные доступные сейчас инструменты.
