コードが書けることの価値が消えた後で、何が残るか

一年前、腕のいいエンジニアの時給が話題になっていました。ベテランが一日で書くコードの量、若手が一週間かけて直すバグの修正速度、そういう尺度で人の価値が測られていた時期がありました。いまそれをそのまま言う人はだんだん減っています。週末にAIに書かせた三百行のコードが動いてしまったときの、あの不思議な気持ちを誰もが一度は味わったからです。

価値の移動ではなく、ボトルネックが静かに上流へ逃げていく現象が起きています。「コードが書ける」という能力は、多くのエンジニアが思っていたよりずっと周辺的な能力でした。中心は別のところ、ピーター・ナウアが 1985 年に「理論形成」と呼んだ営みの側に、ずっとあったのです。AI はそれを暴いただけだ。

その「中心」を見るには、AIの知性と、型検査やlint、形式手法が提供する知性の対比を経由するのが早道です。前者は帰納的で、後者は演繹的。両者は長く対立項として扱われてきましたが、いまその関係は逆転しつつあります。片方の弱みを、もう片方の強みが埋める。この補完性を理解しているかどうかで、AI時代の組織設計の筋が分かれます。

一段目の答えは「仕様を書く力」に見える

コードが書けないならどうするか、という問いに、いまいちばん元気のある答えがSpec-Driven Development (仕様駆動開発) です。2026年の初めに出たサーベイ論文は、こう宣言しています。コードは仕様の実装詳細にすぎず、逆ではない、と。従来は「コードが真実でドキュメントは後追い」でしたが、SDDは仕様をプログラムの根拠に格上げして、継続的インテグレーションで執行可能な契約にまで持ち上げます。仕様とコードがずれたらビルドが落ちる、というところまでやる。

同じ論文には、AI時代の決めゼリフがあります。AIはパターン補完には優れているが読心術は下手だ、というのがそれです。曖昧なプロンプトは推測で埋められる。だから人間の判断を仕様として外側に固定し、推測の余地を減らそう、という発想です。SDD界隈はこの手の「vibe coding批判」で勢いを得ました。プロンプトにノリで流し込めば、AIはそれなりの何かを返してくる。けれどそれなりの何かは、それなり以上にはならない。

コードが書けることの価値が消えても、仕様を書ける力が新しい希少性になる。この希望は一年持ちませんでした。

仕様も、同じ崖を下りる

英国のソフトウェア工学者ローレンス・トラットが、生成AIとプログラミングについて早い時期に書いた論考があります。彼はそこで、ユーザーレベルの仕様はほぼ常に不完全だ、と書きました。良いソフトウェアが扱わねばならないことを、ユーザーの言葉はいつもどこかで漏らしてしまう。ハッシュマップを使ってくれ、と言う顧客はいません。でも「速くしてくれ」の一言が、実装上の選択をすでに規定しています。

さらにトラットは嫌な指摘をします。中規模以上のソフトウェアを書こうとした瞬間、仕様は同じ規模のプログラムと変わらない分量に膨らむ、と。仕様を書き切る努力の終点には、結局プログラマーの仕事が待っています。暗黙知を言葉にしてAIに渡そう、という類のDXプロジェクトが例外なく詰んでいく理由は、だいたいこれです。

Isoformというチームはもっと直截です。仕様はLLMが必要とする文脈を原理的に捕捉しきれない、と彼らは書きます。エッジケースは使われてから現れる。性能問題は負荷がかかってから現れる。ユーザーの本当の振る舞いはリリース後に現れる。書き手の精度を上げても解決しません。現実は仕様よりも速く変わる、という一文が彼らの立場を要約しています。

SDD導入現場からの実直な悲鳴も上がっています。フランスのある開発者は「ウォーターフォールの逆襲」と名付け、Requirements.md、Design.md、Tasks.mdを事前に作り込むワークフローが、90年代のウォーターフォールと顔つきがそっくりだと指摘しました。読むことに時間の8割が溶ける、擬似コードと実装コードの二重レビューで手間が倍増する。自然言語を曖昧さのない水準まで精密化しようとすると、結局はコードそのものに戻ってしまう。これがSDDの行き止まりです。

仕様を書く能力もまた、AIが追いついてくる対象に落ちます。コードの延長線上に仕様を置いた瞬間、同じ崖を下りる。

