Формальная верификация в Тоне
Сама идея формального рассуждения восходит к Готфриду Лейбницу (XVII век), который мечтал о создании универсального языка, способного свести все споры к вычислениям. Идея в том, чтобы привести математическое доказательство того, что система ведёт себя строго в соответствии со своей спецификацией, а не просто проверка на отдельных примерах.
Главная разница с обычными инвариантными тестами в том, что тестирование может показать наличие ошибок, но не их отсутствие, тогда как формальная верификация математически гарантирует корректность для всех возможных входных данных и состояний.
Данная техника наиболее полезна в областях с критическими требованиями к корректности и безопасности, такие как: медицина, ПО для шахт, финансы и блокчейны.
Верификация в веб3 актуальна как никогда - десятки команд занимаются доказательствами на эфире, был создан Lean Foundation для формализации всего протокола, llm агенты исключительно хорошо формируют теоремы.
В Тоне тоже есть industry-level исследования по этой теме - движок символьного исполнения TSA. TSA моделирует семантику TVM на уровне байткода, учитывая все возможные пути исполнения. Неважно насколько обфусцирован код контракта или запутана логика бранчей - если существует путь исполнения который не соответствует заданной спеке - то движок его найдет с любым стейтом.
В написании чекеров для Тона есть несколько сложных моментов:
• Асинхронная акторная модель в кросс-контрактном анализе
• Зубодробительный расчет комиссий сети (storage fee, fwd fee, … - их все нужно символьно эмулировать)
• > 900 инструкций в TVM
Используя TSA, я формально верифицировал ключевые свойства в стандарте жеттонов TEP-74 и написал сервис для проверки контрактов в сети на символьное соответствие спеке.
Полностью стандарт не так интересен (например burn и mint), поэтому я сделал фокус на самом важном для пользователей - трансфере.
На уровне чекеров я проверяю жеттон-кошельки на следующие свойства:
• Трансфер может быть отправлен на любой произвольный адрес (свойство ханнипотов)
• В результате трансфера баланс получателя меняется ровно на поле amount (свойство tax жеттонов)
• Нельзя заблокировать трансферы по флагу (вообще это считается governance, но свойство опасное)
• Гет методы отдают реальный стейт (sanity check)
Демка - https://verify.lagus.cooking
Код - https://github.com/Kaladin13/formal-verification-jetton
Вопросы на подумать:
• Можно ли обмануть мои чекеры по этим свойствам и как
• Какое есть фундаментальное ограничение в форм верифе на Тоне
• Можно ли верифицировать электор
20
14
13
4
2March 2, 2026 1.6K 12 8
