かつてプログラマーの仕事は、かなりの部分が「実装すること」だった。要求を読み、仕様を理解し、関数を書き、型を定義し、テストを書き、エラーを潰し、フレームワークの作法に従ってコードを積み上げていく。もちろんそこには設計も判断もあったが、実際の作業時間の多くは、抽象的な構想を具体的なコードへ変換することに費やされていた。
しかし、生成AIの登場によって、その前提は大きく変わりつつある。
今やAIは、かなりの量のコードを書くことができる。関数を実装し、テストを生成し、APIを呼び出し、UIコンポーネントを組み立て、エラーハンドリングまで含めたコードを提案することができる。かつて人間が一行ずつ書いていた部分を、AIが高速に生成するようになった。
では、人間の仕事はなくなるのか。
私は、そうは考えていない。
むしろ逆である。AIがコードを書く時代になったからこそ、人間が担うべき仕事は、より本質的な場所へ移動している。
それは、コードを書くことではなく、コードになる前の構造を設計することである。
AIはコードを書ける。
しかし、何を正しい構造とみなすべきかは、まだ人間が決めなければならない。
どの状態が存在するのか。
どの操作が許されるのか。
どの不変条件が守られなければならないのか。
あるモジュールの出力は、別のモジュールの入力条件を満たしているのか。
複数のAIエージェントが協調して開発するとき、互いの成果物はどのような契約によって接続されるべきなのか。
私の研究と活動は、この問いに向かっている。
自然言語仕様の限界
AIに開発を任せるとき、多くの人は自然言語で指示を出す。
「注文管理システムを作ってください」
「在庫が足りない場合は注文できないようにしてください」
「決済が成功したら注文を確定してください」
「キャンセル済みの注文は再度確定できないようにしてください」
こうした指示は、人間にとっては一見わかりやすい。けれど、ソフトウェアの仕様としては曖昧である。
「在庫が足りない」とは、どの時点の在庫を指すのか。
注文を確定する前に在庫を予約するのか、それとも決済後に減算するのか。
決済に失敗した場合、注文状態はどこに戻るのか。
キャンセル済みの注文に対して、返金処理はどの状態で行われるのか。
複数のモジュールが並行して開発されたとき、それぞれの前提は本当に一致しているのか。
人間同士であれば、会話によって補正できるかもしれない。
しかし、AIエージェントが複数に分かれて開発するようになると、この曖昧さは一気に問題化する。
注文モジュールを担当するAI。
在庫モジュールを担当するAI。
決済モジュールを担当するAI。
UIを担当するAI。
テストを担当するAI。
それぞれのAIが自然言語の仕様を読み、それぞれの解釈でコードを書く。すると、単体では正しく見えるコードが、結合した瞬間に壊れる。
原因はたいてい、コードの文法ミスではない。
仕様の境界が曖昧だったことにある。
つまり問題は、AIがコードを書けないことではない。
AIに渡される「構造」が曖昧であることなのだ。
形式仕様という骨格
そこで私は、AI時代の開発に形式手法を持ち込むことを考えている。
形式手法とは、ソフトウェアの仕様を数学的に明確な形で記述し、検証するための方法である。私が特に注目しているのが VDM-SL である。VDM-SL は、状態、型、不変条件、事前条件、事後条件を明確に記述できる仕様記述言語であり、実装コードを書く前に「このシステムは何であるべきか」を表現することができる。
私にとって VDM-SL は、単なる古典的な形式仕様言語ではない。
それは、AIに構造を渡すための言語である。
自然言語は柔らかい。
人間にとっては扱いやすいが、解釈の余地が大きい。
コードは具体的である。
しかし、実装の細部に入り込みすぎると、背後にある設計意図が見えにくくなる。
その中間に、形式仕様がある。
形式仕様は、コードではない。
しかし、自然言語よりはるかに厳密である。
そこには、状態があり、制約があり、操作があり、操作前に満たすべき条件があり、操作後に保証されるべき結果がある。
つまり形式仕様は、ソフトウェアの骨格である。
AIにコードを書かせる前に、この骨格を定義する。
AIが生成したコードが、この骨格に沿っているかを確認する。
複数のAIエージェントが協調するとき、それぞれの境界を契約として記述する。
これが、私の研究の中心にある考え方である。
Formal Agent Contracts
私が取り組んでいる Formal Agent Contracts は、この問題意識から生まれている。
これは、複数のAIエージェントが協調して開発を行うとき、エージェント間の約束事を形式仕様として定義し、検証し、必要に応じてコード生成へつなげるための仕組みである。公開されている説明では、Claude Code プラグインとして、自然言語から VDM-SL 仕様を定義し、VDMJ による検証、Z3 によるSMT証明、TypeScript/Python のスキャフォールド生成などを扱う構成が紹介されている。(IID.systems)
ここで重要なのは、開発者が必ずしも VDM-SL の専門家である必要はない、という点である。
従来、形式手法は難しいものだと考えられてきた。実際、厳密な仕様を書くには学習コストがある。数学的な記法に慣れていない開発者にとっては、導入の壁も高い。
しかし、AIが自然言語と形式仕様の間を翻訳できるなら、その壁は低くなる。
開発者は、まず自然言語でドメインのルールを説明する。
AIがそれを VDM-SL の形式仕様に変換する。
AIは、その仕様が何を意味するのかを再び自然言語で説明する。
人間は、その説明が本当に業務ルールに合っているかを確認する。
検証ツールが、仕様の矛盾や証明責務をチェックする。
その後、AIが仕様に沿って実装の雛形を生成する。
この流れでは、人間の役割は「コードを書く人」から「意味を判断する人」へ移る。
人間は、実装の細部をすべて手で書く必要はない。
しかし、何が正しい業務ルールなのか、どの状態遷移が許されるのか、どこに危険な曖昧さがあるのかを判断しなければならない。
AIが手を動かす。
人間が構造を決める。
この分担こそ、AI時代の開発における重要な転換だと考えている。
formal-spec-driven-dev
この考え方を、より広い開発方法論として整理したものが formal-spec-driven-dev である。
これは、テストファーストの発想を否定するものではない。テストは依然として重要である。外部システムとの結合、性能、UI、実際のユーザー操作、運用上の振る舞いを確認するには、テストが必要である。
しかし、AI時代の開発において、テストだけを中心に置くのは不十分である。
テストは有限個のケースを確認する。
形式仕様は、満たすべき性質そのものを記述する。
テストは「この入力では正しく動いた」と言う。
形式仕様は「この操作は、常にこの条件を満たすべきである」と言う。
AIが大量のコードを生成する時代には、個別のコード片をあとからテストで追いかけるだけでは追いつかない。むしろ先に、システムが満たすべき構造を定義する必要がある。
formal-spec-driven-dev は、そのための開発パラダイムである。
人間とAIが対話しながら仕様を定義する。
仕様をもとにモジュールを分割する。
モジュール間の契約を記述する。
複数のAIエージェントが、それぞれの仕様に基づいて並列に実装する。
最後に、コードが仕様と整合しているかを検証する。
公開記事では、VDM-SL 仕様をAIエージェント間の契約として使い、Order、Inventory、Payment などのモジュールを分割して開発する例が紹介されている。そこでは、人間の役割は不要になるのではなく、ドメイン専門家、アーキテクト、品質判断者として高い位置に移ると説明されている。(DEV Community)
この考え方は、私にとって非常に重要である。
なぜなら、AI時代に問われるのは「人間がコードを書けるか」ではなく、人間が正しい構造を見抜けるかだからである。
AI時代に、形式手法が再び意味を持つ
形式手法は、新しいものではない。
むしろ長い歴史を持つ。高信頼性が求められる領域では、仕様を厳密に記述し、検証する考え方は以前から存在していた。しかし一般的なソフトウェア開発に広く普及したとは言いがたい。
理由は明確である。
難しいからである。
時間がかかるからである。
形式仕様を書ける人が少ないからである。
短期的な開発現場では、実装してテストした方が速いと考えられがちだったからである。
しかし、AIによって状況が変わった。
AIは、形式仕様を書く補助ができる。
AIは、仕様を自然言語で説明できる。
AIは、仕様からコードの雛形を生成できる。
AIは、検証エラーを読み、人間に説明できる。
つまり、形式手法の弱点だった「扱いにくさ」を、AIが補える可能性がある。
そして同時に、AIの弱点である「曖昧な指示に対して、それらしいが不確かなものを生成する」という問題を、形式手法が補える。
AIは形式手法を使いやすくする。
形式手法はAIを安全に使いやすくする。
この相互補完こそ、私が見ている可能性である。
私の活動の本質
私の活動は、単に VDM-SL を広めることではない。
単に Claude Code のプラグインを作ることでもない。
単にAIコーディングを便利にすることでもない。
私が取り組んでいるのは、AI時代におけるソフトウェア開発の責任の置き場所を再定義することだ。
AIがコードを書くなら、人間は何をするのか。
AIが複数のモジュールを並列に実装するなら、それらは何によって接続されるのか。
自然言語の曖昧な仕様では足りないとき、何をAIに渡せばよいのか。
テストだけでは保証しきれない正しさを、どのように設計段階で扱うのか。
人間のドメイン知識を、AIが誤解しにくい形にするにはどうすればよいのか。
その答えとして、私は形式仕様に注目している。
形式仕様は、AIにとっての契約である。
人間にとっての確認可能な設計図である。
モジュール間の境界を明確にする約束事である。
コードが生成される前に存在すべき骨格である。
これからの開発では、コードの量はますます増えるだろう。
AIによって、実装速度はさらに上がるだろう。
しかし、速度が上がるほど、間違った方向へ進んだときの被害も大きくなる。
だからこそ、最初に構造を定める必要がある。
何を作るのか。
何を保証するのか。
どこまでをAIに任せるのか。
どこを人間が判断するのか。
どの境界を契約として固定するのか。
私の研究は、その問いに対する一つの実践である。
人間は、より上流へ移動する
AI時代の開発において、人間は不要になるのではない。
人間は、より上流へ移動する。
コードを書く人から、構造を定義する人へ。
実装の細部を追う人から、状態と制約を判断する人へ。
テストケースを積み上げる人から、満たすべき性質を定義する人へ。
AIに命令する人から、AIが誤解できない契約を設計する人へ。
もちろん、これは簡単な移行ではない。
自然言語の要求を形式仕様に落とすには、ドメイン理解が必要である。
AIの出力を鵜呑みにせず、意味を確認する力も必要である。
仕様が業務の現実と合っているかを判断するには、現場感覚も必要である。
しかし、だからこそ人間の役割は残る。
むしろ、そこにこそ人間の価値がある。
AIはコードを書く。
しかし、何が正しいかを最終的に判断するのは人間である。
AIは仕様を生成する。
しかし、その仕様が現実の業務や目的に合っているかを判断するのは人間である。
AIは複数の実装案を出す。
しかし、どの構造が長期的に保守可能で、どの境界が破綻しにくいかを決めるのは人間である。
私は、この人間の役割を軽視したくない。
AI時代に必要なのは、人間を開発から追い出すことではない。
人間の判断を、より本質的な場所に置き直すことである。
形式仕様は、AIに渡すための設計図である
建築には設計図がある。
大きな建物を作るとき、職人がそれぞれ自由に作業を始めるわけではない。構造、寸法、材料、荷重、配管、電気系統、避難経路。そうしたものが設計図として共有される。
ソフトウェアにも、本来それが必要である。
しかし、従来のソフトウェア開発では、その設計図が自然言語の仕様書や、暗黙の会話や、既存コードの雰囲気に依存していることが多かった。
人間だけで開発しているうちは、それでも何とかなる場合があった。
しかし、AIエージェントが複数参加する開発では、暗黙知は通用しにくい。
AIには、明確な契約が必要である。
このモジュールは何を受け取るのか。
どの条件を満たしていなければならないのか。
何を返すのか。
返した結果は、どの不変条件を守っているのか。
次のモジュールは、その結果をどの前提で受け取るのか。
それを曖昧な文章ではなく、検証可能な形で書く。
これが、私の考えるAI時代の設計図である。
形式仕様は、AIを縛るためのものではない。
AIに自由に動いてもらうために、境界を明確にするものである。
ルールのない自由は、破綻を生む。
契約のある自由は、協調を生む。
Formal Agent Contracts という名前に込められているのは、おそらくこの発想である。
私が目指しているもの
私が目指しているのは、形式手法を一部の専門家だけのものにしないことである。
形式仕様は、本来もっと広い開発者に使われてよい。
しかし、そのままでは難しい。
だからAIを使う。
AIに形式仕様を書かせる。
AIに形式仕様を説明させる。
AIに検証結果を解説させる。
AIにコード生成を任せる。
人間は、その意味が正しいかを判断する。
この形であれば、形式手法は特別な専門家だけの道具ではなく、AI時代の実用的な開発基盤になり得る。
重要なのは、AIにすべてを任せることではない。
AIと人間の間に、検証可能な中間表現を置くことである。
自然言語だけでは曖昧すぎる。
コードだけでは遅すぎる。
テストだけでは網羅できない。
だから、形式仕様を置く。
そこに、私の研究の核がある。
結び
AIがコードを書く時代に、私はコードそのものではなく、コードになる前の構造に注目している。
ソフトウェアは、文字列としてのコードの集まりではない。
状態があり、制約があり、操作があり、責務の境界があり、モジュール間の契約がある。
AIがいくら速くコードを書けても、その構造が曖昧であれば、システムは壊れる。
逆に、構造が明確であれば、AIは強力な実装者になる。
だから私は、形式仕様をAI時代の開発の中心に置きたい。
人間がドメインを理解する。
AIが形式仕様への変換を助ける。
検証ツールが構造の矛盾を検出する。
AIエージェントが契約に従って実装する。
人間が意味を確認し、最終的な判断を下す。
これは、人間を不要にする開発ではない。
人間を、より本質的な場所へ戻す開発である。
コードを書くことから、構造を設計することへ。
実装の速度から、仕様の正しさへ。
曖昧な指示から、検証可能な契約へ。
私の活動は、その移行を実現するための試みである。