【第 2 回】AI のハルシネーションとの戦い — 29機能すべてが SUCCESSFUL で、認証バイパスが通った

AIが生成した29機能の業務アプリと49本の検証ハーネスがすべて成功したにも関わらず、最も重要な制御ロジックが空洞だったという事例が報告された。これは、AIの制約と実装の無矛盾性は保証されても、その制約自体の妥当性は保証されないことを示している。

• AI が生成した Rust コードの検証で、29 機能すべてが SUCCESSFUL でも認証バイパス等の致命的なバグが検出された。
• 監査役が実装のみをミューテーション（改変）し、証明が落ちないケースを発見。
• 原因は「常に真になる式」「片方向の含意」「判定入力の assume 化」「誤った型変換」の4パターン。
• Kani による形式検証は実装と制約の無矛盾性は保証するが、制約の妥当性は保証しない。
• AI 生成コードの信頼性確保には、形式検証に加え、人間のレビューとテストが依然として重要。