Monad 团队分享形式化验证实践，发现多个 AI 模型审查时遗漏的链上安全漏洞

Foresight News 消息，Monad 开发团队 Category Labs 发文分享其使用形式化验证（Formal Verification）方法排查 Monad 区块链关键模块漏洞的经验，披露了多个 Claude Opus 4.8、Codex 等前沿大模型在代码审查中未能发现、但形式化证明过程成功捕获的漏洞。涉及 Monad 异步执行机制中的「Reserve Balance（保留余额）」设计及 MIP-8 存储优化中的 C++ 未定义行为问题。团队认为，相比直接要求模型「审查代码」，先写出精确的正确性命题再要求模型寻找反例，这种工作方式更容易暴露隐藏漏洞，形式化验证目前已可大幅借助 AI 辅助完成。