Формальная верификация в Тоне

Сама идея формального рассуждения восходит к Готфриду Лейбницу (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

Вопросы на подумать:
• Можно ли обмануть мои чекеры по этим свойствам и как
• Какое есть фундаментальное ограничение в форм верифе на Тоне
• Можно ли верифицировать электор