自然言語の仕様が穴だらけで、精密にしようとするとコードに近づいていくなら、いっそ機械が厳密に解釈できる「形式言語」で書き下すほうが筋がいい。lintや型検査、そしていわゆる形式手法と呼ばれる道具群、たとえばTLA+、Lean、Dafny、Alloyといった言語が、この方向の蓄積にあたります。ソフトウェア工学にずっと前から存在した系譜ですが、学習コストと導入コストが高すぎて、OSカーネルや分散プロトコル、航空宇宙のような一部の領域でしか使われてきませんでした。金融や学術の隅っこで細々と生きていた、と言ってもいい。

この古い道具が、AIとの組み合わせで景色を一変させつつあります。

帰納と演繹、ふたつの知性

片方は候補を量産し、もう片方が反例で却下する。長く対立してきたふたつの知性が、いまその関係を逆転させつつあります。

AIが見せる知性は、帰納的な知性です。膨大な過去の事例から、いまの入力に似たパターンを引き寄せ、「だいたいこう」という出力を返します。統計的にもっともらしい回答を返す、と言い換えてもいい。強みは未知の入力にも何らかの見解を持てる広さで、弱点は「もっともらしい」と「正しい」の区別がつかないことです。LLMの幻覚は、この知性の様式から必然的に生まれる副作用です。

これに対して、lintやコンパイラの型チェック、TLA+やLean、Dafny、Alloyのような形式手法が提供するのは、演繹的な知性です。厳格に定義された規則から、論理的に結論を導く。強みは結論が保証されることで、弱点は適用範囲が狭いことです。規則の中にないものは何も言えません。自由律俳句を評価させようとしても、ガベージコレクタは黙るしかありません。

このふたつは長く、対立するものとして扱われてきました。AIは自由だが信頼できない、形式手法は信頼できるが手間がかかる、と。一方を取れば他方を失う二項対立でした。

AlphaProofと、最難問P6

この対立の常識が崩れる象徴的な事件が、2024年夏に起きました。グーグルのDeepMindが作ったAlphaProofというシステムが、国際数学オリンピックで銀メダル水準の成績を出したのです。翌2025年のIMOでは、同じグーグル系のGemini Deep Thinkがゴールド水準を達成しています。

仕組みはこうです。AlphaProofは数学の証明をLeanという形式言語で学習します。解くべき問題に対して、候補となる証明の方針を大量に生成する。Leanの証明チェッカーは、そのうち厳密に正しいものだけを受理します。間違った候補は機械的に却下され、AIは次を試す。

世界の数学エリート600人のうち5人しか満点を取れなかった最難問P6を、この往復で機械が解いてみせました。帰納的に候補をばらまくAIと、演繹的に嘘を見抜く検証器の、奇妙に見事な協働です。AIがいくら幻覚を起こそうと、証明チェッカーは通さない。通さないから、AIはまた別の候補を作る。この非対称性のおかげで、LLM単独では届かなかった正しさに手が届きました。

数学者テレンス・タオが2025年にやっていたことは、もっと示唆的です。彼はChatGPTに自分の論文をLeanの形式証明に翻訳させ、1,125行の検証済み証明を人間とAIの協働で完成させました。タオ自身がこれを、指揮者とアドリブ演奏者の即興演奏に喩えています。人間が全体のラインを示し、AIがLean用のコード片を即興で書き、Leanがその正しさを判定する。フィールズ賞受賞者である彼が、形式検証を「AI時代の数学をスケールさせる鍵」と位置づけた意味は重い。AI、大規模化、多人数の参加。こうした変化が数学研究にとって総体としてプラスに働くのは、形式検証が嘘を弾いてくれるおかげだ、とタオは語っています。

Alloyが反例を吐いた日

この協働はソフトウェア設計の外にも広げられます。業務分析の題材として、私が理事を務めている日本CTO協会の組織構造をAlloyにかけてみたことがあります。

一般社団法人というのは、思った以上に組み合わせが多い組織です。会員区分、役職、運営参画の種類、作業グループでの立場。軸が4つあって、それぞれに複数の値が入る。一人の人間は、そのそれぞれで何かを持っていたり持っていなかったりします。そこから誰が何をできるかを導こうとすると、組み合わせは人間の目で読み切れる量を超えます。しかも、ガバナンス上絶対に守りたい非自明な性質があります。監事は事務局長を兼ねてはいけない (監査の独立性)、代表理事でも事務局長を兼ねない限り管理者にはならない、役員交代で管理者権限が揮発しない、という類のルールです。

ふつうにドキュメントで書き下せば、抜けが生まれます。コードレビューで気づける範囲も狭い。AIに草案を書かせてもいいですが、その草案が整合しているかを人間が読み切るのは難しい。こういう場面で使えるのがAlloyという形式手法のツールでした。Alloyはモデル化した世界の中に「この性質が必ず成り立つ」というassertionを書いておくと、5要素くらいの小さな世界で全組み合わせを探索し、反例があれば具体的なインスタンスとして返してくれます。

