От «Код — это закон» до «Спецификация — это закон»: Как формальная верификация может положить конец кризису эксплойтов DeFi на 3,4 миллиарда долларов

Обычная ошибка округления — субцентовая потеря точности в целочисленном делении Solidity — позволила вывести 128 миллионов долларов из Balancer в девяти блокчейнах менее чем за 30 минут. Пулы работали годами. Код прошел множество аудитов. Никто этого не заметил. Таково состояние безопасности DeFi в 2026 году: миллиарды долларов защищены парадигмой, которая наглядно и неоднократно терпела неудачу.

Теперь a16z crypto предлагает радикальное переосмысление. В своем отчете «Big Ideas» за 2026 год венчурная компания утверждает, что индустрия должна отказаться от принципа «код — это закон» — основополагающей веры в то, что развернутый код смарт-контракта является высшей инстанцией — и заменить его принципом «спецификация — это закон», где математически определенные свойства безопасности становятся обязательным стандартом. Этот сдвиг может фундаментально изменить то, как протоколы создаются, проверяются и защищаются.

Проблема на 3,4 миллиарда долларов, которую аудиты не могут решить

Цифры говорят сами за себя. Только в 2025 году криптоиндустрия потеряла более 3,4 миллиарда долларов в результате краж, из которых 1,5 миллиарда пришлось на взлом Bybit. Ошибки в смарт-контрактах нанесли ущерб примерно в 263 миллиона долларов только за первую половину 2025 года. В общей сложности крупнейшие эксплойты в сфере DeFi вывели из протоколов более 10,77 миллиарда долларов.

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

Еще большую тревогу вызывает растущая изощренность атак. Количество эксплойтов с использованием флэш-кредитов резко возросло в 2024 году, составив 83,3 % от всех подходящих случаев. Большинство крупных хакерских атак 2025 года сочетали в себе от двух до четырех типов уязвимостей одновременно. Только северокорейские хакеры украли 2,02 миллиарда долларов в 2025 году, что на 51 % больше, чем в предыдущем году. Злоумышленники становятся умнее быстрее, чем защитники.

Анатомия ошибки округления на 128 миллионов долларов

Эксплойт Balancer заслуживает пристального изучения, поскольку он идеально иллюстрирует, почему принцип «код — это закон» не работает. 3 ноября 2025 года злоумышленник воспользовался математической уязвимостью в том, как пулы ComposableStablePools проекта Balancer обрабатывают свопы на небольшие суммы.

Вот что произошло: когда баланс токенов достигает определенного диапазона (8–9 вэй), целочисленное деление в Solidity вызывает значительную потерю точности. Функция _upscaleArray округляет значение в меньшую сторону при масштабировании, что приводит к занижению инварианта пула — математической константы, которая должна определять справедливые курсы обмена. Это искусственно занижает цену BPT (Balancer Pool Token).

Злоумышленник использовал это, выполнив трехэтапную последовательность свопов в рамках одной транзакции batchSwap, содержащей более 65 операций:

1. Подавление цены: Обмен крупных объемов BPT на базовые токены, что привело баланс одного из токенов к критическому порогу 8–9 вэй, где ошибки округления максимальны.
2. Дешевое приобретение: Минтинг или покупка BPT по искусственно заниженной цене.
3. Полный выкуп: Немедленный обмен BPT на базовые активы по их полной стоимости.

Вся атака была выполнена в конструкторе развернутого смарт-контракта — одной транзакцией, которая вывела 128,64 миллиона долларов в сетях Ethereum, Base, Arbitrum, Avalanche, Optimism, Gnosis, Polygon, Berachain и Sonic. Благодаря быстрому реагированию сообщества удалось вернуть около 19 миллионов долларов, но подавляющая часть средств была потеряна.

Критический урок: это не была какая-то экзотическая уязвимость. Это было нарушение математического инварианта — тип ошибки, которую формальная спецификация выявила бы по определению.

Что на самом деле означает «Спецификация — это закон»

Предложение a16z работает на двух уровнях: статическом (до развертывания) и динамическом (после развертывания).

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

Здесь на помощь приходят инструменты формальной верификации, такие как Certora Prover и K Framework от Runtime Verification. Эти инструменты сопоставляют байт-код смарт-контракта с математическими правилами, определяющими ожидаемое поведение, проверяя каждое возможное состояние контракта и путь выполнения. Certora Prover, например, использует спецификации, написанные на языке CVL (Certora Verification Language), для обнаружения нарушений свойств с помощью статического анализа и решения ограничений.

На динамическом уровне те же самые инварианты становятся активными «ограждениями» — проверками во время выполнения (assertions), которым должна соответствовать каждая транзакция. Если транзакция нарушает основное свойство безопасности, она автоматически отменяется. Это концепция «последней линии обороны»: даже новая, ранее не встречавшаяся атака все равно должна соответствовать фундаментальным свойствам безопасности системы.

