LLMが書いたコードを「数学的に正しい」と証明する——Python/Go対応・形式検証パイプライン完全ガイド【2025年最新】
3行で分かるこの記事
- LLMが生成したPython/Goコードが仕様通りか、テストではなく「数学的証明」で保証する方法を解説します。
- Lean 4・Dafny・Nagini・Gobraなど言語別に最適な形式検証ツールと、LLMと組み合わせた自動検証パイプラインの構築手順を示します。
- コピペで使えるプロンプト5選を掲載——LLMに「検証可能なコード」を最初から出力させる実践テクニック
はじめに——「テスト通ったから大丈夫」は本当？
ChatGPTやClaude、Geminiにコードを書かせる「バイブコーディング」が当たり前になった。しかし、LLMが出力したコードをそのまま業務に組み込んで、本当に安全でしょうか？
テストでは「試したケースでは動いた」ことしか分かりません。エッジケース、境界値、並行処理のレースコンディション——テストで網羅しきれない不具合が本番環境で発覚する事例は後を絶ちません。
ここで登場するのが形式検証（Formal Verification）です。コードが仕様を満たすことをテストケースの列挙ではなく数学的な証明によって保証します。2025年現在、LLMと形式検証ツールを組み合わせた自動検証パイプラインは急速に実用化が進んでいます。
この記事では、機械学習エンジニア（Python）とフロントサイド/バックエンドエンジニア（Go）の両方に向けて、LLM生成コードの形式検証を自動化する手順を、具体的なツールとプロンプトつきで解説します。
第1章 形式検証の全体像——テストと何が違うのか
テスト vs 形式検証
| 観点 | テスト | 形式検証 |
|---|---|---|
| 保証の範囲 | 実行したケースのみ | すべての入力に対して |
| バグの発見 | 偶然の一致に依存 | 数学的に不在を証明 |
| 並行処理 | 再現困難 | データ競合の不在を証明可能 |
| コスト | 低い（書くのは簡単） | 高い（仕様記述が必要） |
| LLMとの相性 | LLMがテストも書ける | LLMが仕様+証明も書ける時代に |
形式検証は「コストが高い」と考えられてきましたが、LLMが仕様の記述や証明のヒント生成を支援できるようになり、状況が大きく変わりました。
2025年の形式検証エコシステム
┌─────────────────────────┐
│ LLM（Claude, GPT等） │
│ コード生成 + 仕様生成 │
└────────┬────────────────┘
│
┌───────────────┼───────────────┐
▼ ▼ ▼
┌────────────┐ ┌────────────┐ ┌────────────┐
│ Lean 4 │ │ Dafny │ │ Viper基盤 │
│ 定理証明系 │ │ 検証言語 │ │ │
│ Python→翻訳 │ │ 多言語出力 │ │ ┌────────┐ │
└────────────┘ └────────────┘ │ │ Nagini │ │
│ │(Python)│ │
│ ├────────┤ │
│ │ Gobra │ │
│ │ (Go) │ │
│ └────────┘ │
└────────────┘
第2章 ツール選定——Python/Goそれぞれの最適解
Python向けツール
1. Lean 4 + VeriBench方式
Lean 4は依存型を持つ関数型言語で、定理証明器としても機能する。PythonコードをLean 4に翻訳し、翻訳後のコードに対して仕様（定理）を記述・証明するアプローチです。
VeriBenchベンチマーク（2025年）によると、LLMエージェントがPythonコードをLean 4に翻訳し、正しさの定理を証明するタスクにおいて、現在のSOTAモデルでもまだ大きなギャップがあります。つまり、完全自動化は難しいが、LLMの支援で人間の負荷は大幅に下がります。
向いているケース: アルゴリズムの正しさの厳密な証明が必要な場合。数値計算ライブラリ、暗号関連コードなど。
Python関数 → LLMがLean 4に翻訳 → 仕様を定理として記述
→ Lean 4の型チェッカーが証明を検証 → 証明が通れば正しさ保証
2. Dafny（中間検証言語として使う方式）
DafnyはMicrosoft Researchが開発した検証対応言語です。事前条件・事後条件・ループ不変条件を記述でき、内蔵のSMTソルバー（Z3）が自動で証明を試みるものです。
2025年の論文では、DafnyをLLMコード生成の「不透明な中間言語」として使うアーキテクチャが提案されています。ユーザーは自然言語で仕様を伝え、LLMがDafnyコードを生成・検証し、検証済みのDafnyコードをPython/Go/C#/Java等に自動コンパイルします。
"Dafny as Verification-Aware Intermediate Language for Code Generation"
著者: Stefan Zetzsche, K. Rustan M. Leino ほか
発表: 2025年1月、POPL 2025併催のDafny Workshop（Denver, Colorado）
URL: https://arxiv.org/abs/2501.06283LLMがターゲット言語のコードを直接出力する代わりに、Dafnyを不透明な中間表現として生成し、仕様に対する正しさを自動検証した上で、ターゲット言語にコンパイルしてユーザーに返すアーキテクチャを提案しています。 arXivプロトタイプはClaude Sonnet 3.5をベースに構築され、HumanEvalベンチマークで評価されています。
最新の成功率: 最新のLLMを使ったDafnyの純粋な検証タスクの成功率は、2024年6月の68%（Opus-3）から2025年には96%まで向上しています。
向いているケース: 実用的な業務コードの検証。Dafnyのコンパイラが複数言語に出力できるため、最終的にPythonやGoのコードとして利用可能です。
3. Nagini（Python直接検証）
NaginiはETH Zurichが開発した、Python 3の静的検証器です。Viper検証基盤の上に構築されており、Pythonコードに直接アノテーション（事前条件・事後条件等）を書き込んで検証するものです。
向いているケース: Pythonコードをそのまま検証したい場合。コードの翻訳が不要なため、最も直接的なアプローチ。メモリ安全性、関数的性質、デッドロック自由性まで検証可能。
Go向けツール
4. Gobra（Go直接検証）
GobraはNaginiと同じくViper基盤上に構築された、Go専用の形式検証ツールです。Go言語の特徴的な機能——ゴルーチンによる並行処理、チャネル通信、インターフェースの構造的部分型——に対応しています。
SCION（次世代インターネットアーキテクチャ）のGo実装の検証に実際に使われた実績があります。
向いているケース: Goコードのメモリ安全性、クラッシュ安全性、データ競合自由性の証明。特に並行処理の正しさを検証したい場合に強い。
// Gobraのアノテーション例
// @ requires acc(s) && len(s) > 0
// @ ensures result >= 0 && result < len(s)
func findMin(s []int) (result int) {
// @ invariant i >= 0 && i <= len(s)
// @ invariant result >= 0 && result < len(s)
for i := 1; i < len(s); i++ {
if s[i] < s[result] {
result = i
}
}
return
}
5. Dafny → Go出力
DafnyのコンパイラはGo言語への出力をサポートしています。Lean 4がGoと相性が悪い問題を回避しつつ、形式検証の恩恵を受けられるアプローチです。
ツール選定マトリクス
| ツール | 対象言語 | 自動化度 | LLM支援の成熟度 | 並行処理の検証 |
|---|---|---|---|---|
| Lean 4 | Python→翻訳 | 中（証明に人間の支援が必要） | 高（多数の研究） | 不得意 |
| Dafny | Python/Go/C#/Java（コンパイル出力） | 高（SMTソルバー自動証明） | 最高（成功率96%） | 限定的 |
| Nagini | Python（直接） | 高 | 中 | デッドロック検証可 |
| Gobra | Go（直接） | 高 | 低（今後に期待） | ゴルーチン+チャネル対応 |
| Verus | Rust→（参考） | 中 | 中 | Rust所有権で保証 |
第3章 自動検証パイプラインの構築手順
パイプライン全体像
Step 1: 仕様記述（自然言語 → 形式仕様）
│
Step 2: LLMにコード+検証アノテーション生成を依頼
│
Step 3: 検証器で自動検証
│ ├── 成功 → デプロイ可
│ └── 失敗 → エラーメッセージをLLMにフィードバック
│ │
Step 4: LLMがコードを修正（ループ）
│
Step 5: 検証成功 → ターゲット言語にコンパイル or そのまま利用
Python向け：Dafny中間言語パイプライン（推奨）
# 1. Dafnyのインストール
dotnet tool install --global dafny
# 2. LLMにDafnyコードを生成させる（後述のプロンプト参照）
# 3. Dafnyで検証
dafny verify solution.dfy
# 4. 検証成功後、Pythonにコンパイル
dafny build --target:py solution.dfy
# 5. 生成されたPythonコードを利用
python solution-py/solution.py
Go向け：Gobraパイプライン（推奨）
# 1. Gobraのインストール（Java 11+が必要）
# https://github.com/viperproject/gobra からリリースを取得
# 2. LLMにGobra仕様アノテーション付きGoコードを生成させる
# 3. Gobraで検証
java -jar gobra.jar --input solution.go
# 4. 検証成功 → アノテーションはコメントなのでGoコードとしてそのまま利用
go build solution.go
フィードバックループの自動化スクリプト例
import subprocess
import anthropic
client = anthropic.Anthropic()
def verify_and_fix(dafny_code: str, max_attempts: int = 5) -> str:
"""Dafnyコードを検証し、失敗時はLLMで自動修正するループ"""
for attempt in range(max_attempts):
# ファイルに書き出し
with open("solution.dfy", "w") as f:
f.write(dafny_code)
# Dafnyで検証
result = subprocess.run(
["dafny", "verify", "solution.dfy"],
capture_output=True, text=True
)
if result.returncode == 0:
print(f"検証成功！（{attempt + 1}回目）")
return dafny_code
# 失敗時：エラーメッセージをLLMにフィードバック
error_msg = result.stderr + result.stdout
response = client.messages.create(
model="claude-sonnet-4-20250514",
max_tokens=4096,
messages=[{
"role": "user",
"content": f"""以下のDafnyコードが検証に失敗しました。
エラーメッセージを分析して修正してください。
【現在のコード】
{dafny_code}
【エラーメッセージ】
{error_msg}
修正したDafnyコード全文のみを出力してください。"""
}]
)
dafny_code = response.content[0].text
raise Exception("検証に失敗しました（最大試行回数超過）")
第4章 コピペで使えるプロンプト5選
プロンプト1: Python関数のDafny検証（数値計算）
あなたはDafnyの形式検証エキスパートです。
以下のPython関数の仕様を満たすDafnyメソッドを生成してください。
【Python関数の仕様】
- 関数名: binary_search
- 入力: ソート済み整数配列 arr、検索値 target
- 出力: targetのインデックス（見つからない場合は-1）
- 事前条件: 配列はソート済み（∀i, j: i < j → arr[i] <= arr[j]）
- 事後条件:
- 戻り値が-1でない場合、arr[戻り値] == target
- 戻り値が-1の場合、配列にtargetは存在しない
【要件】
1. requires句で事前条件を記述
2. ensures句で事後条件を記述
3. ループ不変条件（invariant）を明示
4. decreases句で停止性を保証
5. `dafny verify` で検証が通ること
Dafnyコードのみを出力してください。
プロンプト2: GoのHTTPハンドラのGobra検証（Web API）
あなたはGobraの形式検証エキスパートです。
以下のGo関数にGobra検証アノテーションを付与してください。
【Go関数の仕様】
- 関数名: ValidateAndSanitizeInput
- 入力: ユーザーからの文字列入力 input string
- 出力: サニタイズ済み文字列 string, エラー error
- 事前条件: inputはnil以外
- 事後条件:
- errorがnilの場合、出力文字列は空でない
- errorがnilの場合、出力文字列にHTML特殊文字（<, >, &, ", '）が含まれない
- errorがnon-nilの場合、出力文字列は空文字列
【要件】
1. // @ requires で事前条件を記述
2. // @ ensures で事後条件を記述
3. Gobraで検証が通ること
4. Goのコンパイルも通ること（アノテーションはコメント）
Gobra仕様付きGoコードを出力してください。
プロンプト3: MLパイプラインの型安全性（Python + Lean 4）
あなたはLean 4とPythonのエキスパートです。
以下のPythonの機械学習前処理関数をLean 4に翻訳し、
正しさの定理を記述・証明してください。
【Python関数】
def normalize(data: list[float]) -> list[float]:
"""min-max正規化。出力の各要素は[0,1]の範囲。"""
min_val = min(data)
max_val = max(data)
if max_val == min_val:
return [0.0] * len(data)
return [(x - min_val) / (max_val - min_val) for x in data]
【証明すべき性質】
1. 出力リストの長さ == 入力リストの長さ
2. 出力の全要素が 0.0 以上 1.0 以下
3. 入力が空でなければ出力も空でない
Lean 4のコード、定理の記述、証明を出力してください。
プロンプト4: Go並行処理のデータ競合自由性
あなたはGobraの形式検証エキスパートです。
以下のGoの並行処理コードにGobra仕様を付与し、
データ競合（data race）が存在しないことを形式検証してください。
【Go関数の仕様】
- 複数のゴルーチンが共有カウンターをインクリメント
- チャネルを使って同期
- 最終結果が正確にN（ゴルーチン数）であること
【要件】
1. チャネルのプロトコル仕様を記述
2. 各ゴルーチンのパーミッション（アクセス権）を明示
3. データ競合の不在を証明
4. 最終値の正しさ（カウンター == N）を証明
Gobra仕様付きGoコードを出力してください。
プロンプト5: Dafnyによるクロス言語検証（Python+Go共通仕様）
あなたはDafnyの形式検証エキスパートです。
以下の仕様をDafnyで実装・検証し、
検証済みコードをPythonとGoの両方にコンパイルしてください。
【共通仕様】
- 関数名: MergeSort
- 入力: 整数のシーケンス
- 出力: ソート済み整数のシーケンス
- 事後条件:
1. 出力はソート済み（∀i: 0 <= i < |output|-1 → output[i] <= output[i+1]）
2. 出力は入力の置換（同じ要素を同じ回数含む）
3. 出力の長さ == 入力の長さ
【要件】
1. Dafnyで完全な実装と証明を記述
2. `dafny verify` で検証が通ること
3. `dafny build --target:py` でPython出力
4. `dafny build --target:go` でGo出力
5. 両方の出力が正しく動作すること
1つの検証で2言語の正しいコードを得る
「Write once, verify once, compile everywhere」を実現してください。
第5章 実践上の注意点と限界
できること・できないこと
形式検証でできること:
- アルゴリズムの正しさの完全な証明
- メモリ安全性の保証
- データ競合の不在の証明
- 入出力関係の仕様適合性の証明
形式検証で（まだ）難しいこと:
- 大規模コードベース全体の検証（部分的に適用するのが現実的）
- 外部ライブラリを含むコードの検証（ライブラリの仕様が必要）
- 性能要件の検証（「正しく動く」は証明できるが「速い」は別の話）
- 仕様そのものの正しさ（仕様が間違っていれば検証も無意味）
段階的な導入戦略
いきなり全コードを形式検証するのは非現実的だ。以下の優先順位で段階的に導入しよう
。
- セキュリティクリティカルなコード: 認証、暗号、入力バリデーション
- 金融計算: 利息計算、為替変換、税金計算
- データパイプラインのコア変換: ETLの変換ロジック
- 並行処理の同期コード: ゴルーチン、async/await周り
第6章 今後の展望——LLM × 形式検証の未来
2025年現在の状況をまとめると、Dafnyの検証成功率は1年で68%→96%に跳ね上がりました。LLMがDafnyコードの生成と修正を繰り返す「検証ループ」の有効性は、複数の研究で実証されています。
今後1〜2年で予想される変化を予想してみました。
- IDE統合の進化: VS CodeやGoLandから直接形式検証を実行し、LLMが即座に修正提案を行うワークフロー
- 仕様の自然言語記述: 自然言語で書いた仕様をLLMが形式仕様に自動変換する精度の向上
- 検証済みライブラリの蓄積: 形式検証済みの標準ライブラリが増えることで、実用コードの検証が容易に
「バイブコーディング」から「ベリコーディング（vericoding）」へ——LLMが生成したコードをLLMが検証する時代はすぐそこまで来ています。
この記事のまとめ
| 言語 | 推奨ツール | アプローチ |
|---|---|---|
| Python | Dafny（中間言語）+ Nagini（直接検証） | LLM → Dafny生成 → 検証 → Python出力 |
| Go | Gobra（直接検証）+ Dafny（中間言語） | LLM → Gobra仕様付きGo生成 → 検証 |
| 両方 | Dafny | 1つの検証で複数言語に出力 |
今日からできるアクション:
-
dotnet tool install --global dafnyでDafnyをインストール - 上記プロンプト1をClaude/GPTに投げてみる
- 生成されたDafnyコードを
dafny verifyで検証する - 検証が通ったら
dafny build --target:pyでPythonコードを取得する
形式検証は「アカデミアの道具」から「現場のエンジニアの武器」に変わりつつあります。LLMという強力な助手を得た今、その恩恵を受けない手はないです
。
参考文献・ツール一覧
- Lean 4 — 依存型定理証明器
- Dafny — Microsoft Research、検証対応プログラミング言語
- Gobra — Go言語の形式検証ツール（ETH Zurich）
- Nagini — Python 3の静的検証器（ETH Zurich）
- Viper — 中間検証言語基盤（ETH Zurich）
- VeriBench — LLM×Lean 4の形式検証ベンチマーク
- dafny-annotator — LLM支援によるDafnyアノテーション自動生成
- APOLLO — LLM+Lean4自動証明パイプライン
- Vericoding Benchmark — 形式検証済みコード合成ベンチマーク
著者注
: この記事の内容は2026年3月時点の情報に基づいています。形式検証×LLMの分野は急速に発展しているため、最新の情報は各ツールの公式ドキュメントを参照してください。