`

// 監事は事務局長を兼務できない（監査の独立性）

fact AuditorCannotBeChief {

all p: Person |

(some ot: p.officerTerms | ot.role = Auditor)

implies (no se: p.staffEngagements | se.staffType = Chief)

}

// 役員交代で管理者権限は揮発しない

assert AdminSurvivesOfficerChange {

all p: Person |

(some se: p.staffEngagements | se.staffType = Chief)

implies effectiveGlobalPerm[p] = GP_Admin

}

check AdminSurvivesOfficerChange for 5

`

AIや人間が書いたルールをAlloyにかけると、矛盾があれば「Person$0は監事かつ事務局長です」といった具体的な反例を吐いてきます。言葉で追うと一生気づけない穴を、機械が秒で見つけてくれる。ソフトウェアの設計ではなく、組織のガバナンスルールを書くような場面でも、この「反例を機械に探させる」営みが成り立ちます。

候補を出す側 (設計者、AI、あるいはその両方) が帰納的に案をひねり出し、Alloyの検証器が演繹的にそれを殴り返す。通らなければ案を作り直す。通ったとき、そのルールは組み合わせ爆発の全域にわたって整合していると保証されます。AlphaProofと同じ構造です。

「帰納と演繹、補い合う」は抽象論ではありません。すでに現場で、組織のガバナンス設計にも、分散システムのプロトコル検証にも、マイクロカーネルの安全性証明にも使われている道具立てになっています。AIが業務ルールの草案を大量に生成し、Alloyのような形式手法が矛盾を具体的な反例で返す。この往復があれば、非技術領域のビジネス分析ですら、AIと形式手法の協働で精度を上げられます。

なぜ補完が強いのか

この組み合わせが強いのは、それぞれの弱点を相手が埋めるからです。AIの帰納は、厳密な論理的探索を苦手とする代わりに、無数の可能性のなかから「それっぽいもの」を引き当てる瞬発力を持つ。形式手法の演繹は、AIが苦手な「嘘を見抜く」ことを数学的に保証する代わりに、「何を考えるべきか」を自分で決められない。片方だけだと袋小路に入ります。帰納だけではでたらめを正しいと思い込みますし、演繹だけでは問題空間の広さに負けます。

ソフトウェア開発の現場に戻ると、AIコード生成とlint、型検査、テスト、形式検証の関係が、実は数学証明と同じ構造をしています。AIが書く帰納的なコードを、演繹的なツールが殴り返す。殴られた側は候補を作り直す。このループが回っているかぎり、AIは単独で出すには危うすぎる出力を、使える品質まで引き上げていけます。これまで型検査やlintは「便利な補助ツール」として扱われてきましたが、AI時代においては役割が変わります。AIの帰納の暴走を押さえる、演繹的な重しとしての役割が、本質的になります。

形式手法の民主化と、その本当の限界

この補完性が見えると、マーティン・クレップマンが2025年末に公開した予測記事の意味もはっきりしてきます。タイトルは「AIは形式検証をメインストリームにする」。

彼の見立てはこうです。これまで形式検証は、経済性が悪すぎて普及しませんでした。seL4というOSカーネルの形式検証は、8,700行のCコードに20人年と20万行の証明を要しました。この経済性の悪さが、形式手法を大学の教科書の中に閉じ込めてきた。ところがAIがタダ同然に証明を書き続けるなら、この経済性は逆転します。AIが生成したコードをわざわざ見る必要すらなくなる、コンパイラが吐いた機械語をわざわざ読まないのと同じように、とクレップマンは書いています。

実装側も動いています。アップルの研究チームが公開したHilbertというシステムは、数学証明の標準ベンチマークで 99.2% という桁違いの成績を出しました。Dafny や Verus のような形式検証言語でも、AI が証明を書く成功率は上がり続けています。

ここまでだと、AI時代の最終解が見えた気がしてくる。コードを書かない、仕様を書かない、検証も書かない、全部AIに任せて結果だけ受け取ればいい、と。

民主化論のおもしろいところは、その先にあります。

クレップマン自身が、自分の楽観論に静かに留保を付けています。形式仕様の読み書きには依然として専門性と慎重な思考が要る、と。AIが民主化するのは「検証を実行するコスト」であって、「仕様を書く能力」ではない。制限要因は技術ではなく文化の変化だ、と彼は結んでいます。

