Monad 开发团队 Category Labs 近日分享了利用形式化验证（Formal Verification）排查区块链关键模块漏洞的实践经验。
报道披露，在针对 Monad 异步执行机制中的“保留余额（Reserve Balance）”设计以及 MIP-8 存储优化中的 C++ 未定义行为进行审查时，Claude Opus 4.8 和 Codex 等前沿大模型均未能发现潜在漏洞，而形式化证明过程则成功捕获了这些深层缺陷。
团队指出，在代码审查中，直接要求 AI 模型“审查代码”的效果有限。相比之下，更高效的协作方式是先定义精确的正确性命题，再引导模型寻找反例，这种方法能更有效地暴露隐藏漏洞。Category Labs 认为，形式化验证目前已能在大幅借助 AI 辅助的情况下高效完成。
