Sui Prover становится проектом с открытым исходным кодом: почему формальная верификация — это недостающее звено в безопасности смарт-контрактов

В 2025 году сектор DeFi потерял 3,3 миллиарда долларов из-за эксплойтов смарт-контрактов — несмотря на то, что большинство атакованных протоколов прошли аудит, а некоторые даже несколько раз. Взлом Bybit на 1,5 миллиарда долларов в феврале, эксплойт GMX на 42 миллиона долларов и бесчисленные атаки повторного входа (reentrancy) доказали неудобную истину: традиционные аудиты безопасности необходимы, но недостаточны. Когда важна математическая точность, тестирования пограничных случаев недостаточно. Их нужно доказывать.

Вот почему переход Sui Prover на открытый исходный код значит гораздо больше, чем очередной релиз на GitHub. Разработанный компанией Asymptotic и теперь свободно доступный сообществу разработчиков Sui, Sui Prover внедряет формальную верификацию — ту же математическую технику, которая гарантирует надежность систем управления полетами и архитектур процессоров — в повседневную разработку смарт-контрактов. В условиях, когда один упущенный пограничный случай может привести к потере сотен миллионов, возможность математически доказать корректность поведения кода перестает быть роскошью. Она становится необходимостью.

Парадокс аудита: когда «безопасно» — недостаточно безопасно

Ландшафт безопасности блокчейнов в 2025 году выявил тревожную закономерность. Согласно отчету Halborn «Top 100 DeFi Hacks», протоколы, прошедшие строгие аудиты, все равно становились жертвами эксплойтов. Причины были разными: уязвимости в цепочке поставок, недостатки контроля доступа, тонкие математические ошибки в экономических моделях. Но общей чертой было то, что традиционный анализ кода — будь то ручная проверка или автоматическое сканирование — не мог выявить все возможные сценарии сбоев.

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

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

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

Что на самом деле делает формальная верификация

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

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

Затем инструмент верификации (проверщик) — в данном случае Sui Prover, построенный на движке верификации Boogie и SMT-решателе Z3 — исчерпывающе проверяет, удовлетворяет ли код этим спецификациям при всех возможных входных данных. В отличие от тестирования, которое проверяет конкретные значения, Sui Prover оценивает код сразу для всех возможных вариантов через математические рассуждения.

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

Язык программирования Move, используемый в Sui и Aptos, с самого начала разрабатывался с учетом формальной верификации. Его ресурсоориентированная модель и строгая статическая типизация обеспечивают фундамент, который делает формальную верификацию более практичной, чем в таких языках, как Solidity. Язык спецификаций Move (MSL) позволяет разработчикам выражать три категории свойств:

• Инварианты структур (Struct Invariants): какое состояние структура должна поддерживать на протяжении всего своего жизненного цикла.
• Спецификации функций (Function Specifications): предусловия, постусловия и гарантии поведения для каждой функции.
• Спецификации глобального состояния (Global State Specifications): общесистемные свойства, которые должны сохраняться при всех переходах состояний.

Sui Prover: от внутреннего инструмента к ресурсу сообщества

Компания Asymptotic изначально разработала Sui Prover для поддержки своей аудиторской работы над протоколами, строящимися на Sui. Будучи единственным поставщиком услуг формальной верификации на Sui, им требовались инструменты, способные выйти за рамки ручного анализа для математической проверки зон высокого риска в коде клиентов.

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

Sui Prover доступен на GitHub и может быть установлен через Homebrew (brew install asymptotic-code/sui-prover/sui-prover). Активная разработка продолжается, а последние задачи, открытые в январе 2026 года, касаются текущих улучшений.

Что делает Sui Prover особенно ценным, так это его интеграция с существующим процессом разработки на Sui Move. Разработчики могут добавлять спецификации в свой существующий код постепенно, сначала верифицируя критически важные функции и постепенно расширяя покрытие. Спецификации выполняют двойную роль: они служат и проверками безопасности, и документацией — любой, кто проверяет или интегрирует контракт, может прочитать спецификации, чтобы понять гарантированное поведение системы.

Свойства из реального мира, которые можно доказать

Сила формальной верификации становится осязаемой, когда вы рассматриваете конкретные свойства, которые можно доказать:

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

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

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

Гарантии контроля доступа: Доказательство того, что только авторизованные адреса могут вызывать привилегированные функции, независимо от состояния контракта или последовательности предыдущих операций.

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

Это не теоретические примеры. Разработчики в экосистеме Sui уже применили формальные спецификации для проверки DeFi-контрактов, включая AMM и системы доходного фермерства с кредитным плечом. Когда эти свойства доказываются, а не предполагаются, уровень безопасности фундаментально меняется.

