論文の概要: KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code

• arxiv url: http://arxiv.org/abs/2605.03822v1
• Date: Tue, 05 May 2026 14:50:24 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-06 19:35:43.981665
• Title: KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code
• Title（参考訳）: KVerus: Rustコードのためのスケーラブルでレジリエントな形式検証証明生成
• Authors: Yuwei Liu, Xinyi Wan, Yanhao Wang, Minghua Wang, Lin Huang, Tao Wei,
• Abstract要約: 我々は、VerusベースのRust検証のための検索拡張システムであるKVerusを紹介する。 KVerusは、コードメタデータ、レムマセマンティクス、ツールチェーン仕様の動的知識ベースを構築する。 複雑なファイル間の依存関係をナビゲートして証明を合成し、共通の進化的変化に直面した時に自動的に証明を修正することができる。
• 参考スコア（独自算出の注目度）: 15.778121969330476
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal verification provides the highest assurance of software correctness and security, but its application to large-scale, evolving systems remains a major challenge. While large language models (LLMs) have shown promise in automating proof generation, they often fail in real-world settings due to their inability to handle complex cross-module dependencies or changes in the codebase or the verification toolchain. We identify the fundamental problem as the Semantic-Structural Gap: LLMs operate on semantic code patterns, whereas formal verification is governed by rigid structural dependencies, a disconnect that leads to brittle, unsustainable proofs. To bridge this gap, we propose a new paradigm of self-adaptive verification and present KVerus, a retrieval-augmented system for Verus-based Rust verification that can adapt to an evolving software environment. KVerus constructs a dynamic knowledge base of code metadata, lemma semantics, and toolchain specifics. By combining dependency-aware program analysis, semantic lemma indexing, and error-driven self-refinement, it can navigate intricate cross-file dependencies to synthesize proofs and automatically repair proofs when faced with common evolutionary changes. Across three single-file benchmarks, KVerus verifies 80.2% of tasks, outperforming the state-of-the-art AutoVerus (56.9%) and degrades less than AutoVerus under breaking Verus updates. On three repository-level benchmarks with cross-file dependencies, KVerus achieves a 51.0% success rate, compared to 4.5% for a multi-round prompting baseline. Finally, on the Asterinas Rust OS kernel, KVerus produces upstream-accepted proofs that verify 23 previously unverified functions (21.0% of proof code) in the memory-management module. KVerus represents a significant step towards making formal verification a scalable and sustainable practice for modern, security-critical software.
• Abstract（参考訳）: 形式的検証は、ソフトウェアの正当性とセキュリティの最高保証を提供するが、大規模で進化するシステムへの適用は依然として大きな課題である。 大きな言語モデル(LLM)は証明生成の自動化を約束しているが、複雑なモジュール間の依存関係やコードベースや検証ツールチェーンの変更を扱うことができないため、現実の環境では失敗することが多い。 LLMはセマンティック・構造的ギャップ(Semantic-Structural Gap): LLMはセマンティック・コード・パターンで動作するが、形式的検証は厳密な構造的依存関係によって制御される。 このギャップを埋めるため、我々は自己適応型検証の新しいパラダイムを提案し、進化するソフトウェア環境に適応可能なVerusベースのRust検証のための検索強化システムであるKVerusを提示する。 KVerusは、コードメタデータ、レムマセマンティクス、ツールチェーン仕様の動的知識ベースを構築する。 依存関係を意識したプログラム分析、セマンティック・レムマ・インデックス、エラー駆動型自己修正を組み合わせることで、複雑なファイル間の依存関係をナビゲートして証明を合成し、共通の進化的変化に直面した時に自動的に証明を修正することができる。 3つのシングルファイルベンチマークで、KVerusは80.2%のタスクを検証し、最先端のAutoVerus(56.9%)を上回り、Verusのアップデートを破り、AutoVerusより低下する。 ファイル間の依存関係を持つ3つのリポジトリレベルのベンチマークでは、KVerusは51.0%の成功率を達成している。 最後に、Asterinas Rust OSカーネル上で、KVerusは、メモリ管理モジュールの23の未検証関数(証明コードの21.0%)を検証する上流受け入れ証明を生成する。 KVerusは、最新のセキュリティクリティカルなソフトウェアに対して、フォーマルな検証をスケーラブルで持続可能なプラクティスにするための重要なステップである。

関連論文リスト

• DocSync: Agentic Documentation Maintenance via Critic-Guided Reflexion [0.0]
  DocSyncは、ドキュメントのメンテナンスを構造的に基盤付けられた反復的な生成タスクとしてフレーム化するエージェントワークフローである。 LoRA適応小言語モデルを用いたDocSyncの資源制約実装を実証的に評価する。 このAST対応エージェントアプローチが標準エンコーダ・デコーダのベースラインを大幅に上回ることを示す。
  論文  参考訳（メタデータ） (2026-05-04T02:41:33Z)
• IMPACT-CYCLE: A Contract-Based Multi-Agent System for Claim-Level Supervisory Correction of Long-Video Semantic Memory [73.22944697933603]
  既存のパイプラインは不透明でエンドツーエンドの出力を生成し、検査の中間状態は公開しない。 IMPACT-Cycleは,マルチモーダル反復クレームレベルのメンテナンスとして,長時間ビデオ理解を再構築するマルチエージェントシステムである。
  論文  参考訳（メタデータ） (2026-04-22T03:03:33Z)
• WybeCoder: Verified Imperative Code Generation [22.401681809856896]
  WybeCoderはエージェントコード検証フレームワークである。 コード、不変性、そして証明が共進化する所で、証明・アズ・ユー・ジェネレーション開発を可能にする。
  論文  参考訳（メタデータ） (2026-03-31T00:06:44Z)
• Dynamic analysis enhances issue resolution [53.50448142467294]
  DAIRA(Dynamic Analysis-enhanced Issue Resolution Agent)は、エージェントの推論サイクルに動的解析を組み込む自動修復フレームワークである。 テストトレース駆動の方法論によって駆動されるDAIRAは、軽量モニタを使用して重要なランタイムデータを抽出する。 Gemini 3 Flash Previewを使用すると、DAIRAは新たな最先端(SOTA)パフォーマンスを確立し、SWE-bench Verifiedデータセットで79.4%の解像度を達成する。
  論文  参考訳（メタデータ） (2026-03-23T14:48:54Z)
• RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
  LLM(Large Language Models)は、コード生成において顕著な能力を示しているが、セキュアなコードを生成する能力は依然として重要で、未調査の領域である。 我々はRealSec-benchを紹介します。RealSec-benchは、現実世界の高リスクなJavaリポジトリから慎重に構築されたセキュアなコード生成のための新しいベンチマークです。
  論文  参考訳（メタデータ） (2026-01-30T08:29:01Z)
• Probing Pre-trained Language Models on Code Changes: Insights from ReDef, a High-Confidence Just-in-Time Defect Prediction Dataset [0.0]
  本稿では,22の大規模C/C++プロジェクトから得られた関数レベル修正の信頼性の高いベンチマークであるReDefを紹介する。 欠陥ケースはコミットの反転によって固定され、クリーンケースはポストホック履歴チェックによって検証される。 このパイプラインは3,164の欠陥と10,268のクリーンな修正をもたらし、既存のリソースよりも信頼性の高いラベルを提供する。
  論文  参考訳（メタデータ） (2025-09-11T07:07:11Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。 SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。 我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。