産業側の実証も同じ方向を指します。2011年からTLA+を使い続けているアマゾンのAWSは、S3やDynamoDB、Auroraの中核で形式手法を武器にしてきました。彼らが15年かけて学んだ最大の教訓は、技術ではなく普及の作法だったといいます。エンジニアに売り込むとき、「formal methods」「verification」「proof」という言葉を使わなかった。代わりに「Debugging Designs (設計のデバッグ)」と呼びました。

民主化とは、概念を広めることではなく、概念を隠すことだ、と言えます。型チェックをしていることを気にするプログラマーはいない。ガベージコレクタの挙動を普段意識する人もいない。形式手法が本当に普及するとすれば、到達点は「AIが内部で勝手に使っていて、人間は意識もしない」状態です。

仕様を書ける人という称号に希望を託した人にとって、この道はあまり長くありません。仕様を書く能力は民主化しない。だからこそ希少なのだ、と喜ぶ前に気づくべきことがあります。それが希少性として残るのは、仕様がまだ目に見える場所にある間だけだ。

保守しなくていいコードには、検証もいらない

民主化論を根底から揺さぶる視点が、もうひとつあります。形式検証の楽観論に対して、あるオンラインコミュニティの開発者が短いコメントを残していました。ソフトウェア品質を重視する経営者は少数派だ、そしてAIは保守性の必要性そのものを消しにかかっている、という観察です。

この一行は静かに重い。AIがコードを書き直す速度が上がれば上がるほど、コードは使い捨てになります。使い捨てのコードに形式検証をかける動機は、そもそも生まれない。民主化のコストが下がっても、需要そのものが先に消える可能性がある、という話です。

AIはコードをタダにしたのではなく、コードを「書き捨てるもの」に変えつつあります。紙のメモとエクセルファイルの中間みたいなものになる。動けば勝ち、動かなければ捨てる、次もAIに頼む。そういう世界では、長く保守する価値のあるコードはむしろ少数派になります。

形式手法が生き残るのは、保守する経済合理性があるドメインだけです。決済基盤、医療機器のファームウェア、クラウドの分散プロトコル、航空機の制御系。それ以外の大半、社内ツールや業務アプリや広告最適化のコードに、証明器を回す気はだれも起こさないでしょう。

どこを使い捨てにして、どこを守るか。全部を守ろうとすれば破産しますし、全部を使い捨てれば組織が空洞化します。この線引きは技術的な判断ではなく、経営判断です。そして線を引ける人は、いまだにほとんどいません。

ナウアが1985年に区別したもの

こういう議論を繰り返していると、どうしても1985年のピーター・ナウアの論文「Programming as Theory Building」に戻ることになります。ナウアはデンマークの計算機科学者で、ALGOL 60の仕様策定にも関わった人物です。1985年に出たこの論文は、当時のソフトウェア工学の主流とは違う方向を指していました。その後のアジャイル運動のなかでAlistair Cockburnらが参照し、いまAI時代に改めて読み直されています。

プログラマの仕事には、人から人へ伝えられるものと、伝えられないものがある。ナウアは三つの層に分けました。コード。仕様やドキュメント。そして理論。コードは読めば見える。仕様やドキュメントにも書ける。けれど三つ目の「理論」はどちらにも書き下せない。人間の頭の中にしか宿らない、と彼は言います。

「理論」というのは、その領域についての深い理解のことです。なぜこの設計にしたのか。どんな変更ならシステムの整合を壊さないか。どのエッジケースを意図的に無視しているか。バグが出たとき、どこを疑うべきか。こういう判断ができる状態を、ナウアは「理論を持っている」と呼びました。

彼の論文には、刺さる具体例が出てきます。ある会社がコンパイラの保守を別のチームに引き継いだ。元のチームは十分なドキュメントを残し、仕様も書き、コメントも書いた。客観的に見て資料は揃っていた。ところが新チームがバグを直そうとすると、毎回おかしな副作用が出た。なぜこのコードがこうなっているか、の「なぜ」がどこにも書いていなかったのです。結局、新チームは自分たちで理論を再構築するしかなく、ほぼ書き直しになりました。

プログラムの死は、その理論を持っていたチームが解散したときに訪れる、とナウアは結論します。コードが残っていても、理論が失われれば、そのプログラムはもう変更を受け付けません。

私が以前『エンジニアリング組織への招待』で書いた「不確実性の削減」と、これはほぼ同じ構造を指しています。対象領域について「こうなるはず」と予測できる状態こそが理論であり、それが組織に宿っていないと、変更のたびに当てずっぽうで動くしかない。理論を宿らせる営みと、不確実性を減らす営みは、同じことを別の言葉で語っています。

