據 Woofun AI 消息，Monad 開發團隊 Category Labs 分享了利用形式化驗證排查區塊鏈關鍵模塊漏洞的實踐。該過程成功捕獲了 Claude Opus 4.8、Codex 等前沿大模型在代碼審查中未能發現的多個安全隱患，主要涉及 Monad 異步執行機制中的"Reserve Balance"設計及 MIP-8 存儲優化中的 C++ 未定義行爲問題。

團隊指出，相較於直接要求模型審查代碼，先構建精確的正確性命題再尋找反例的工作流能更有效地暴露隱藏漏洞。目前，形式化驗證流程已可大幅藉助 AI 輔助完成，提升了安全審計的深度與效率。