はじめに
本記事では、一ヶ月ほど前から細々と試していた Web サービス向けの形式手法による仕様駆動開発が、ようやくハーネスとして大体こんな感じかもと固まってきたのでその紹介をしたいと思います。
作ったものは Cradle という Lean による仕様駆動開発ハーネスです。
まずは問題意識から説明していきたいと思いますが、「長えよ！Cradleについて早く教えろ！」という方はこちらへどうぞ
想定読者
- 大きめの Web サービスの開発に携わっている方
- AI-DLC や CC-SDD で悩んでいる方
既存のAI駆動開発の課題
Vibe Coding
まずは Vibe Coding の課題です。この言葉が登場して大体１年半ほど立ちましたが、既に様々な課題が認識されています。
例えば、
- コードの保守性が著しく下がる。技術的負債が急速に蓄積されていくことで継続的な開発が困難になる。
- バグや脆弱性が埋め込まれやすくなる。
- 要件が小出しされることで、一貫性のない仕様が実装される
などです。
特に３つ目の課題は原理的な問題で、人間が長期的なセッションで一貫性のある要件をインプットし続けるのが難しいことに起因します。昨今の複数エージェントを起動した並列開発では特に起きやすく、たった３，４回のラリーでも矛盾した要件を入れてしまうことがあります。どんなにコード品質やセキュリティ等の非機能要件を整備するハーネスを固めたところで、機能要件を正しく伝えられなければソフトウェアは正しく作れません。
もちろん、最近のLLMは賢いので大抵の場合矛盾を指摘してくれますが、それでも抜け漏れなどにより、急速にコード品質が悪化していきます。
ドキュメントベースの仕様駆動開発
前述の Vibe Coding の課題を解決するために生まれたのが AI 駆動の仕様駆動開発です。仕様駆動開発自体は AI の隆盛以前も存在しましたが、ドキュメントの管理コストが重いという課題がありました。SIer で Excel のメンテが辛いというのはよく聞いた話だと思います。
そのような仕様駆動開発ですが、LLM の登場によってドキュメントの生成を簡単に行えるようになったことで、軽量に行うことができるようになりました。これによって個人でも簡単に規律のある開発が実現できるようになるはずでした。
しかし、実際に起こったのはドキュメント量の爆発的な増加でした。エンハンスを繰り返すたびにドキュメントが累積し、AI のコンテキスト処理能力・人間の認知限界を超える、ということが起こります。
それにより発生する課題は２つです。
課題１：要件インプットの誤り
AI-DLC や CC-SDD では、Inception フェーズ、Discovery フェーズと呼ばれる、AI が人間に要件を選択肢形式で問いかけるフェーズが存在します。このフェーズでよく起こるのが、人間側が選択肢それぞれが選んだときにどういう影響があるのか、どんなふるまいになるのかが予見できない、ということです。私見ですが、人間は自然言語のみで複雑な仕様や質問を理解できるようにできていません。しっかりとした理解を得るためには図やHandsOn的なものが必須です。しかし、AI-DLC 等のワークフローでは基本的に自然言語のみで質問を聞きます。その結果質問内容に対する理解が浅くなったり、誤った理解をしてしまい、誤った回答や曖昧な指示を与えてしまうことで、初期要件に歪みが生じる事態が発生します。
そしてその誤りに気づくのはテストや実稼働時の工程です。AI 駆動開発で開発効率が上がったとはいえ、手戻り工数は大きいです。
課題２：ドキュメントと実装の整合性の歪み
AI は必ずしもドキュメントを正しく書けるとは限りません。AI 駆動の仕様駆動開発では、その性質上過去資産が膨大に生じます。それらのすべてを AI のコンテキストに載せることは不可能なため、必然的に既存仕様との整合性を保つことが難しくなり、矛盾が蓄積していくことになります。
また、そのようにして出来上がったドキュメントをベースとして出力された実装にも不整合が生まれます。矛盾を含んだドキュメントから生成されるため、既存仕様との不整合や要件の微妙な未達が発生するのです。
これらの問題に対して、現状は人間による E2E テストの作成やテスト観点レビューを厚くする等の対応を行なっていると思いますが、それも完璧ではありません。
結果として、変更を加えるたびに潜在的なバグや仕様の不整合が蓄積していき、長期的な保守・拡張が困難になっていきます。さらにそれは、LLM 隆盛以前よりも遥かに高速に積み上がっていきます。
形式手法による仕様駆動開発という打ち手
ドキュメントベースの仕様駆動開発の課題は、つまるところドキュメントが実行可能でなく、静的解析ができないことに起因します。
前章で言及したそれぞれの課題は
- requirement-verification-questions.md に書かれた質問をそれぞれその時点で 実行して 確かめることができない
- ドキュメントに含まれた論理的矛盾を、決定論的に 解析して 明らかにすることができない
という、ドキュメントの実行可能性、検査可能性の話に集約できます。巨大なドキュメント群も LLM の推論を介さずに決定論的に矛盾を解析・発見することができれば、AI のコンテキストも我々人間の認知限界も関係ありません。そしてドキュメント自体が実行可能であれば、それを触って確かめることができるため、人間の理解を促進することができるはずです。
これらをできるのが形式手法だと私は考えます。
形式手法とは
形式手法とは、ソフトウェアやシステムの振る舞いを数学に基づいた厳密な言語で定義し、論理的に検証するアプローチです。一般的な開発プロセスでは、仕様書は自然言語、あるいはUMLや画面設計書などで書かれます。しかし、自然言語にはどうしても解釈の揺れや暗黙の前提、エッジケースの記述漏れが含まれてしまいます。
形式手法は、このような仕様の曖昧さを数学的なアプローチでゼロに近づける体系です。
検証アプローチの分類
形式検証にはさまざまな手法がありますが、代表的なアプローチとしてモデル検査と演繹的検証があります。
| アプローチ | 手法 | 特徴 | 主なツール |
|---|---|---|---|
| 状態探索型（モデル検査） | システムの状態遷移モデルを作り、不変条件に違反するパスがないか網羅的に探索する | 自動化しやすく反例を見つけやすいが、状態爆発問題がある。 | TLA+/TLC， SPIN，Alloy※ |
| 演繹的検証（定理証明） | システムや実装を数学的にモデル化し、満たすべき性質を命題として記述して、その性質が成立することを論理的に証明する。 | 無限の入力空間や複雑な不変条件も扱えるが、証明記述のコストが高い。 | Coq, Lean, Isabelle |
※ Alloy は厳密には有限スコープ内で反例やモデルを探索する bounded model finder
Lean とは
今回、Cradle ハーネスにおける仕様の形式化と証明のエンジンとして採用したのが Lean です。
Lean は、依存型理論に基づく対話型定理証明支援系であり、同時に純粋関数型プログラミング言語でもあります。一番の特徴として、コンパイラが証明器として機能するということです。つまり、仕様を表す型に対して、正しく型検査が通る実装を与えること自体が、その仕様が満たされていることの数学的証明になります。
例えば Lean では証明を次のように記述します。
以下のようにモデルが定義されていたとして、
-- 口座の状態
structure Account where
balance : Nat
deriving Repr
-- 引き落とし操作
-- 残高が足りていれば更新後のAccountを返し、足りなければnoneを返す
def withdraw (acc : Account) (amount : Nat) : Option Account :=
if h : acc.balance >= amount then
some { balance := acc.balance - amount }
else
none
引き落とし操作 withdraw の仕様の証明は以下のようになります。
-- 定理：引き落とし成功時、残高は必ず減少または維持される
theorem withdraw_decreases_balance
(acc : Account) (amount : Nat) (newAcc : Account) :
withdraw acc amount = some newAcc → newAcc.balance <= acc.balance := by
-- 1. withdraw 関数の定義を展開する
intro h
unfold withdraw at h
-- 2. 条件分岐（残高 >= 金額）で場合分け
split at h
case isTrue cond =>
-- 成功ケース：some newAcc = some { balance := acc.balance - amount }
injection h with h_acc
rw [← h_acc]
-- 自然数の引き算の性質（a - b <= a）により自明
exact Nat.sub_le acc.balance amount
case isFalse cond =>
-- 失敗ケース：none = some newAcc となり矛盾するため排除
contradiction
withdraw acc amount = some newAcc → newAcc.balance <= acc.balance の部分が命題であり、by 以降がその証明になります。証明したい命題をわかりやすく表現すると、「acc から amount 円引き落とした(withdraw した)結果が、newAcc ならば、newAcc.balance は acc.balance 以下である」ということになります。証明部については、ほとんど自明なので割愛します。
どうでしょうか？大体 Lean の雰囲気は掴めたでしょうか？
Lean による仕様駆動開発ハーネス "Cradle"
ここまでは、既存の仕様駆動開発の課題や形式手法に触れてきました。ここからは本題の、Lean による仕様駆動開発ハーネス "Cradle" です
コンセプト
Cradle のコンセプトは以下の３つです
- Lean による正当性が検証された矛盾のない仕様記述
- 実行可能な仕様による人間の確認コスト最小化
- Lean から Kotlin (interface, テスト) への決定論的な変換による、仕様の決定論的ハーネス化
Lean による正当性が検証された矛盾のない仕様記述
Cradle では、AI-DLCのように要件に関する質問をしていき、エージェントが解釈した仕様のモデリングを行います。ドメインモデルは Lean によって記述され、モデリングの過程で曖昧な点、矛盾点が見つかるたびに、論点としてあげられユーザーに聞き返されます。
そのようにしてできた Lean によるドメインモデルは曖昧性や矛盾点が排除されており、エージェントが解釈した仕様は必ず満たすようになっています。
実行可能な仕様による人間の確認コスト最小化
前節で説明されていた Lean によるドメインモデルは、Lean 自体がプログラミング言語である以上、実行可能なプログラムとなっています。いくつか Cradle 側で用意されたボイラープレートを利用する必要があるものの、ドメインモデルを視覚的に操作することのできる Web モックアップを通じて、Lean で記述された仕様をそのまま実行することができます。
これによって要件の質問の際に、ある選択肢を選んだときどうなるか、というのを実際に動かして試したり、バックエンドの実装フェーズに入る前にフロントエンドに接続して挙動を確かめたり、ということができます。つまり、エージェントが解釈した仕様と人間が想像している仕様の合致を、
- 人間が要件質問を理解するコストを下げて、正しく要件をインプットできる確率を上げる
- 中間成果物の確認の容易性を向上させて、成果物と人間の意図のズレを発見する確率を上げる
の２段構えによって高い水準で保証することができるのです。
Lean から Kotlin (interface, テスト) への決定論的な変換による、仕様の決定論的ハーネス化
ここまでのコンセプトでできた Lean による仕様は、そのまま堅牢な Web サービスのバックエンドとして利用することができません。なぜなら、 Lean は定理証明支援系であり、一般的な Web サービスとして必要な セキュリティ水準やオブサーバビリティ、パフォーマンスを実現し得ないからです。とはいえ、Lean から Kotlin に書き換えるのを全面的にエージェントに行わせるというのもまた、変換にゆらぎが生じるため、バグが生じる可能性をはらんでいます。
Cradle はそのような課題に対して、ドメインモデルの各コンポーネントから interface とプロパティベーステストを自動生成する、という解決策で対処しています。interface は各コンポーネントを表す構造体やそれを利用する関数のシグネチャから生成することができますし、プロパティベーステストは各コンポーネントの満たすべき性質を証明した定理群から具体値を当てはめることで生成できます。エージェントは、そのようにして生成された interface をテストが通るように実装すれば良いので、テストが通るコードを書けたということは、ほぼ必然的に仕様を満たすコードが書けたということになります。もちろん完璧ではないですが、こういったガードレールを何も用意せずに直接 Lean から Kotlin に変換するよりは圧倒的に仕様準拠度の高いものができるはずです。
あくまでイメージではありますが、３つのコンセプトが正しく適用できれば、以下のような状態を目指せます。
Lean によるドメインモデリングのコアとなる考え方
続いてどのように Lean によってドメインモデルを記述するか、について説明していきます。
基礎となる考え方は以下です。
「上位のコンポーネントの性質に関する定理は、それ自身の制約と、下位のコンポーネントの制約・性質定理を使って証明する」
例えば、Entity の性質に関する定理は依存する ValueObject や 子 Entity の持つ制約や性質に関する定理を使って証明されます。簡単な例ですが以下のような形です。
LLM プロバイダーの API キーと クレジットの単純な関係をモデリングしたものです。ApiKey はそれそのものが使用可能量 Credit を持ち、その限界量を超えて使うことはできない、という関係性になります。
/-!
# 上位の定理を、自身の制約と下位の定理から証明する例
* 下位 `Credit` : クレジットの量。性質定理はここでだけ定義（中身 `amount`）を開いて証明する。
* 上位 `ApiKey` : Credit を持つ集約。定理は「ApiKey 自身の定義・制約」と
「Credit の性質定理」を使って証明する。
-/
/-! ## 下位コンポーネント: Credit -/
structure Credit where
amount : Nat
deriving Repr, DecidableEq
namespace Credit
def zero : Credit := ⟨0⟩
instance : LE Credit := ⟨fun a b => a.amount ≤ b.amount⟩
instance (a b : Credit) : Decidable (a ≤ b) := inferInstanceAs (Decidable (a.amount ≤ b.amount))
/-- 引き算。足りなければ 0（残高は負にならない）。 -/
def sub (a b : Credit) : Credit := if b ≤ a then ⟨a.amount - b.amount⟩ else zero
/-- 残っている（0 より多い）。 -/
def isPositive (a : Credit) : Bool := decide (0 < a.amount)
/-! ### Credit の性質定理（上位から使われる公開の契約） -/
theorem zero_not_positive : zero.isPositive = false := rfl
theorem zero_le (a : Credit) : zero ≤ a := Nat.zero_le a.amount
theorem le_refl (a : Credit) : a ≤ a := Nat.le_refl a.amount
theorem le_trans {a b c : Credit} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c := Nat.le_trans h₁ h₂
/-- 引いた結果は元より多くならない。 -/
theorem sub_le (a b : Credit) : a.sub b ≤ a := by
unfold sub
split
· exact Nat.sub_le a.amount b.amount
· exact zero_le a
end Credit
/-! ## 上位コンポーネント: ApiKey -/
structure ApiKey where
/-- 購入したクレジット -/
purchased : Credit
/-- 残っているクレジット -/
credits : Credit
/-- この日になった時点で期限切れ -/
expiresOn : Nat
namespace ApiKey
/-- ApiKey 自身の制約: 残高は購入した量を超えない。 -/
def Valid (k : ApiKey) : Prop := k.credits ≤ k.purchased
/-- クレジットが購入され、API キーが渡された。有効期限は購入から 30 日。 -/
def issue (c : Credit) (purchasedOn : Nat) : ApiKey := ⟨c, c, purchasedOn + 30⟩
/-- 推論でクレジットを消費する。足りなければ残高を使い切って打ち切る。 -/
def charge (k : ApiKey) (cost : Credit) : ApiKey :=
{ k with credits := if cost ≤ k.credits then k.credits.sub cost else Credit.zero }
/-- まだ推論に使える（クレジットが残っていて期限内）。 -/
def live (k : ApiKey) (today : Nat) : Bool :=
k.credits.isPositive && decide (today < k.expiresOn)
/-! ### ApiKey 自身の定理（ApiKey の定義だけを開く） -/
/-- クレジットが尽きた鍵は推論に使えない。 -/
theorem live_of_no_credits (k : ApiKey) (today : Nat) (h : k.credits.isPositive = false) :
k.live today = false := by
simp [live, h]
/-- 残高で足りなければ使い切る。 -/
theorem charge_short (k : ApiKey) (cost : Credit) (h : ¬ cost ≤ k.credits) :
(k.charge cost).credits = Credit.zero := by
simp [charge, h]
/-! ### 上位の性質定理（自身の定理・制約 ＋ Credit の定理で証明する） -/
/-- 残高不足で打ち切られた鍵は、もう推論に使えない。 -/
theorem charge_short_not_live (k : ApiKey) (cost : Credit) (today : Nat)
(h : ¬ cost ≤ k.credits) : (k.charge cost).live today = false := by
apply live_of_no_credits -- ApiKey の定理
rw [charge_short k cost h] -- ApiKey の定理
exact Credit.zero_not_positive -- Credit の定理
/-- 買った直後は制約を満たす。 -/
theorem issue_valid (c : Credit) (d : Nat) : (issue c d).Valid :=
Credit.le_refl c -- Credit の定理
/-- 消費しても制約は保たれる。 -/
theorem charge_valid (k : ApiKey) (cost : Credit) (hk : k.Valid) : (k.charge cost).Valid := by
simp only [Valid, charge]
split
· exact Credit.le_trans (Credit.sub_le _ _) hk -- Credit の定理 ＋ ApiKey の制約 hk
· exact Credit.zero_le _ -- Credit の定理
end ApiKey
この考え方に沿って、ValueObject, Entity, AggregateRoot, DomainService までモデリングした上で、更にそれを利用する UseCase もモデリングします。そうしてできたそれぞれのコンポーネントを Kotlin に interface, プロパティベーステストとして落とし込むわけです。
ワークフロー
前述のような考え方を基盤として、Cradle では以下のような流れで開発を進めます。
ドメイン探索
ドメイン探索フェーズでは、以下のような選択形式の質問シートが作成され、選択肢によっては、「これを選択するとこのような挙動になる」、という専用のシナリオがドメインモデルの Web モックアップに一時的に作成されます。
## Q2. （前の問いで「少しずつも」を選んだ場合のみ）少しずつ届いている途中でクレジットが尽きて打ち切られたとき、業務上は何が起きたことになりますか?
| | 選択肢 | 選ぶとどうなるか | モックアップ |
|---|---|---|---|
| **a** | 届いた分はユーザーのもの | HS-008 の「渡らない」は、まとめて届くときだけの話になります | probe-q2-a |
| **b** | 届いた分も無かったことになる | 手元に届いていても、業務上は渡っていない扱いです | probe-q2-b |
| **c** | 少しずつのときは子キーを切り替えない | 親キーでも別の子キーでやり直さず（イベント#24 は起きず）、打ち切りで終わります | probe-q2-c |
**回答:**
<!-- 選択肢の記号か、自由に書いてください。「前提が違う」「問いが成り立たない」もそのまま。 -->
仕様の Lean 化
仕様の Lean 化では、ドメイン探索フェーズでのユーザーの回答に基づき Lean によるドメインモデルが作成されます。作成される Lean のコードは「Lean によるドメインモデリングのコアとなる考え方」で示した Lean コードとだいたい同じようなものができると考えていただいて差し支えありません。
ドメインモデルの Web モックアップ作成
このフェーズでは、以下のようなドメインモデルの Web モックアップが作り込まれます。このモックアップはほぼ生のドメインモデルであり、ドメイン探索での選択肢の確認やドメインモデル自体へのレビューはこのモックアップを利用して行います。
バックエンド インターフェース・テスト自動生成
このフェーズでは、Cradle 内蔵の Kotlin 製 plugin である lean2kotlin によって、Lean から Kotlin への interface とプロパティベーステストの生成が実行されます。
Entity の interface は以下のように生成され、
/**
* Lean: `LLMX.Domain.ApiKey`(aggregateRoot)
*/
interface ApiKey {
val id: ApiKeyId
val secret: KeySecret
val owner: MemberId
val listing: ListingId
val provider: ProviderId
val pricing: Pricing
val credits: Credit
val expiresOn: java.time.LocalDate
val parent: ParentKeyId?
val entries: List<UsageEntry>
val refunded: Credit?
/** 返金の金額: 未使用分 × 買ったときの値段 [HS-069]。1 クレジット = 1 ドル [HS-068]。 */
fun refundUsd(): Credit?
/** 子キーが親キーから外された [イベント#38]。クレジットは残る [HS-045]。 */
fun detach(): ApiKey
/** 期限が切れている（その日になった）[HS-078]。 */
fun expired(today: java.time.LocalDate): Boolean
/** 親キーに紐づいている（＝子キー）。 */
fun isChild(): Boolean
/** クレジットの有効期限が切れた [イベント#12]。ユーザーの退会でも同じく失効する [HS-048]。 */
fun expire(): ApiKey
/** API キーが作り直された: 前の鍵は使えなくなり、新しい鍵に残りのクレジット・有効期限・明細・親キーとの紐づけが */
fun reissue(secret: KeySecretId): ApiKey
/** 残高で足りる。 */
fun covers(usage: Usage): Boolean
/** 実際に消費されるクレジット。足りなければそこまでの残高全部 [イベント#13][HS-008]。 */
fun charged(usage: Usage): Credit
/** ユーザーに届く答えの片。最後まで行われて残高で足りれば答えのすべてが届く。打ち切り・中断では、 */
fun delivered(input: InferenceInput, pieces: List<AnswerPiece>, finished: Boolean): List<String>
/** まだ推論に使える（クレジットが残っていて期限内）。 */
fun live(today: java.time.LocalDate): Boolean
/** 子キーが親キーに紐づけられた（別の親キーへの紐づけ直しも同じ操作）[イベント#22][イベント#38][HS-045]。 */
fun attach(parent: ParentKeyId): ApiKey
/** 未使用のクレジットが返金された [イベント#26]。その子キーの残りは 0 になり推論には使えなくなる */
fun refund(): ApiKey
/** この使用量に要るクレジット（購入したときの料金設計で換算）[HS-009]。 */
fun required(usage: Usage): Credit
/** 推論が行われ、クレジットが消費された [イベント#9][イベント#10]。足りなければそこまでの分だけ消費して */
fun charge(input: InferenceInput, model: ModelName, pieces: List<AnswerPiece>, finished: Boolean): ApiKey
}
テストは以下のように生成されます。
/**
* Lean: @[contract] 定理群から演繹された `ApiKey` の単体テスト。
* ふるまいは Entity interface のメソッド — 入力は実体化フック
* (fixture → 実装の Entity)で作り、返り値は観測(toFixture)で比較する。
*/
abstract class ApiKeyEntityContractTest {
/** fixture の実体化(観測が一致する実装の Entity を返す)。 */
protected abstract fun apiKey(fixture: ApiKeyFixture): ApiKey
/** fixture の実体化(観測が一致する実装の Entity を返す)。 */
protected abstract fun modelName(fixture: ModelNameFixture): ModelName
/** fixture の実体化(観測が一致する実装の Entity を返す)。 */
protected abstract fun pricing(fixture: PricingFixture): Pricing
/** ファクトリの実装を返す。 */
protected abstract fun factory(): ApiKeyFactory
/** 紐づけ直してもクレジットと明細は変わらない（フレーム）[HS-045]。 */
@Test
fun `attach は定理 attach_frame を再現する(1)`() {
assertEquals(ApiKeyFixture(id = ApiKeyId(java.util.UUID.fromString("00000000-0000-0000-0000-00000000005b")), secret = KeySecretFixture(id = KeySecretId(java.util.UUID.fromString("00000000-0000-0000-0000-00000000005b"))), owner = MemberId(java.util.UUID.fromString("00000000-0000-0000-0000-00000000005b")), listing = ListingId(java.util.UUID.fromString("00000000-0000-0000-0000-00000000005b")), provider = ProviderId(java.util.UUID.fromString("00000000-0000-0000-0000-00000000005b")), pricing = PricingFixture(inputTokensPerCredit = 4L, outputTokensPerCredit = 4L, cacheInputTokensPerCredit = 4L, cacheOutputTokensPerCredit = 4L), credits = CreditFixture(numerator = 4L, denominator = 4L), expiresOn = java.time.LocalDate.parse("2024-10-04"), parent = ParentKeyId(java.util.UUID.fromString("00000000-0000-0000-0000-000000000064")), entries = listOf<UsageEntryFixture>(UsageEntryFixture(usage = Usage(inputTokens = 4L, outputTokens = 4L, cacheInputTokens = 4L, cacheOutputTokens = 4L), credits = CreditFixture(numerator = 4L, denominator = 4L), transcript = TranscriptFixture(input = InferenceInput(body = "s0", stream = false, kinds = listOf<InputKind>(InputKind(name = "s1"))), model = ModelNameFixture(text = "s2"), answer = listOf<String>("s3")))), refunded = CreditFixture(numerator = 4L, denominator = 4L)),
apiKey(ApiKeyFixture(id = ApiKeyId(java.util.UUID.fromString("00000000-0000-0000-0000-00000000005b")), secret = KeySecretFixture(id = KeySecretId(java.util.UUID.fromString("00000000-0000-0000-0000-00000000005b"))), owner = MemberId(java.util.UUID.fromString("00000000-0000-0000-0000-00000000005b")), listing = ListingId(java.util.UUID.fromString("00000000-0000-0000-0000-00000000005b")), provider = ProviderId(java.util.UUID.fromString("00000000-0000-0000-0000-00000000005b")), pricing = PricingFixture(inputTokensPerCredit = 4L, outputTokensPerCredit = 4L, cacheInputTokensPerCredit = 4L, cacheOutputTokensPerCredit = 4L), credits = CreditFixture(numerator = 4L, denominator = 4L), expiresOn = java.time.LocalDate.parse("2024-10-04"), parent = ParentKeyId(java.util.UUID.fromString("00000000-0000-0000-0000-00000000005b")), entries = listOf<UsageEntryFixture>(UsageEntryFixture(usage = Usage(inputTokens = 4L, outputTokens = 4L, cacheInputTokens = 4L, cacheOutputTokens = 4L), credits = CreditFixture(numerator = 4L, denominator = 4L), transcript = TranscriptFixture(input = InferenceInput(body = "s0", stream = false, kinds = listOf<InputKind>(InputKind(name = "s1"))), model = ModelNameFixture(text = "s2"), answer = listOf<String>("s3")))), refunded = CreditFixture(numerator = 4L, denominator = 4L))).attach(parent = ParentKeyId(java.util.UUID.fromString("00000000-0000-0000-0000-000000000064"))).toFixture())
}
...
テストに関しては、JUnitのテストクラスとして継承してテスト対象であるコンポーネントの生成メソッドを override すればそのままテストクラスとして動作するようになっています。
これらをビルド・テストが通るように実装・継承することで、ほぼ全ての仕様が担保される想定となっています。
残ったフェーズについては、一般的なソフトウェア開発とほとんど変わらないため、割愛します。
現状の Cradle に存在する課題
Cradle はまだまだ不完全なハーネスです。ここに挙げられるだけでもこれだけあり、他にもまだ多くの課題が残っています。そのため、Cradle 自体の理念に共感してくださった方はぜひともマサカリ片手にリポジトリを覗いていって、ダメ出し等をくだされば幸いです。
- 設計が必ず軽量 DDD 的なものになる
- バッチや内部管理画面等システムレベルで分けたい物まで一緒のシステムになってしまう
- Lean によるドメインモデリングフェーズがとてつもなく遅い
- 戦略的な非機能要件設計ができない
- 「分散トランザクション」「楽観/悲観ロック」「外部決済APIの冪等性」「結果整合性」「セッション管理」などの並行性・時間・副作用が絡む領域をサブエージェントによる非機能要件レビューに任せてしまっている
- ドメインモデリングが非常に甘い。整合性境界の考慮や適切な粒度の概念分割があまりできていなさそう
- FE / BE の実装自体のハーネス整備がまだ
- AI-DLC でいう Inception フェーズと Construction フェーズの Functional Design が結合しており、実質的に要件分析と設計フェーズが融合してしまっている
- ...
終わりに
本記事では、AI駆動開発における仕様の肥大化・不整合という課題に対し、形式手法（Lean）をハーネスとして組み込むアプローチと、そのプロトタイプ実装である「Cradle」について紹介しました。
Vibe Coding やドキュメントベースの仕様駆動開発が直面している壁は、結局のところ「仕様が実行可能でなく、静的・決定論的に検証できないこと」にあります。自然言語のドキュメントをいくら AI に書かせても、コンテキストの爆発と人間の認知限界の前には破綻してしまいます。
仕様を数学的に検証可能な Lean のコードとして記述し、それを動くモックとして人間が手触り感を持って確認し、さらにテストやインターフェースへ決定論的に落とし込む。このサイクルを回すことで、初めて「人間が正しく意図を伝え、AI が仕様に忠実な実装を高速に組み上げる」という真の仕様駆動開発が成立するのではないかと考えています。
もちろん、残っている課題で触れた通り、モデリングの実行速度や非機能要件の担保、設計パターンの柔軟性など、プロダクション適用に向けて乗り越えるべき壁は山積みです。定理証明支援系を実務の Web 開発プロセスに滑らかに組み込む試みは、まだ始まったばかりと言えます。
それでも、「仕様の検証を自然言語のあやふやさから解放し、数学とコードの堅牢な基盤の上で行う」という方向性には大きな可能性を感じています。
もしこのアプローチに少しでも面白みや可能性を感じていただけたら、ぜひ GitHub リポジトリ を覗いてみてください。「ここはどう考えているの？」「形式手法ならこういうアプローチもあるのでは？」といったフィードバックやマサカリ、Issue や PR を心よりお待ちしています。
また本記事で登場した Lean や Kotlin のコード例は Cradle を用いて開発したサンプルプロジェクト LLMX から加工・引用したものになります。Cradle を利用して開発されたシステムがどのようなものになるか気になる方は、こちらも併せてご確認いただければ幸いです。