技術概要：KVerus

問題定義

形式検証はソフトウェアの正しさを保証する最も高い手段を提供するが、証明の記述、依存関係の管理、ツールチェーンの変更への適応に必要な膨大な手作業のため、大規模で進化し続けるシステムへの拡張は困難なままとなっている。大規模言語モデル（LLM）は証明生成の自動化において有望な成果を示してきたが、現実世界のマルチモジュール環境では失敗している。著者らはその根本原因を「意味的 - 構造的ギャップ」と特定している。すなわち、LLM は意味的なコードパターンに基づいて動作するのに対し、形式検証（特に Rust における Verus 使用時）は、厳格な構造的依存関係、論理的帰結、そして精密な構文規則によって支配されているという点である。

現在の LLM ベースのアプローチは、以下の 4 つの主要な限界に苦しんでいる：

1. 文脈理解の欠如：モジュール化されたシステム全体を横断して推論し、関連するコンポーネントを特定する能力の欠如。
2. 補題発見の低さ：特にドキュメントが不完全な場合、既存の補題を発見し再利用できないこと。
3. ツールチェーン進化への脆弱性：検証ツールチェーン（例：Verus）が更新された際に適応できず、以前有効だった証明が破綻すること。
4. スケーラビリティの問題：大規模なコードベースとともに進化できない、壊れやすく手作業で維持されるグローバルな仕様に依存していること。

手法：KVerus

意味的 - 構造的ギャップを埋めるため、著者らはKVerus、すなわち検索拡張型かつ自己適応型の検証システムを提案する。KVerus は、動的な知識ベースを構築し、それを利用して証明を生成・洗練するパイプラインとして機能する。このシステムは 4 つの中核モジュールから構成される：

1. プリプロセッサ（コードおよび補題の事前処理）

• メタデータ依存グラフ：コードベースの型付き有向グラフを構築するために、深い静的解析を実行する。ノードは言語オブジェクト（関数、型、トレイト）を表し、エッジは依存関係（型/構造および呼び出し/仕様）を表す。
• 依存コード抽出：対象関数に対して、グラフを（最大 3 階層まで）走査し、関連するファイル横断の定義、シグネチャ、依存関係を抽出する。これにより、単一ファイルを超えた包括的な構造的視点が提供される。
• 補題抽出：すべての補題関数のシグネチャ、事前条件（requires）、事後条件（ensures）、および位置を抽出する。

2. コンプリヘンダー（知識の理解と合成）

• 意味的補題インデックス化：現実世界のプロジェクトにおけるドキュメント不足に対処する。LLM を用いて、形式仕様に基づき文書化されていない補題の自然言語要約を生成する。これらの要約と既存のドキュメントをベクトル化し、検索拡張生成（RAG）のためにインデックス化する。
• 自動更新される Verus 知識：公式の Verus ドキュメントを定期的に解析し、最新の構文規則や機能（例：ループ終了節）を抽出する。この知識ベースはツールチェーンとともに自動的に進化し、陳腐化を防ぐ。

3. プロバー（知識駆動型証明生成）

• 文脈構成：対象関数とその抽出された依存コードを組み合わせる。
• 要件分析：LLM を用いて対象および依存コードを分析し、証明に必要な補題の自然言語記述を生成する。
• RAG 検索：これらの記述を用いて補題知識ベースをクエリし、関連する補題を検索する。
• 合成：対象、依存関係、および検索された補題を含む構造化されたプロンプトを構築し、初期の証明試行を生成する。

4. リファイナー（エラー駆動型証明洗練）

• エラー選別：検証が失敗した場合、コンパイラ出力のパターンマッチングを用いてエラー（構文、算術オーバーフロー、ループ不変式の欠落など）を分類する。
• ターゲット知識検索：エラータイプに対応する Verus 知識ベースから、具体的な修正ガイダンスを検索する。
• 反復的洗練：エラーメッセージ、失敗したコード、および修正知識を含む新しいプロンプトを構築し、LLM に証明の洗練を依頼する。このループは、検証が成功するか、最大反復回数に達するまで継続される。

主要な貢献

1. 意味的 - 構造的ギャップの特定：LLM の意味的推論と形式検証の構造的硬直性の間の断絶を、スケーラビリティの主要なボトルネックとして形式的に定義した。
2. 自己適応型検証パラダイム：静的な生成から継続的な適応へと移行する新規フレームワーク。これにより、検証システムはコードベースおよびツールチェーンとともに進化可能となる。
3. KVerus の実装：依存関係感知型解析、意味的補題インデックス化、およびエラー駆動型自己洗練を統合した稼働中のシステム。
4. 現実世界での検証：Asterinas Rust OS カーネル、特にCortenMMメモリ管理モジュールへの成功した適用。

結果

著者らは、KVerus を 3 つの単一ファイルベンチマーク（Verus-Bench, MBPP, Human-Eval）および 3 つのリポジトリレベルベンチマーク（MathSpec-Bench, Memory Allocator, CortenMM）で評価した。

• 単一ファイル性能：KVerus はタスクの80.2%（251/313）を検証し、最先端のAutoVerus（56.9%）およびAlphaVerus（24.9%）を上回った。また、AutoVerus と比較してトークンコストを 50% 以上削減した。
• ツールチェーン更新への堅牢性：3 つの Verus リリースにわたる実験において、KVerus は優れた安定性を示した。ループに対する明示的な decreases 節の導入という破壊的変更が行われた際、AutoVerus の成功率は**23.9%低下したが、KVerus はわずか1.2%**の低下にとどまった。
• リポジトリレベル性能：ファイル横断依存関係ベンチマークにおいて、KVerus は**51.0%**の成功率を達成し、マルチラウンドプロンプティングのベースライン（4.5%）を大幅に上回った。
• Asterinas ケーススタディ：KVerus は CortenMM モジュール内の23 の未検証関数を成功裏に検証し、これは同モジュールの証明コードの**21.0%**を占めた。これらの証明はカーネルのメインラインおよび Verus 標準ライブラリに採用された。
• アブレーション研究：Verus 知識を除去すると単一ファイル性能が最も大きく低下し（最新構文規則の必要性を強調）、コードメタデータを除去するとリポジトリレベル性能が最も大きく低下した（ファイル横断文脈の必要性を強調）。

意義と主張

本論文は、KVerus が現代のセキュリティクリティカルなソフトウェアにとってスケーラブルかつ持続可能な実践としての形式検証への重要な一歩であると主張している。知識中心かつ自己適応型のアーキテクチャを通じて意味的 - 構造的ギャップに対処することで、KVerus は以前の LLM ベースのアプローチの脆さを克服する。

著者らは、彼らの研究が「静的なワンショット生成」から「継続的かつ適応的な検証」へとパラダイムをシフトさせることを強調している。構文、意味、ドメイン知識を体系的に整理することで、以前は自動化ツールでは扱いが難しかった複雑な現実世界のシステム（OS カーネルなど）の検証を自動化することが可能であることを実証している。生成された証明が本流に採用されたことは、システムの実際的な有用性と出力の質を裏付ける具体的な証拠である。