Элегантность этого подхода заключается в его асимметрии. Злоумышленники должны найти нарушения, в то время как защитникам нужно лишь определить, как выглядит «правильная» работа. Как заявляют в a16z: «Даже новая атака должна соответствовать тем же свойствам безопасности, которые обеспечивают целостность системы, поэтому единственными возможными атаками остаются незначительные или крайне сложные в исполнении».

Кто уже строит таким образом

Видение «спецификация — это закон» не является чисто теоретическим. Несколько крупных протоколов начали внедрять формальную верификацию как основную часть своего процесса разработки.

Aave, крупнейший лендинговый протокол по объему TVL, интегрировал Certora Prover непосредственно в свой конвейер непрерывной интеграции (CI). Каждое изменение кода автоматически проверяется на соответствие формальным спецификациям перед слиянием. Это не периодический аудит — это математическое доказательство, запускаемое при каждом комите.

Uniswap V2 прошел формальную верификацию своей основной модели маркет-мейкера «x * y = k» с использованием K Framework от Runtime Verification. Верификация охватывала формализацию математической модели, её реализацию в смарт-контракте и символьное выполнение скомпилированного байт-кода для четырех критически важных функций.

Kamino, лендинговый протокол на базе Solana, начал проверять критические инварианты с помощью Certora Prover в начале 2025 года. XRP Ledger также внедрил проверку инвариантов на уровне протокола. Это разработки не только для Ethereum — подход «спецификация — это закон» распространяется на все экосистемы блокчейнов.

ИИ встречает формальную верификацию: AI Composer от Certora

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

В декабре 2025 года компания Certora запустила AI Composer — платформу для написания кода с ИИ и открытым исходным кодом, которая встраивает формальную верификацию непосредственно в процесс генерации кода. В отличие от обычных инструментов ИИ для написания кода, которые приоритезируют скорость, AI Composer гарантирует, что каждый сгенерированный фрагмент кода соответствует математическим правилам безопасности перед выполнением.

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

Этот симбиоз ИИ и верификации также отвечает на замечание a16z о том, что текущая безопасность DeFi должна «систематически доказывать глобальные инварианты, а не верифицировать выбранные вручную локальные». ИИ может исследовать пространство спецификаций шире, чем инженеры-люди, потенциально выявляя тонкие математические нарушения — такие как ошибка округления в Balancer — которые ускользают при ручной проверке.

Юридические и управленческие последствия

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

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

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

Вызовы и ограничения

Тезис «спецификация — это закон» убедителен, но сталкивается с реальными препятствиями.

Полнота спецификации является фундаментальной проблемой. Как формально определить каждое свойство, которое имеет значение? Спецификации пишутся людьми, и люди могут упустить критические свойства — точно так же, как аудиторы пропускают критические баги. Спецификация, которая не фиксирует правильные инварианты, дает ложную уверенность.

Риск компонуемости добавляет еще один уровень сложности. Ценность DeFi заключается во взаимодействии протоколов друг с другом. Формальная верификация инвариантов одного протокола не гарантирует безопасности, когда этот протокол сочетается с другими неожиданными способами. Поверхность взаимодействия между протоколами остается во многом неописанной территорией.

Производительность и стоимость являются практическими проблемами. Формальная верификация требует больших вычислительных ресурсов. Проверка инвариантов во время выполнения (runtime) увеличивает затраты на газ для каждой транзакции. Для высокочастотных протоколов, обрабатывающих тысячи транзакций в секунду, эти затраты имеют значение.

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

Путь вперед

Несмотря на эти вызовы, траектория ясна. Стоимость эксплойтов — 3,4 миллиарда долларов в 2025 году, 10,77 миллиарда долларов в совокупности — делает статус-кво неприемлемым. Страховые рынки, институциональный капитал и регуляторные структуры будут все чаще требовать доказуемых гарантий безопасности.

Конвергенция написания спецификаций с помощью ИИ, зрелых инструментов формальной верификации и инфраструктуры обеспечения соблюдения правил во время выполнения снижает барьер для входа. Когда Aave может запускать Certora Prover при каждом комите, а Kamino может проверять инварианты на Solana, инструментарий перешел из области академических исследований в производственную инфраструктуру.

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

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

BlockEden.xyz предоставляет блокчейн-инфраструктуру API корпоративного уровня, обеспечивающую работу DeFi-приложений в нескольких сетях. По мере того как формальная верификация становится отраслевым стандартом, надежная инфраструктура узлов формирует основу для верифицированного взаимодействия протоколов. Изучите наш маркетплейс API, чтобы строить на инфраструктуре, созданной для эпохи безопасности.