据 Foresight News 报道，Monad 的 Category Labs 团队近日分享了 Monad 区块链形式化验证的结果，揭示了多个安全漏洞，这些漏洞是包括 Claude Opus 4.8 和 Codex 在内的先进 AI 模型在代码审查中未能发现的。
发现的漏洞涉及 Monad 异步执行机制中的 Reserve Balance 设计以及 MIP-8 存储优化中的 C++ 未定义行为问题。该团队证明，形式化验证成功捕获了这些缺陷，并强调在请求 AI 寻找反例之前，先定义精确的正确性命题比直接请求代码审查更能有效暴露隐藏的漏洞。
