Команда Monad поделилась опытом формальной верификации, выявив несколько уязвимостей безопасности в блокчейне, которые были пропущены при проверке с помощью AI-моделей.

По сообщению Foresight News, команда разработчиков Monad, Category Labs, опубликовала статью, в которой поделилась опытом использования метода формальной верификации для выявления уязвимостей ключевых модулей блокчейна Monad. В публикации раскрывается, что несколько передовых крупных моделей, таких как Claude Opus 4.8 и Codex, не смогли обнаружить определённые уязвимости при аудите кода, в то время как процесс формального доказательства успешно их выявил. Речь идет о проблемах в механизме асинхронного исполнения Monad, связанных с дизайном «Reserve Balance» (резервный баланс), а также о не определённом поведении C++ при оптимизации хранения в MIP-8. Команда считает, что по сравнению с прямым требованием к модели «аудировать код», подход, при котором сначала формулируется точное утверждение о корректности, а затем модель ищет контрпример, более эффективен для выявления скрытых уязвимостей. На сегодняшний день формальная верификация уже может эффективно выполняться с помощью AI.