据 Woofun AI 消息，Monad 开发团队 Category Labs 分享了利用形式化验证排查区块链关键模块漏洞的实践。该过程成功捕获了 Claude Opus 4.8、Codex 等前沿大模型在代码审查中未能发现的多个安全隐患，主要涉及 Monad 异步执行机制中的"Reserve Balance"设计及 MIP-8 存储优化中的 C++ 未定义行为问题。

团队指出，相较于直接要求模型审查代码，先构建精确的正确性命题再寻找反例的工作流能更有效地暴露隐藏漏洞。目前，形式化验证流程已可大幅借助 AI 辅助完成，提升了安全审计的深度与效率。