形式的検証で最も難しいのは、検証器そのものではない。証明を書くことだ。
熟練のRustエンジニアにMicrosoft ResearchのSMTベース検証器であるVerusを渡せば、午後ひとりで関数にpreconditionとpostconditionを注釈できる。その後、検証器は機械的な確実性をもって、その関数があらゆる可能な入力に対してcontractを満たすかどうかを教えてくれる。その部分は満足感がある。
しかし次にloopにぶつかる。検証器はpostconditionを導出できないと訴える。エンジニアはinvariant、つまり各反復の前後で真となる論理命題が必要になる。このinvariantの発見には、以前は博士号が必要か、少なくとも40時間の試行錯誤が必要だった。OOPSLA 2025で発表されたAutoVerusは、LLMエージェントのネットワークを用いてこの作業の90%以上を自動化する。中央値の証明タスクは30秒以内、あるいは3回のLLM呼び出しで解決する。
以下に、実際の仕組み、かかるコスト、そしてまだ破綻する箇所を述べる。
真のボトルネックはSMTソルバーではなくinvariant探索である
VerusはRustをghost code、precondition、postconditionで拡張する。次のように書く：
use vstd::prelude::*;
verus! {
fn sum(arr: &[i32]) -> (result: i32)
requires
arr.len() <= 0x40000000,
ensures
result == spec_sum(arr@),
{
let mut total = 0;
let mut i = 0;
while i < arr.len()
invariant
0 <= i <= arr.len(),
total == spec_sum(arr@.subrange(0, i as int)),
{
total = total + arr[i];
i = i + 1;
}
total
}
}requires節がprecondition、ensures節がpostconditionである。whileループ内のinvariantブロックが証明を成立させる鍵だ。これはSMTソルバーに、各反復で何が真であり続けるかを伝える。
難しいのはinvariantである。total == spec_sum(arr@.subrange(0, i as int))は自明ではない。人間は最初のi個の要素を処理した後に何が真であり続けるかを帰納的に考えてこれを書く。AutoVerusは、検証器のフィードバックに導かれる探索問題としてinvariant合成を扱うことで、これを自動生成する。
AutoVerusがLLMエージェントを探索戦略として用いる仕組み
AutoVerusはGPT-4への単一プロンプトではない。構造化されたコンテキストを互いに受け渡す特殊化されたエージェントのパイプラインである。
最初のエージェントはRust関数とそのdoc commentを読む。verification conditionを抽出し、requires、ensures、invariant節の初期ドラフトを生成する。
2番目のエージェントはこれらの注釈をVerusに入力する。Verusは注釈付きコードをコンパイルし、そのSMTソルバー（通常はZ3）にproof obligationのdischargeを依頼する。ソルバーがUNSATと答えれば性質は成立する。SATと答えればcounterexampleを生成する。ほとんどの場合、最初のドラフトは失敗する。
修復エージェントは検証器のエラーメッセージと失敗したproof obligationを読む。より強いinvariant、より厳しいbound、あるいはauxiliary lemmaを提案する。サイクルは繰り返される：生成、検証、修復。AutoVerusは中央値で3回のLLM呼び出しで収束すると報告している。150の非自明なベンチマークタスクの半数以上が30秒以内に終了する。
肝心なのは、LLMが論理に抜群であるということではない。証明探索は局所最適化問題であり、LLMは手入力する人間よりも速く空間を探索するために、局所的な改善を推測するのに十分な能力を持っている。
90%という数字が実際に意味するもの
AutoVerusは150の非自明なRust証明タスクのベンチマークで、90%以上の証明自動化を達成した。これには配列境界推論、ループ蓄積、再帰的構造走査が含まれる。ベンチマークは実際のVerusコードベースから抽出された。
90%という数字は、LLMパイプラインが人間の介入なしにVerusが受理する証明を生成したことを意味する。それがプログラマーの意図した仕様であるとは限らない。LLMは関数名、doc comment、型署名から意図を推論する。関数がprocessと名付けられ、doc commentが「handles the thing」と書いてあれば、生成された仕様は汎用的で誤っている可能性がある。
これは、copilotがコード生成にもたらしたのと同じ分業だ。LLMが初稿を書き、人間が領域正確性のためにレビューする。違いは、誤った証明は静かだということだ。検証を通過した生成証明は、誤った性質を証明している可能性がある。関数が何をすべきかを理解している人間が依然として必要だ。
AutoVerusができないこと
AutoVerusはVerusが表現できる範囲に制限される。VerusはRustのサブセットを扱う。async、closures、特定の標準ライブラリコレクションはサポートしない。コードがtokioでタスクをspawnする場合、AutoVerusはまだ助けられない。
AutoVerusはパターンにも縛られる。90%の成功率は、訓練分布に似たコード、つまり配列に対するループ、算術蓄積、境界チェックに適用される。証明が自明でないauxiliary lemmaを必要とする場合、修復エージェントは繰り返し上限に達するまでループする可能性がある。その時点で、手作業で証明を書き直すことになる。
コストもゼロではない。ベンチマークタスクは証明あたり数セントかかる。完全なモジュールはAPI呼び出しで10〜30ドルかかる可能性がある。これは検証エンジニアの時間より2桁安いが、無料ではない。
実際のコードでAutoVerusを実行する
AutoVerusはMicrosoft Researchから入手できる。リポジトリはGitHub上のmicrosoft/verus-proof-synthesisである。Verusがインストールされていることを前提とする。
実際のワークフローは以下の通り：
# 1. Install Verus
git clone https://github.com/verus-lang/verus.git
cd verus && source ./source/vstd.sh
# 2. Clone AutoVerus
git clone https://github.com/microsoft/verus-proof-synthesis.git
cd verus-proof-synthesis
# 3. Set your API key for the LLM backend
export OPENAI_API_KEY="sk-..."
# 4. Run AutoVerus on a Rust file
python autoverus.py --input src/my_module.rs --output src/my_module_verified.rs出力はrequires、ensures、invariant節を含む注釈付きRustファイルである。すべての注釈をレビューする。その後、Verusを実行する：
verus src/my_module_verified.rsVerusがverification results:: verifiedと報告すれば、SMTソルバーがすべての義務をdischargeしたことを意味する。エラーを報告した場合は、AutoVerusに再入力して別の修復ラウンドを行うか、手動で修正する。
CI統合では、Verusを注釈付きモジュールでのみ実行される別ジョブとして扱う。Verusの検証時間は注釈の複雑さに応じて増大する。恐れている関数から始める：パーサー、プロトコルステートマシン、信頼できないバッファにインデックスするあらゆるもの。
AutoVerusを使うべき時と諦めるべき時
AutoVerusは、Verusのサブセットに収まるRustコードがあり、無限の正しさ証明が欲しい場合に試す価値がある。Kaniは注釈なしで有界証明を与え、クラッシュなしチェックには高速だが、無限ループにわたる性質は証明できない。AutoVerusは完全な無限証明を与える。その代償として、ほとんど自動生成される注釈が必要になる。
コードがasyncである、複雑なclosuresを使う、あるいは「すべてのリクエストは最終的にレスポンスを受け取る」といったliveness性質の証明が必要な場合は諦める。livenessには依然としてTLA+が必要だ。カスタム数学理論を証明に必要とする場合も諦める。LLMエージェントは新しい数学を発明しない。以前に見たパターンを取得して適応するに過ぎない。
正直な結論
AutoVerusはコードを理解する必要性をなくさない。すでに理解しているコードのinvariantを40時間かけて書く必要性をなくす。変化はproof engineeringからprompt engineeringへのシフトだ：意図を記述し、エージェントが証明空間を探索し、SMTソルバーが結果を認証する。
このシフトは、形式的検証を専門家のニッチからCIパイプラインのステップへ移すのに十分だ。アプリケーションと信頼できないネットワーク入力の間の30行の解析コードについて、パニックしないことを証明するのが現実的になった。証明は数秒で生成され、数分で検証され、パーサーが何をすべきかを知る人間によってレビューされる。
1つの関数から始める。Rustを書く。AutoVerusを実行する。注釈を読む。意図と一致すれば、機械検証済みの証明を得たことになる。一致しなければ、白紙より良い出発点を得たことになる。
Frequently Asked Questions
What is AutoVerus and how does it relate to Verus?
AutoVerus is an automated proof generation system built on top of Verus, a Rust verifier from Microsoft Research. Verus checks whether annotated Rust code satisfies its specifications using an SMT solver. AutoVerus generates those annotations using a network of LLM agents.
How accurate is AutoVerus at generating proofs?
On its benchmark of 150 non-trivial Rust proof tasks, AutoVerus achieved over 90% automation. More than half resolved in under 30 seconds or three LLM calls. Accuracy depends on how closely your code matches the training distribution patterns.
Does AutoVerus eliminate the need to learn formal verification?
No. You still need to understand the annotations to review them for correctness. A generated proof that passes verification may prove the wrong property if the LLM misread your intent. AutoVerus reduces proof writing time from days to minutes, but it does not replace human judgment.
What Rust code works with AutoVerus?
Code that fits the Verus subset: functions with loops, array indexing, arithmetic, and recursive structures. AutoVerus does not support async, closures, or many standard library collections. It is best suited for systems code, parsers, and algorithmic functions.
How much does AutoVerus cost to run?
The benchmark tasks cost cents per proof. A full module might cost ten to thirty dollars in API calls. This is significantly less than the 40 to 80 hours of engineering time required for manual proof writing.