Ландшафт безопасности требует лучших инструментов

Статистика 2025 года делает аргументы в пользу формальной верификации убедительными. По данным исследователей безопасности, на оффчейн-инциденты пришлось 56,5 % атак и 80,5 % потерянных средств в 2024 году, но уязвимости смарт-контрактов остаются разрушительными при их эксплуатации. Уязвимости контроля доступа в одиночку нанесли задокументированный ущерб в размере 953,2 млн долларов в течение 2024 года.

В отчете OWASP Smart Contract Top 10 за 2025 год зафиксированы совокупные потери в децентрализованных экосистемах на сумму более 1,42 млрд долларов. Традиционные инструменты безопасности — Mythril для символьного выполнения, Echidna для фаззинга на основе свойств, ручные аудиты от таких фирм, как OtterSec, Halborn и MoveBit — решают разные аспекты проблемы. Но по мере того как протоколы становятся сложнее и управляют большим объемом активов, пробелы между этими подходами становятся все более опасными.

CertiK внедрила методы формальной верификации для математической проверки смарт-контрактов, защитив, согласно их отчетам, активы на сумму более 300 млрд долларов. Такой масштаб демонстрирует как спрос на математические гарантии безопасности, так и осуществимость применения формальных методов в блокчейн-системах.

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

Почему Move делает формальную верификацию практичной

Не все языки программирования одинаково пригодны для формальной верификации. Гибкость Solidity и сложность EVM делают формальную верификацию сложной задачей — она возможна, но требует значительных затрат на инструменты и экспертизу.

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

Такое наследие дизайна означает, что сами стандартные библиотеки Move прошли формальную верификацию. Когда вы строите на Sui или Aptos, вы опираетесь на фундамент, имеющий математические доказательства корректности — доказательства, которые суммируются по мере того, как вы накладываете поверх свой собственный верифицированный код.

Практический вывод: формальная верификация на Move требует меньше специализированных знаний, чем на других платформах. Документация Sui Prover, примеры и интеграция со стандартными рабочими процессами разработки делают его доступным для разработчиков, не являющихся специалистами по формальным методам. Вы можете учиться писать спецификации постепенно, начиная с простых контрактов функций и переходя к сложным инвариантам по мере углубления понимания.

Что это значит для разработчиков Sui

Для разработчиков, создающих проекты на Sui, открытый исходный код Sui Prover открывает новые возможности:

Дифференциация безопасности: В конкурентной среде DeFi доказательство свойств безопасности — это не просто снижение рисков, а конкурентное преимущество. Пользователи и аудиторы могут проверять заявления о безопасности протокола, а не полагаться на утверждения на веру.

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

Качество документации: Формальные спецификации — это точная документация, которая не устаревает. Если спецификация утверждает, что функция сохраняет определенный инвариант, это либо доказуемо верно, либо верификатор (prover) укажет на нарушение.

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

Экосистема Sui уже включает множество опытных аудиторских фирм, таких как MoveBit (пионеры в формальной верификации Move), Certora, OtterSec и Zellic. Sui Prover добавляет инструмент, который разработчики могут использовать напрямую, не обязательно привлекая внешних аудиторов для каждой задачи верификации.

Более широкая траектория

Открытие исходного кода Sui Prover вписывается в общую тенденцию созревания инструментов безопасности во всей блокчейн-индустрии. Формальная верификация переходит из области академических исследований в производственную инфраструктуру, от специализированных консалтинговых агентств к инструментам, доступным разработчикам.

Эта траектория важна, так как объем активов, защищенных смарт-контрактами, продолжает расти. DeFi-протоколы в совокупности управляют активами на сотни миллиардов долларов. Одна ошибка в крупном протоколе может привести к убыткам, превышающим те, с которыми традиционные софтверные компании сталкиваются за все время своего существования.

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

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

С чего начать

Для разработчиков, заинтересованных в изучении формальной верификации на Sui:

1. Установите Sui Prover: brew install asymptotic-code/sui-prover/sui-prover
2. Начните с малого: Добавьте спецификации к одной критически важной функции и убедитесь, что она проходит проверку.
3. Изучите язык спецификаций: Move Specification Language имеет отличную документацию для описания общих свойств.
4. Итерируйте: Расширяйте покрытие на большее количество функций и более сложные инварианты по мере обретения уверенности.

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

Для индустрии, которая потеряла миллиарды из-за предотвратимых ошибок в 2025 году, вопрос не в том, стоит ли формальная верификация затраченных усилий. Вопрос в том, как быстро экосистема сможет ее внедрить. Выпуск Sui Prover с открытым исходным кодом устраняет один барьер — теперь должны последовать знания и практика.

---

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