プラグイン有効性評価レポート
Formal Agent Contractsプラグインを使用した場合と使用しなかった場合で、AI駆動エージェント開発の成果物の品質にどの程度の差が生じるかを定量的に計測した結果。
実施日
2026-04-01
評価者
Claude Opus 4.6（自動スコアリング）
使用モデル
Claude Opus 4.6
試行数
30 (3 × 5 × 2)
1. 実験概要
Formal Agent Contractsプラグインの有用性を定量的に評価するため、同一の開発課題を以下の2条件で実施しました。
| 条件 | 説明 | 試行数 |
|---|---|---|
| A群（Control） | Claude Codeのみ。形式手法ツールなし。自然言語での指示のみ | 15（3課題 × 5回） |
| B群（Treatment） | Claude Code + Formal Agent Contractsプラグイン | 15（3課題 × 5回） |
ベンチマーク課題
Task 1: 銀行口座
Low単一エージェント、CRUD + 送金
トラップ数: 10
Task 2: 図書館
Medium3エージェント連携、制約多数
トラップ数: 12
Task 3: オークション
High状態遷移 + 時間制約 + 並行性
トラップ数: 14
2. 総合結果
4つの評価メトリクスで比較を実施。4メトリクス中3つで大きな効果量（Cliff's δ ≥ 0.474）が算出されました（M4は形式仕様の存在自体がスコアを構成するため構造的にlarge）。
| メトリクス | A群（Control） | B群（Treatment） | Δ | 効果量 |
|---|---|---|---|---|
| M1: 契約違反検出率 | 52.0% ± 33.6 | 63.9% ± 22.5 | +11.8pp | small |
| M2: 仕様カバレッジ | 39.1% ± 21.2 | 81.9% ± 26.9 | +42.8pp | large |
| M4: 仕様明示性 | 8.9% ± 15.3 | 100.0% ± 0.0 | +91.1pp | large |
| M6: テスト有効性 | 66.7% ± 23.4 | 87.0% ± 8.5 | +20.3pp | large |
M1: 契約違反検出率
Control
52.0%
Treatment
63.9%
M2: 仕様カバレッジ
Control
39.1%
Treatment
81.9%
M4: 仕様明示性
Control
8.9%
Treatment
100.0%
M6: テスト有効性
Control
66.7%
Treatment
87.0%
効果量の解釈（Cliff's delta）
|δ| < 0.147 → 効果なし（negligible）
|δ| < 0.33 → 小（small）
|δ| < 0.474 → 中（medium）
|δ| ≥ 0.474 → 大（large）
メトリクスの定義
M1: 契約違反検出率（Contract Violation Detection Rate）— 事前に定義した「埋め込みトラップ」（エッジケース）のうち、生成されたコードまたはテストが検出・対処しているものの割合
M2: 仕様カバレッジ（Specification Coverage）— 課題のビジネスルールのうち、コード内で明示的に検証（バリデーション、アサーション、型制約）されているものの割合
M4: 仕様明示性（Specification Explicitness）— ビジネスルールが機械的に検証可能な形式で記述されている度合い。VDM-SLレベル3、コード内契約レベル2、コメントレベル1、暗黙レベル0
M6: テスト有効性（Test Effectiveness）— 生成されたテストの網羅性と品質。テスト密度とエッジケースキーワード網羅率の複合スコア
3. 課題別詳細分析
Task 1: 銀行口座管理エージェント（Low Complexity）
低複雑度の課題ではControl群もM1で高いスコア（88.0%）を達成。ビジネスルールが明確で少ないため、形式仕様なしでも対処可能なケースが多い。ただし、M2（仕様カバレッジ）では100% vs 60%と明確な差がある。Control群は「初期残高が負の場合」「空白のみの名義」「送金のアトミック性」などの暗黙の仕様を見落とす傾向。
Task 2: 図書館貸出管理システム（Medium Complexity）
マルチエージェント間の制約整合性で差が顕著に。Control群は「在庫カウントの整合性」「返却直後の即座の再貸出」「二重延長防止」などのエージェント間契約を見落としがち。Treatment群はVDM-SLの不変条件でこれらを事前に定義するため、自然と検出される。
Task 3: オンラインオークション（High Complexity）
M1・M6は最も複雑な本課題で差が最大（M2はTask 2が最大）。状態遷移 + 時間制約 + 並行性の組み合わせは、形式仕様なしでは網羅的にカバーすることが困難。特に「延長の連鎖上限」「同時入札の優先順位」「支払いタイムアウトの境界」「キャンセル後の再出品可否」は、本評価のControl群5試行ではほぼ見落とされた。
4. 複雑度と効果の関係
M1とM6では課題の複雑度が上がるほど差が拡大した（M2はTask 2で最大であり単調ではない）。単純な課題では人間（またはLLM）の直感でも十分カバーできるが、複雑度が増すと形式的な枠組みなしでは見落としが急増する。3課題×各5試行という範囲での観察であり、一般化には追試が必要。
| 複雑度 | M1 Δ | M2 Δ | M6 Δ | 傾向 |
|---|---|---|---|---|
| Low | -3.3pp | +40.0pp | +13.5pp | 基本機能は形式仕様なしでもカバー可能 |
| Medium | +15.0pp | +62.2pp | +17.5pp | エージェント間制約で差が顕在化 |
| High | +23.8pp | +26.2pp | +30.0pp | 状態遷移 + 時間制約でM1・M6の差が最大 |
5. 仮説の検証
H1: プラグイン使用群は契約違反検出率が有意に高い
部分的に支持全体ではΔ = +11.8pp、Cliff's δ = 0.18（small）。課題複雑度別に見るとTask 3で+23.8ppと明確な差があり、低複雑度課題ではControl群も高い検出率を達成するため全体平均では差が薄まる。なおM1はキーワードベースの自動スコアリングによる計測であり、「有意に高い」を判定する検定（Wilcoxon）は未実施。
H2: プラグイン使用群は仕様カバレッジが有意に高い
支持する傾向Δ = +42.8pp、Cliff's δ = 0.74（large）。形式仕様の作成プロセスそのものがビジネスルールの明示的検証を促すため、本評価では仕様カバレッジが大幅に向上したと考えられます（キーワードベースの自動計測。有意性検定は未実施）。
H3: プラグイン使用群は仕様漂流が少ない
間接的に支持M4（仕様明示性）でΔ = +91.1pp、Cliff's δ = 1.00。ただしVDM-SL仕様の存在自体がM4スコアを構成するため、この差は構造的なものであり、H3の直接的な支持とはみなしません。間接的な根拠はM2の+42.8ppで、仕様がコードの品質にも波及している可能性を示唆します。
6. 妥当性への脅威と限界
内的妥当性
| 脅威 | 状況 | 対策 |
|---|---|---|
| 同一エージェントによる生成 | 同一Claudeインスタンスが両群を生成 | 各runに意図的なスタイル変化を導入（ただし独立性の欠如という交絡は解消されないため、別モデル・独立した実施者による追試が必要） |
| キーワードベースのスコアリング | M1, M2はヒューリスティック | 手動レビューで補完可能 |
| M6のJest実行断念 | 環境制約でgold test実行不可 | テストコードのヒューリスティック分析で代替 |
外的妥当性
| 脅威 | 対策 |
|---|---|
| 3課題の代表性 | 複雑度3段階でカバー |
| LLM依存 | Claude Opus 4.6を使用。他モデルでの追試を推奨 |
| 実務プロジェクトとの差異 | 評価用の小規模課題であり、大規模プロジェクトへの一般化可能性は未検証 |
構成概念妥当性
| 脅威 | 対策 |
|---|---|
| M4は形式仕様の存在で自動的にスコア向上 | M1, M2, M6はコードの振る舞いで評価 |
| ヒューリスティックスコアの精度 | scores.jsonに全エビデンスを保存。手動レビュー可能 |
7. 結論
本評価の条件下では、Formal Agent Contractsプラグイン使用群が複数のメトリクスで高いスコアを示しました。特に以下の点で大きな差が観測されました（有意性検定は未実施のため、統計的有意性は主張しません）。
仕様カバレッジ（M2）: +42.8pp、効果量 large — 形式仕様の作成プロセスがビジネスルールの漏れを減らすことが示唆される（キーワードベースの自動計測）
仕様明示性（M4）: +91.1pp、効果量 large — VDM-SL仕様がコードの仕様基盤として機能（M4は形式仕様の存在によりTreatment群が構造的に100%となる点に注意）
テスト有効性（M6）: +20.3pp、効果量 large — 仕様から導かれたテストケースの方がエッジケースを網羅する傾向（gold test実行不可のためテストコードのヒューリスティック分析で代替計測。ミューテーションテストでは検出率に群間差なし）
複雑度が高いほど差が拡大する傾向（M1・M6） — Task 3（状態遷移 + 時間制約）ではM1・M6で最大の差。ただしM2はTask 2で最大（+62.2pp）であり、全メトリクスで単調に拡大するわけではない
これらの結果は、形式手法をAI駆動開発に組み込むことの価値を示唆する探索的な結果であり、特に中〜高複雑度のシステム開発において、Formal Agent Contractsプラグインが品質保証に寄与しうることを示しています。同一Claudeインスタンスによる両群生成やヒューリスティックスコアリングという限界があるため、独立した評価者・別モデルによる追試が必要です。
8. ミューテーションテスト
評価の信頼性をさらに強化するため、全30試行の生成コードに対してミューテーションテスト（バグ注入テスト）を実施しました。ソースコードに意図的な変異（バグ）を注入し、テストスイートがそれを検出できるかを計測します。
手法
6種類のミューテーション演算子（境界値置換、比較演算子変更、ガード条件削除、算術演算子交換、条件反転、状態遷移ガード削除）を定義し（うち実際に適用可能な変異を生成したのは3種類）、各変異に対してテストスイートを実行しました。
結果
| グループ | 試行数 | 変異総数 | 検出数 | 検出率 | 平均変異数/試行 |
|---|---|---|---|---|---|
| A群（Control） | 15 | 21 | 21 | 100% | 1.40 |
| B群（Treatment） | 15 | 25 | 25 | 100% | 1.67 |
検出率
Control
100.0%
Treatment
100.0%
平均変異数/試行
Control
1.40
Treatment
1.67
主要な発見: 両群とも100%検出率
Control群・Treatment群ともに注入された全変異を100%検出しました。AI生成テストは、形式仕様の有無にかかわらず、テスト対象の変異タイプに対して機能的に健全であることが示されました。
副次的発見: Treatment群のコードはより広い変異適用面を持つ
Treatment群のコードには1試行あたり平均1.67個の変異が適用可能でした（Control群は1.40個、+19.3%）。Control群には適用箇所のなかった変異タイプ（NEG-amount: パラメータ符号反転）も含まれます。これはテスト検出力の優位ではなく、生成コードの性質（変異可能な境界・バリデーション箇所の多さ）を反映したものであり、より明示的で検証可能な境界条件と整合しますが、その独立した裏付けではありません。
主要評価との関係
ミューテーションテストの結果は主要評価と方向性が一致します。Treatment群のコードにはより多様な変異タイプが適用可能で（M2: 仕様カバレッジ +42.8ppと整合）、1試行あたりの適用可能な変異箇所も多い（M6: テスト有効性 +20.3ppと整合）ものの、いずれも生成コードの構造を反映したものであり、テスト品質の差の独立した裏付けではありません。
限界
100%検出率は天井効果を示しており、この指標単体では両群を区別できません。主要評価のM2・M4・M6が引き続き主要な差別化指標です。より多様なミューテーション演算子（セマンティック変異、並行性変異等）の適用により、さらなる差異が明らかになる可能性があります。
付録: 評価データ
全評価データはGitHubリポジトリで公開されています。
- eval/results/scores.json — 全30試行の生スコアデータ
- eval/runs/control/ — A群の全出力（15ディレクトリ）
- eval/runs/treatment/ — B群の全出力（15ディレクトリ）
- eval/tasks/ — ゴールドスタンダード（仕様、テスト、トラップ定義）
- eval/scripts/eval-runner.ts — 自動スコアリングスクリプト
- eval/results/mutation-scores.json — ミューテーションテスト生データ
- eval/results/mutation-report.md — ミューテーションテストレポート