セキュリティ企業は、エージェント型コードレビューを超えたAIを活用し、実際のコード検査前にカスタムツールや形式モデルを構築し、セキュリティ監査を強化しています。例えば、開発者ツールが不足しているMiden VMのレビューでは、エージェントが6か月間かけてLSPサーバー、デコンパイラ、静的解析エンジン、VM実行者のリーンモデルを作成しました。これらのツールは、検証されていないプルーバーからの入力がFalcon署名の偽造や資金盗難を可能にする重大なセキュリティ脆弱性を特定しました。リーンモデルはまた、Midenコアライブラリのかなりの部分に対して95件の機械チェックによる正確性証明も生成しました。Miden VMは独自のアセンブリ言語(MASM)を持つ新しいゼロ知識VMで、スタックマシンアーキテクチャと開発者ツールの欠如により独自のレビュー課題を抱えていました。これに対処するため、チームはLSPサーバーと構文ハイライト、コードナビゲーション、命令文書化のためのVS Code拡張機能から重要なツールの開発を優先しました。次に、MASM手続き用のデコンパイラを開発し、暗黙のスタック操作や宣言されていない署名などの複雑さにもかかわらず、高レベルの意味情報を提供します。このデコンパイラは数か月にわたる取り組みで、貴重な内部解析フレームワークと静的解析の中間表現を生み出しました。この中間表現を活用し、チームは静的解析のための抽象解釈エンジンを構築し、証明者提供値の検証、型制約の強制、ローカル変数の初期化を保証するパスを実装しました。これにより、400以上の型検証改善案と高重大度のバグ、すなわちmod_12289手続きにおける未制約のアドバイザ値が発見されました。この脆弱性により、悪意のある証明者が余りを操作し、Falcon署名を偽造しMidenアカウントを流出させる可能性がありました。バグ発見を超えて、エージェントはLeanを用いた形式検証を探求し、Miden VMエグゼキュータのモデリングやMASM手続きを自動的にLeanに変換しました。このエージェント駆動の形式モデリングにより、バイナリ演算コンポーネントの正確性証明が95回実現し、既存のユニットテストで見落とされていた2つの微妙なバグ、すなわち64ビット右回転(rotr)のエッジケースと256ビット乗算(wrapping_mul)の問題が明らかになりました。これらの高度なツール開発と形式的モデリングの取り組みは、AIエージェントの最近の進歩によって実現可能となり、時間とリソースの制約で達成不可能だった準備作業の深さと質を大幅に向上させました。