この視点で現在のSDD論争を見ると、景色がはっきりします。仕様を書くのは人間の理論で、仕様はその理論の痕跡にすぎない。仕様を精密にしていくほど、仕様を正しく読める人間には仕様の背後の理論が必要になります。仕様は理論の代わりになりません。Alloyのassertionも同じで、assertionを書く人間にはドメインの理論が要ります。assertionは理論を機械にチェックさせるための翻訳であって、理論そのものではありません。

AIが作った正しそうなコードと仕様を受け取る組織に、密かに積み上がるものがあります。知識の負債、と呼ぶ論者もいます。コードは動く、テストも通る、仕様もそれっぽい。けれどなぜそうなっているのかを説明できる人間は、組織の中にいない。ナウアの言う「プログラムの死」が、最初から組み込まれた状態で開発が進む、という奇妙な光景が生まれます。

帰納的な知性と演繹的な知性を組み合わせる仕組みができても、どんな問いを立てるか、どの仕様を書くかは人間の理論に戻ってきます。タオがLeanとChatGPTの即興演奏で指揮者の役を担ったように、人間は「何を証明すべきか」を決める側に残ります。AlphaProofは最難問を解けましたが、「その問題を解く価値があるか」を決めたのは国際数学オリンピックの出題委員会です。AIとツールの連合軍は、問われた問いに答える速度を上げる。問いを立てる仕事は、人間のところに残ります。

ボトルネックは、上流に逃げる

コードが書ける価値は下がる。仕様を書ける価値は一瞬上がってまた下がる。検証の価値はコンパイラのように不可視化される。残るのは何でしょうか。

残るのは、解決空間の外側にある仕事です。プロダクト開発業界でマーティ・ケーガンが長く主張してきた「問題空間」のほうです。ただし、問題空間があれば解決空間は簡単に埋まる、という素朴な発想もまた、ケーガン自身が戒めています。問題を見つける仕事と、解を見つける仕事は、別の筋肉を使うからです。

ニック・チューンは、問題と解決の二分法そのものを古いと言います。彼が提案するのは、問題・戦略・解決の三段構えです。問題を見つける、どの問題に資源を張るか決める、決めたものを解く。AIが強くなるほど、一番下の解決が薄くなり、一番上の問題の輪郭が太くなり、真ん中の戦略がボトルネックになります。そして問題層の中心に座っているのが、前章で見たナウアの「理論形成」だ。

真ん中の戦略層は、日本企業ではほぼ空席です。AI に投資する予算は解決層に注がれ、問題層と戦略層は組織図にすら立っていない。

以前 NewsPicks に書いた「消える生産性」と、この構造は同じです。赤の女王の国で生き残るには、走り続けるだけではだめで、どの方向に走るかを決めた者だけが前進する。AIで解決側を高速化しても、競合も同じ速度で高速化しますから、相対的には何も変わりません。勝ち負けは、解決の速度ではなく、戦略と問題の選び方で決まります。

残るもの

経営者とCTOがやることは、ここから 3 つの方向に分かれます。

区別する目を持つこと。AIがコードを大量生産する時代、どこを使い捨てにして、どこを守るかを決められるのは経営判断だけです。形式手法は守る側にしか効きません。守るべき領域を見極める力が、コードを書く力よりはるかに希少になります。

問題定義の筋肉を鍛えること。解決のコストが下がるほど、「何を解くか」の違いが成果の違いを決めます。日本のAI投資が解決の効率化ばかりに偏っているのは、問題の筋肉が弱いから。組織図と予算配分を、問題側に作り替える必要があります。

理論形成の場を作ること。ナウアの指摘した「理論は書き下せない」という事実は、AI時代にむしろ重くなっています。AIが帰納的に、形式手法が演繹的に、両方から攻めて埋められるのは解決空間の大半だけで、理論そのものは人間の頭の中に宿るしかない。理論を持つ人はだれか、どう継承するか、どう更新するか、という問いは経営の問いだ。仕様書を一万行書かせても、Alloyのassertionを千本通しても、この問いには触れません。

「コードが書けること」は、実は周辺的な能力でした。中心にあったのは、問題を見つける力、戦略を決める力、理論を組織に宿らせる力で、この構造はAIが来ても変わっていません。変わったのは、解決のコストが下がった分、この中心が裸で露出したという一点だ。

コードが書けることの価値が消えても、たぶん何も困らない。本当に困るのは、消えた価値に気づかず、同じ場所を効率化しようと予算を使い続けることです。それは赤の女王の走り方。止まれば負ける気がするから走りますが、走っても前には進みません。