Monadチームは形式的検証の実践を共有し、複数のAIモデルによる審査で見逃されたオンチェーンのセキュリティ脆弱性を発見した。

Foresight Newsの報道によると、Monadの開発チームであるCategory Labsは、形式的検証（Formal Verification）手法を用いてMonadブロックチェーンの重要モジュールの脆弱性を調査した経験を共有し、Claude Opus 4.8やCodexなどの最先端大規模モデルによるコードレビューでは発見できなかったが、形式的証明のプロセスで発見された複数の脆弱性を公表しました。これには、Monadの非同期実行メカニズムにおける「Reserve Balance（保留残高）」設計や、MIP-8ストレージ最適化におけるC++の未定義動作の問題が含まれています。チームは、モデルに直接「コードのレビュー」を依頼するのではなく、まず正確な正当性命題を書き出し、そのうえでモデルに反例を探させる方法の方が隠れた脆弱性を発見しやすいと考えており、形式的検証は現時点でAIの補助によって大幅に効率化することが可能だと述べています。