第1回「仕様がバグっている」を無くす
この記事の要約
「仕様がバグっている」——開発者なら誰もが経験したことがあるはずです。同じ仕様書を読んだのに、エンジニアAとエンジニアBの解釈がバラバラ。テスト工程でようやく「そもそも仕様がおかしい」と気づく。でも、そのときにはもう手遅れ。
この記事では、AIエージェントに「曖昧な仕様書」をぶつけると、どこが曖昧かを構造的に検出してくれて、対話で解消し、検証済みの仕様書を再生成してくれるというパイプラインを紹介します。
使うのはClaude Codeのプラグイン「Formal Agent Contracts」の2つのスキルです。
なぜ仕様は「バグる」のか
日本語（自然言語）は本質的に曖昧です。普段の会話ではその曖昧さが柔軟性として機能しますが、仕様書の文脈ではバグの温床になります。
たとえば、こんな一文を見てください。
ユーザーは複数の住所を登録できる。
一見明確に見えますが、これをシステムとして実装しようとすると疑問が噴出します。
- 「複数」とは何件まで？ 上限はあるのか？
- 住所が0件（未登録）は許容されるのか？
- 「ユーザー」とは？ ゲストユーザーも含むのか？
人間はこの曖昧さを「常識」で補完します。でも、人によって「常識」は違います。 だから同じ仕様書を読んでも解釈がバラバラになるのです。
解決の鍵：「VDM-SLに書こうとしてみる」
ここで形式仕様記述言語VDM-SLの出番です。といっても、皆さんがVDM-SLを覚える必要はありません。AIエージェントがVDM-SLへの変換を試み、「書けない箇所」を炙り出すのがポイントです。
VDM-SLでは「ユーザーは複数の住所を登録できる」を型として定義しなければなりません。
-- 上限なし、0件許容
addresses : seq of Address
-- 上限なし、1件以上必須
addresses : seq1 of Address
-- 最大5件、1件以上必須
addresses : seq1 of Address
inv addrs == len addrs <= 5
どれを書くべきか？ 元の仕様書からは決まりません。つまりこの仕様は「バグっている」——ここがまさに、VDM-SLへの変換を試みること自体が仕様の検証行為として機能する瞬間です。
パイプラインの全体像
┌──────────────────────┐
│ 曖昧な仕様書（MD） │ ← あなたの手元にある仕様書
└──────┬───────────────┘
▼
┌──────────────────────┐
│ import-natural-spec │ ← AIがVDM-SLへの変換を試行
│ 曖昧性を構造的に検出 │ 書けない箇所 = 曖昧な仕様
└──────┬───────────────┘
▼
┌──────────────────────┐
│ 対話で曖昧性を解消 │ ← AIが質問、あなたが回答
│ 優先度: 🔴→🟡→🔵 │ 1つずつ確定していく
└──────┬───────────────┘
▼
┌──────────────────────┐
│ verify-spec │ ← VDMJで機械的に検証
│ 構文・型・証明責務 │ 矛盾がないか自動チェック
└──────┬───────────────┘
▼
┌──────────────────────┐
│ export-human-spec │ ← 検証済みVDM-SLから
│ 自然言語仕様書を生成 │ 人間が読める仕様書を再生成
└──────────────────────┘
入力も出力もMarkdownの仕様書。中間でVDM-SLを経由することで、**機械的な検証を通した「バグのない仕様書」**が手に入ります。
実演：ECサイトの注文仕様を食わせてみる
ここからは実際のAIエージェントとのやりとりを見ていきます。
ステップ1：曖昧な仕様書を用意する
こんなMarkdown仕様書を用意しました。ありがちな仕様書です。
# 注文管理システム仕様書
## データ
- 注文には注文ID、顧客、商品リスト、ステータスがある
- ステータスは保留中、確認済み、発送済み、キャンセルの4つ
- 顧客はアクティブな会員のみ注文可能
## 操作
- 注文作成：顧客が商品を選んで注文する
- 注文キャンセル：注文をキャンセルする
- ステータス更新：注文のステータスを更新する
これをClaude Codeでimport-natural-specスキルに渡します。
この仕様書をVDM-SLの形式仕様に変換して
ステップ2：AIが曖昧性を検出する
AIエージェントは仕様書を読み込み、VDM-SLに変換しようとします。するとすぐに「書けない箇所」が見つかります。
📄 Document Analysis: order-spec.md
Found:
Sections: 2 (データ, 操作)
Requirements: 6
Data models: 1 (ステータス列挙)
Constraints: 1 ("アクティブな会員のみ")
⚠️ 検出された曖昧性: 7件
🔴 ブロッキング（VDM-SLの型定義が書けない）:
1. 「商品リスト」— 同じ商品を複数個注文できるか？
→ seq of Product（重複あり）か set of Product（重複なし）か決まらない
2. 「アクティブな会員」— 会員のステータス一覧が定義されていない
→ どの状態が「アクティブ」なのか列挙できない
🟡 重要（事前条件・事後条件に影響）:
3. 「注文キャンセル」— どのステータスの注文がキャンセル可能か？
→ 発送済みの注文もキャンセルできるのか？
4. 「ステータス更新」— 任意のステータスに遷移可能か？
→ 「キャンセル→確認済み」のような逆戻りは許可されるか？
5. 商品リストが空の注文は作成できるか？
🔵 明確化（より精密にする）:
6. 注文IDの採番ルールは？（自動採番？外部指定？）
7. キャンセル時に在庫は戻るか？（外部システム連携の有無）
7件の曖昧性が構造的に検出されました。 特に注目すべきは🔴のブロッキング——「商品リスト」の型がseqなのかsetなのか、元の仕様書からは判断不能です。
ステップ3：対話で1つずつ解消する
AIは優先度の高い順に質問してきます。
🔴 [1/7] 「商品リスト」について
同じ商品を複数個注文するケースはありますか？
a) 同じ商品を複数個注文可能（例: りんご×3, みかん×2）
b) 同じ商品は1つだけ（商品の種類を選ぶ形式）
c) 商品と個数のペア（商品×数量のマップ）
「c」と回答すると、AIは即座にVDM-SLの型を確定します。
-- [REQ-001] 注文には商品リストがある
-- 解決: 商品×数量のマップ（同一商品の複数個注文対応）
OrderItems = map ProductId to nat1
inv items == items <> {|->} -- 空の注文は不可
こんな調子で7件を順番に解消していくと、全ての曖昧性が消えたVDM-SL仕様が完成します。
ステップ4：機械的検証で矛盾をチェック
完成したVDM-SLはverify-specで機械的に検証されます。
✅ 構文チェック: OK
✅ 型チェック: OK
📋 証明責務: 4件生成
PO-1: CancelOrder操作の事前条件充足性
→ 「注文が存在し、かつステータスが保留中or確認済みであること」
→ 意味: キャンセル可能な状態の注文しかキャンセルできないことが保証されている
PO-2: CreateOrder操作の事後条件
→ 「作成後、注文IDでシステムから取得可能であること」
→ 意味: 注文作成が確実にシステムに反映されることが保証されている
仕様段階で矛盾がないことが機械的に確認されています。
ステップ5：人間が読める仕様書を再生成
最後にexport-human-specで、検証済みのVDM-SLから人間が読める仕様書を再生成します。
# 注文管理システム — 仕様書
> この文書はVDM-SL形式仕様から生成されました。
> 正（source of truth）はVDM-SL仕様です。
## 用語集
| 用語 | 定義 |
|------|------|
| 注文品目 | 商品IDと数量（1以上の自然数）のペア。空の注文は不可。 |
| 会員ステータス | アクティブ、休止、退会の3状態。 |
## 操作
### 注文作成
**目的:** 顧客が商品を選択し、新規注文を作成する。
**前提条件:**
- 顧客のステータスが「アクティブ」であること
- 商品リストに1つ以上の商品が含まれること
- 各商品の数量が1以上であること
**保証:**
- 新しい注文IDが発番され、システムに登録される
- 注文のステータスは「保留中」で開始される
### 注文キャンセル
**目的:** 未発送の注文をキャンセルする。
**前提条件:**
- 対象の注文がシステムに存在すること
- ステータスが「保留中」または「確認済み」であること
（**発送済みの注文はキャンセルできない**）
**保証:**
- ステータスが「キャンセル」に変更される
- 他の注文に影響しない
最初の曖昧な仕様書と比べてください。全ての曖昧性が解消され、前提条件と保証が明確に記述されています。 もはや「解釈のバラつき」が起きる余地はありません。
何が起きたのか——構造的に理解する
このパイプラインの本質は、VDM-SLへの変換を「試みる」という行為自体が仕様の検証になるという点です。
自然言語の仕様書は「読める」ので、人間は曖昧な箇所を見落としがちです。しかしVDM-SLは数学的に厳密な言語なので、曖昧なまま書くことが不可能です。だから「書けない箇所」＝「曖昧な仕様」が構造的に浮かび上がります。
検出される曖昧性のパターンは7種類に整理されています。
| パターン | 例 | なぜVDM-SLで露呈するか |
|---|---|---|
| 曖昧な数量詞 | 「複数の」「いくつかの」 |
seq? set? 上限は? 型が決まらない |
| 未定義の用語 | 「アクティブな」 | 列挙型の値リストが書けない |
| 暗黙の制約 | 代理注文の可否 | 事前条件として明示するか否か |
| 欠落したエラーケース | 支払い失敗時 | 事後条件でエラー状態を表現できない |
| 曖昧な関係 | 「関連する」 | 1対多? 多対多? map? set? |
| 時間的曖昧性 | 「〜の後に」 | 逐次的な操作順序が定義できない |
| 境界条件 | 「最大」「以上」 |
<= か < かinv式が書けない |
重要なのは、**AIがこれらの曖昧性を「暗黙的に解決することは決してない」**という設計です。曖昧性を検出したら、必ず人間に質問する。人間が判断し、AIが形式化する。この役割分担が品質を担保しています。
質問の優先度設計——全部聞くと疲れるから
曖昧性が20件見つかったとして、一度に全部聞かれたら人間はうんざりします。そこで3段階の優先度で順番に聞く設計になっています。
🔴 ブロッキング — VDM-SLの型定義が書けない。これが解消しないと先に進めない。最優先。
🟡 重要 — 型は書けるが、事前条件や事後条件に影響する。ここを間違えるとバグになる。
🔵 明確化 — なくても一応書けるが、あったほうがより精密な仕様になる。
この優先度設計により、最小限の対話で最大限の効果を得られます。
トレーサビリティ——元の要件を見失わない
生成されるVDM-SLには[REQ-nnn]タグが付き、元のMarkdown仕様書の各要件と双方向にトレースできます。
-- [REQ-003] 「顧客はアクティブな会員のみ注文可能」
-- 解決済み: 会員ステータスが<ACTIVE>であること
CreateOrder(custId: CustomerId, items: OrderItems) res: OrderId
pre custId in set dom customers
and customers(custId).status = <ACTIVE>
これにより、どの要件がどのVDM-SL要素に対応しているかが常に明確です。「この事前条件はどこから来たの？」→「REQ-003、元の仕様書のこの一文です」と即答できます。
VDM-SLは正、自然言語仕様書は派生物
このパイプラインで最も重要な設計原則があります。
VDM-SLが正（source of truth）であり、自然言語仕様書は派生成果物である。
ステークホルダーがレビューして「ここを変えたい」と言ったら、自然言語仕様書を直接編集するのではなく、VDM-SLを修正→検証→再生成というサイクルを回します。
修正要望 → VDM-SL修正 → verify-spec → export-human-spec → レビュー
↑ │
└────────────────────────────────────────────────────────┘
なぜこの原則が重要か？ 自然言語を直接修正すると、「修正した結果、別の箇所と矛盾が生じた」ことに気づけません。VDM-SLを経由すれば、矛盾は機械的に検出されます。
まとめ：仕様のバグを構造的に潰す
- 自然言語の仕様書は本質的に曖昧で、「仕様のバグ」はコードのバグより発見が遅く、影響が大きい
- VDM-SLへの変換を試みること自体が仕様の検証行為として機能する。書けない箇所＝曖昧な仕様
- AIエージェントが7パターンの曖昧性を構造的に検出し、優先度付きの対話で解消する
- VDMJによる機械的検証で仕様内の矛盾を自動検出
- 検証済みVDM-SLから人間が読める仕様書を再生成。解釈のバラつきがない仕様書が手に入る
開発の手戻りの多くは「仕様段階のバグ」に起因します。コードを書く前に、仕様そのものを検証する。これが import-natural-spec → verify-spec → export-human-spec パイプラインの価値です。
次回予告
第2回では 「既存コードから仕様をあぶり出す——リバースパイプライン」 を紹介します。仕様書がないまま動いているコードから、AIエージェントが仕様を逆算して形式化するワークフローです。