定理証明・形式検証はいまから学ぶ価値があるか ── なぜ「人が仕様を書く」必要があるのか、Lean 4 から始める学習ロードマップ

先に、結論だけ申し上げます。

形式証明は「プログラムのバグを、すべて消す魔法」ではありません。 人間が「何を保証したいか」を仕様として書き、その仕様に対してプログラムが正しいことを、数学的に検証する技術です。

それゆえに、仕様を自分で書き下す必要がある場所 ── 暗号ライブラリ、OSカーネル、コンパイラ、認可エンジンといった「基盤」 ── で、とりわけ価値を持ちます。

日本の一般的なWeb開発では、急に必須になる技術ではありません。 その点は、隠さずお伝えします。

しかし、AIエージェントや Physical AI に「何をさせてよいか」を定める仕様の層では、今後、重要性が増す可能性があります。

そして学び始めるなら ── 命題論理・述語論理・自然演繹まで来たら、もう Lean 4 を触ってよい、というのが本記事の答えです。

この記事はLeanの使い方を解説する記事ではありません。

AIエージェント時代に「人間が仕様を書く」とはどういうことかを考え、その入口としてLean 4を紹介する記事です。

---

「プログラムにバグがないことを、テストではなく、数学で証明する」

そんな技術があると聞いたとしたら、どう思われるでしょうか。

夢物語のように聞こえるかもしれません。

しかし、それは現実に存在し、航空機やロケット、暗号や金融システムといった、間違いが許されない場所で、静かに使われています。

その技術を担うのが、Lean、Rocq（旧 Coq）、Agda、Idris、Isabelle といった言語です。

より正確に言えば、本記事が主役として扱うのは、数学的な証明を人間が構成し、コンピュータがその正しさを検証する「対話的証明支援系」 と呼ばれる系統の道具です。

近年は、数学者が難問の証明を機械で検証したり、AI が生成した答えの正しさを保証したりする道具としても、にわかに注目を集めています。

とはいえ、いざ学ぼうとすると、壁が立ちはだかります。

和書はほとんどなく、実務で使う機会も限られ、そもそもどこから手をつければよいのか、道しるべがありません。

「面白そうだが、自分には縁のない世界だろう」と、多くの方が入口の前で引き返してしまいます。

この記事は、その入口に、一本の道を通すことを目的にしています。

高校数学をだいぶ忘れてしまった、Python で機械学習を書いているエンジニアの方
── そうした読者を念頭に、この技術は何の役に立つのか、キャリアにつながるのか、そして何を、どの順で学べばよいのかを、順を追ってお話しします。

予備知識は要りません。
どうぞ、気楽にお付き合いください。

---

TL;DR ── この記事が明らかにすること

この記事は、次の筋道で進みます。

第１に、「プログラムの正しさを数学的に確かめる技術」は、２つの問いによって３つに分かれます。

問いは、「証明したい性質を、自分で書き下す必要があるか」と、「その証明を、機械が自力で見つけられるか」 です。

• 証明したい性質があらかじめ決まっている（配列の範囲外を読まないかどうか証明したい、まずい状態に陥らないかどうかを証明したい）
  ボタン一つで機械が調べてくれます。静的解析やモデル検査がこれです
   
• 性質は自分で書くが、証明は機械が探してくれる ── Dafny や F* がこれです
   
• 性質も証明も、人が書く ── Lean、Rocq、Agda、Isabelle。この記事の主題です

第２に、コストの源は「性質を自分で書き下す必要があるかどうか」にあります。

「配列の範囲外を読まない」なら、ツールに組み込み済みです。しかし「この関数は、数学的に定義された AES 暗号と、どんな入力に対しても厳密に一致する」という性質は、その都度、数学の言葉で書き下すしかありません。

第３に、その書き下しが必要になったのは、「基盤」を作る現場でした。

暗号ライブラリ、OSカーネル、Cコンパイラ、クラウドの認可エンジン。いずれも、その上に無数のソフトウェアが乗る土台です。土台であるがゆえに、「どんな入力が来るか」を限定できません。だから「すべての入力について、仕様どおりである」と証明する必要が生じました。

そして、そのうち証明が深すぎて機械が自力で見つけられなかったもの ── OSカーネル、コンパイラ、認可エンジン ── で、人が証明を組み立てる道具が使われました。 米国と欧州が、この領域に踏み込んできました。

第４に、では日本は、同じ問題を膨大なテストで乗り切ってきたのでしょうか。

そうではない、というのが本記事の見立てです。

日本の高保証産業が強いのは、自動車の電子制御や鉄道の進路制御といった、入力の範囲が物理的に決まっている領域です。

そこで求められる性質は、ツールにあらかじめ組み込まれている種類のものでした。

つまり、性質を自分で書き下さねばならない場面に、そもそも直面する機会が少なかったのです。

「ツールに組み込まれている性質」「自分で書き下す性質」とは、どういうことでしょうか。

具体例で説明します。

ツールにあらかじめ組み込まれている性質とは、こういうものです。

• 配列の範囲外を読み書きしない
• ゼロで割らない
• 数値があふれない
• システムが停止したまま動かなくなる状態に陥らない

これらは、どんなプログラムにも共通して問われることです。

だから検証ツールの側が、あらかじめ「こういう不具合を探せ」という形で持っています。

利用者は、性質を書く必要がありません。
プログラムを読み込ませてボタンを押せば、機械が調べてくれます。

他方で、自分で書き下さねばならない性質とは、こういうものです。

• この関数は、AES 暗号の数学的な定義と、どんな入力に対しても同じ結果を返す
• このコンパイラは、どんなソースコードについても、変換の前後で動作が変わらない
• この認可エンジンは、どんな規則の組み合わせに対しても、定めたとおりの許可・拒否を返す

これらは、プログラム一般に共通する話ではありません。

「AES 暗号とは何か」を数学の言葉で書き表さなければ、そもそも比べる相手がないのです。

だから、利用者が自分で、その性質を記述するところから始めなければなりません。

そして、この「書き下す」作業こそが、証明支援系の学習コストの源です。

性質を記述するには、論理学と型理論の素養が要ります。

日本が強い制御系の現場で問われてきたのは、多くの場合、前者のすでにツールが持っている種類の性質でした。

「センサ値が異常でも制御が破綻しない」
「危険な状態に至らない」

といった問いは、ツールに組み込んでおける形をしています。

後者を必要とする場面に立たなければ、証明支援系を持ち出す理由も生じません。

これが、この節で述べようとしていることです。

第５に、その地図を、いまAIが塗り替えつつあります。

AI の出力が正しいことを機械的に保証すること。

これは、「どんな入力が来るか分からない」新しい基盤層の問題です。
そしてこの領域では、まだどの国も他国より先行しているという立ち位置を確たるものにし得ていません。

第６に、Physical AI と AI エージェントでは、システムの層によって必要な手法が違います。

ロボットや自動運転の知覚・制御そのものを検証するのは、性質があらかじめ決まっている手法です。

「危険領域に入らない」
「入力が少し変わっても出力が破綻しない」

── 型が決まっているからです。

他方で、エージェントに何をさせてよいか、という規則の層では、性質を人が書き下すしかありません。

「この取引は規制に適合するか」
「この融資は与信基準を超えていないか」

は、その都度、書くほかないからです。

この「書き下す」作業こそが、証明支援系の学習で身につく力です。

そのうえで、証明を機械が自動で見つけられる範囲なら機械に任せ、届かなければ人が組み立てる
── 実務では両方が使われています。

そして、この２つをつなぐ「自然言語の規則を、形式的な仕様に翻訳する」層が、いま最大の未解決問題であり、最前線です。

機械学習の素養と証明支援系の素養が、両方必要になる場所です。

「そこも、賢い AI エージェントに任せればよいのでは？」

当然の疑問です。実際、AI に仕様を書かせる研究は進んでいます。

しかし、任せきることはできません。

理由は「AI が嘘をつくから」ではありません。
証明の嘘なら、検証器が弾きます。

問題は別のところにあります。

「その仕様が、人間の本当の意図を表しているか」だけは、機械に確かめようがないのです。
照合すべき相手 ── 意図 ── が、形式の世界に存在しないからです。

しかも、仕様と証明を両方 AI に任せると、証明しやすい弱い仕様を書けば目標を達成できてしまうという誘因が生じます。

実際、自然言語からコードと仕様を生成する研究では、自明な仕様で検証器を満足させてしまう「空虚な検証」への対処が必要だったと報告されています。

もうひとつ。

形式検証の価値は、「たぶん正しい」ではなく「証明されている」と言えることにあります。

仕様の生成を確率的な仕組みに委ねれば、鎖の最初の環が確率的になり、全体が「たぶん正しい」に落ちます。 使う理由そのものが損なわれるのです。

AI が仕様を起草することと、確認する人間を不要にできることは、別の問題です。

この論点は、第５部で改めて詳しく扱います。

第７に、ここに、日本がこれまでとは違う形で参加できる可能性があります。

日本は Physical AI の現場
── ロボット、自動車、工場
── を世界有数の規模で持っています。

検証すべき対象を持っていること自体が、この分野では希少な資産です。

以上を踏まえた実務的な結論は、次のとおりです。

• これらの言語は、決してマイナーではありません。 数学の最前線と、産業の基盤層で、いま現に使われています。
   
• ただし、日本の一般的なWeb開発の現場では、導入のハードルが高いのも事実です。この点は隠さずお伝えします。
   
• 学ぶなら、まず Lean 4 から。 ブラウザで遊べる入門があり、コミュニティが最も活発で、詰まったときに聞ける場所があります。
   
• 今後ニーズが伸びそうな職域は、海外・基盤産業・そして「AI × 証明支援系」 です。とくに最後は、機械学習の素養を持つ方に有利な、生まれたばかりの領域です。
   
• ただし、「AI 時代の到来で需要が急増している」という言い方は、いまの時点では強すぎます。 実務を動かしている量は、まだ自動手法のほうが多い。証明支援系の需要は、立ち上がり始めた段階です。 この見立ての根拠は、記事の中で述べます。
   
• 学び始める目安は、はっきりしています。命題論理・述語論理・自然演繹まで来たら、もう Lean 4 を触ってよい。 論理学を体系的に修めてから、という順序は必要ありません。むしろ、それをやろうとして力尽きる方が多いのです。

想定読者

この記事は、次のような方に向けて書いています。

• 高校数学は、だいぶ忘れてしまった
   
• Python で機械学習の仕事をしている（型ヒントは書くが、型システムを深く学んだことはない）
   
• 論理学、定理証明、形式証明、関数型プログラミング、大学レベルの数学 ── いずれも、まとまって学んだ経験はない
   
• けれど、「証明をコンピュータで検証する」という世界に、なんとなく惹かれている

予備知識は、要りません。 この記事は、そこから始められるように書きます。

この記事を読む価値

「Lean や Coq が気になるけれど、どこから手をつければいいのか分からない」

この記事は、皆様がそのような状態から脱して、卒業するお手伝いをさせていただくのが目的です。

具体的には、次の疑問に順にお答えします。

• これらの言語は、マイナーなのでしょうか？
   
• 実務で使える職場は、どの業界の、どの職種なのでしょうか。
   
• 機械が自動で調べてくれる道具があるのに、なぜ人間が証明を書く必要があるのでしょうか。
   
• 欧米では、その「人間が証明を書かねばならない場面」とは、具体的に何だったのでしょうか。
   
• 日本では、なぜその需要が乏しいのでしょうか。膨大なテストで乗り切ってきたのでしょうか。
   
• 学ぶのに時間とエネルギーがかかりそうですが、キャリアにつながるのでしょうか。
   
• 論理学の学習がどこまで進んだら、定理証明・形式検証を無理なく学ぶ準備が整うのでしょうか。
   
• 数ある定理証明言語・形式証明言語を前にして、どの言語、どの順路で学べばよいのでしょうか。

---

第１部 ── 形式手法という森の地図

本題に入る前に、技術の全体像を一枚の地図としてお見せします。

細部は後で詳しく説明しますので、ここでは「そういう地図なのか」と眺めるだけで十分です。

「プログラムやシステムの正しさを、数学的に確かめる」技術は、まとめて形式手法（formal methods）と呼ばれます。

ただし、この言葉が指す中身は一つではありません。

性格のまったく違う技術が、同じ「形式手法」の名のもとに、いくつも含まれています。

ここを混同すると、学ぶ道を誤ります。

そこで本記事では、学習経路を考えるために、形式手法を便宜上４つの系統に分けます。

これは学術的に確立した分類ではなく、本記事が説明のために設けた区分です。

実際には、これらは重なり合います。

たとえば TLA+ は、モデル検査だけでなく TLAPS という定理証明の機構も持ちます。
Dafny も、内部で複数の技法を組み合わせています。

それでも、「誰が仕様を書き、誰が証明を作るのか」 という軸で分けておくと、学び方を考える上で役立ちます。その目的での区分だとお考えください。

系統	ひとことで言うと	誰が主役か	代表的なツール	この記事との関係
① 対話的証明支援系	人が証明の構造を設計し、機械が検証する	人間（機械は検証役）	Lean、Rocq（旧 Coq）、Agda、Idris、Isabelle	★本記事の主題
② 仕様に基づく自動検証	設計や仕様を、ツールが検査する	機械（人は仕様を書く）	Dafny、F*、TLA+	隣接領域
③ 静的解析・モデル検査	ボタン一つで、機械が自動で調べる	機械	Astrée、Frama-C、SPIN	別カテゴリ
④ ハードウェア検証	回路を、専用ツールで検証する	機械	Verilog/VHDL ＋ EDA ツール	別ジャンル

この地図で**いちばん大切なのは、「人間がどこまで手を出すか」**です。

そして、それは２つの問いで決まります。

問い１：証明したい性質を、自分で書き下す必要があるか。

問い２：その証明を、機械が自力で見つけられるか。

• ③④のタイプは、成立しているかどうかを証明したい性質がツールに組み込まれており、証明も機械が探します。 いわば「ボタンを押すと機械が調べてくれる」手軽さがあります。ただし、確かめられることには限界があります。
   
• ②のタイプは、証明したい性質は人が書きますが、証明は機械が探します。
   
• ①のタイプ（この記事の主題）は、証明したい性質を人が書き、証明の道筋も人が設計します。 訓練が要りますが、そのぶん書き下した仕様に対して、非常に強い保証が得られます。

本記事が扱うのは、①の対話的証明支援系 ── とりわけ Lean・Rocq・Agda・Idris・Isabelle です。

なぜ、手軽な③④だけでは足りず、手間のかかる①がわざわざ必要なのでしょうか？

その理由は、第２部でじっくりと解説します。 この記事の核心にあたる部分です。

まずは、「形式手法にはいくつもの種類があり、この記事はそのうち『人が仕様を書き、証明の道筋も設計する』系統を主題にしている」 とだけ、頭の隅に置いてください。

４つの系統は、どう違うのか？

表に挙げた①〜④は、どれも聞き慣れない言葉だったかもしれません。

ここで、それぞれの内容を簡潔に紹介しておきます。
いまは、全体像をなんとなくつかんでいただければ十分です。

ここで紹介する①〜④は、いずれも、「たくさんのテストケースを自動で作って、片っ端から試す」ものではありません。

テストは、いわば「入力をいくつか試して、たまたま動いたから大丈夫だろう」と確かめる方法 です。

入力が無数にあれば、全部は試せません。

試した入力では動いても、試さなかった入力でバグが潜んでいるかもしれません。

これがテストの限界です。

先ほど表で示した①〜④はどれも、この限界をそれぞれのやり方で乗り越えようとします。

問題なのは、一件ずつ実際に動かして確かめる、というやり方をとる限り、入力が無数にあればどうやってもテストしきれない という困難さです。

これは、原理的な限界です。

では、この限界を越えるには、何をどう変えたらよいのでしょうか？

鍵となるのは、個別の入力に対して実際に実行し、その結果を確認するというやり方を捨てることです。

というのも、この方法を採用している限り、確認できるのは、実際にテストを行うときに実行した有限個の入力に対する結果に限られるからです。

入力が無数にあれば、どこまで実行を重ねても、まだテストを実施できていない、未検証の入力ケースが残ることになります。

限界は、ここから生じているのです。

ならば、実際にテストケースを実行してみることで、実施した入力に対する結果を確認するというやり方以外の方法に、活路を見出すより他ありません。

しかし、どのようにして、「未だ実行していない入力について、正しい結果が得られる」ことを示せるのでしょうか？

表に挙げた４つの系統は、ここで異なるアプローチを選択することになります。

そのアプローチは、大きく３つに分かれます。

• 数学の論理で導くアプローチ

入力を個々に（ひとつひとつ）実行していくのではなく、「すべての場合について成り立つ」ことを数学の論法（帰納法など）によって導くアプローチです。

テストを一度も実行することなく、無限にある入力事例について、起こるであろう結果を証明します。

これが①の証明支援系です。

• 範囲を区切り、その中を網羅するアプローチ

対象を、状態が有限になるようなモデルとして切り出した上で、その範囲の中では、状態を一つ残らず調べるアプローチです。

②や③のモデル検査がこれにあたります。

• 値そのものではなく、値の性質を追うアプローチ

個々の値を一つずつ確認する代わりに、その変数に入る値がどんな性質を持つかを追いかけます。

たとえば、変数 $x$ に $3$ が入る場合、$7$ が入る場合、$11$ が入る場合・・・と一つずつ調べるのではなく、「$x$ に入るのは正の数だけだ」と押さえたうえで、そのまま解析を進めます。

こうすれば、$x$ の取りうる値が何通りあっても、一度の解析で済みます。

ただし、解析ツールが $x$ について把握しているのは「正の数である」という一点だけです。

そのため、$x$ が $0$ にならないことは確実に言えるので「$0$ で割る危険はない」と判定できますが、$x$ が $100$ 未満かどうかまでは判定することはできません。

判断がつかない箇所は、安全のために「危険かもしれない」と警告します。

その結果、本物の危険を見逃すことはありませんが、実際には問題のない箇所まで警告してしまう ことがあります。③の静的解析がこのアプローチを採用します。

なお、厳密な学術用語としては、このように値を性質でまとめて扱う操作を抽象化（abstraction）、その考え方に基づく手法全体を抽象解釈（abstract interpretation）と呼びます。

つまり、「あらゆる場合を、一つずつ選んで確かめる」わけではないのです。

数学的な論法によって導くか、範囲を区切ってその中を網羅するか、値の性質でまとめて安全側に判定するか。

いずれのアプローチにも、「どの入力を調べるか選ぶ」というステップがありません。

ここが、テストとの決定的な違いです。

テストでは、無数にある入力の中から、試すものを選ばなければなりません。時間は有限だからです。

だからこそ、選ばなかった入力が必ず残ります。

一方、３つのアプローチは、いずれも選びません。

数学的な論法はすべての場合をまとめて扱い、
モデル検査は切り出した範囲を一つ残らず尽くし、
静的解析は個々の値を区別せずに計算します。

選び残しが、そもそも生じないのです。

だからこそ、テストでは到達できない範囲まで、正しさを主張できるのです。

次の２つは、どこが違うのでしょうか。

• 範囲を区切って、その中を網羅するか
   
• 値の性質でまとめて、安全側に判定するか

違いは、状態を数え上げるかどうかにあります。

モデル検査（２つ目）は、状態を数え上げます。

対象を有限個の状態として書き表したうえで、その状態を一つ残らずたどります。 「変数 $x$ は $0$ から $100$ まで」と決めれば、その $101$ 通りを、すべて調べ尽くすわけです。網羅的に探索するやり方です。

それに対して、静的解析（３つ目）は、状態を数え上げません。

その代わりに、変数が取りうる値を、あらかじめ決めた有限個の記号に置き換えます。

たとえば、「正」「零」「負」の３つを用意し、$3$ も $7$ も $11$ も、すべて「正」という記号ひとつに割り当てます。

そして、この記号どうしで演算を進めます。

「正 × 正 ＝ 正」「正 ＋ 正 ＝ 正」といった具合です。

$x$ が「正」、$y$ が「正」と分かっていれば、$x \times y$ を実際に計算しなくても、結果が「正」であることが導けます。

$3 \times 7$ なのか $11 \times 5$ なのかを、いちいち確かめる必要はなくなるのです。

こうして、値を記号に置き換えたまま、プログラムの先頭から末尾まで計算を通してしまうのです。

片方は「すべての状態を見る」、もう片方は「記号に置き換えて計算する」。

以上が、２つを分ける決定的な違い です。

以下、４つの系統をひとつひとつ取り上げて読み解いていきます。

（１つ目）対話的証明支援系

人間が、数学の証明を一歩ずつ書いていき、機械がその証明に穴がないかを厳しくチェックする。
そういう道具です。

Lean、Rocq（旧 Coq）、Agda、Idris、Isabelle がこれにあたります。

学校の数学で「証明せよ」という問題を解いたことを思い出してください。
あれを、機械を相手に、機械が絶対に見逃さない厳密さでやる、というイメージです。

テストとの違いは決定的です。

これは、入力を試すのではなく、数学的に証明します。

たとえば、「すべての入力について、この性質が成り立つ」ことを、数学的帰納法などを使って、無限にある場合を一気にまとめて証明するのです。

そのため、証明した性質については、試していない入力でも成り立つことが保証されます。

手間はかかりますが、書き下した仕様に対して、非常に強い保証を得ることができます。

「最強の手法」ではありません。

保証の強さは、何を仕様として書いたか、どの論理体系を使ったか、そしてコンパイラやハードウェアをどこまで信頼するかに依存します。証明支援系が保証するのは、あくまで書かれた仕様に対する正しさです。

強みは「保証の絶対的な強さ」ではなく、「保証したい性質を自由に書き下せること」にあります。 その代わり、仕様と証明を構築するコストが高い ── これがトレードオフです。

ここで、大切な留保をひとつ。

形式証明は、「バグが絶対にないこと」を魔法のように保証するものではありません。

正確には、**「明確に定義された仕様に対して、プログラムがその仕様を満たすこと」**を証明します。

つまり、仕様の書き方そのものが間違っていれば、その誤りごと証明してしまうのです。

「仕様が、人間の本当の意図と一致しているか」を確かめるのは、あくまで人間の仕事として残ります。

（２つ目）仕様に基づく自動検証

人間が「こう動くべき」という仕様を書き、その証明を機械が自力で探す、という道具です。

①との違いは、証明を人が組み立てるかどうかにあります。①では人が証明を書きますが、こちらでは書きません。仕様だけ書けば、あとは機械が探します。

代表的なものが２種類あります。

• Dafny、F*（エフスター）── コードに事前条件・事後条件・不変条件を注釈として書き込むと、内蔵の SMT ソルバという自動証明エンジンが証明を探します。見つかれば、それで終わりです。
   
• TLA+ ── プログラムのコードではなく、**その手前の「設計図」**の正しさを確かめるのに向いています。Amazon が自社の巨大なクラウドサービスの設計チェックに使っています。設計が取りうる状態を機械が漏れなく調べ尽くし、「どんな順序で処理が起きても、まずい状態には決して至らない」ことを確認します。

この系統は、①と③の中間に位置します。 性質は自分で書く（①と同じ）が、証明は機械が探す（③④と同じ）。

この位置づけが、第２部で重要になります。

（３つ目）静的解析・モデル検査

書いたプログラムを、実際に動かさずに機械が自動で調べて、「ここでエラーが起きうる」「危険な箇所はない」と教えてくれる道具です。

Astrée や Frama-C は、航空機などのC言語プログラムを解析するのに使われてきました。

人間は証明を書かず、ボタンを押せば機械が答えを出すのが特徴です。

ここは誤解されやすいところなので、少し丁寧に説明します。

この系統も、テストのように入力をいくつも試すのではありません。やり方は、大きく2通りあります。

• モデル検査（model checking）

検査したいシステムを取りうる状態が有限になるような「モデル」として書き表した上で、そのモデルが取りうる状態を機械が体系的に調べ尽くす手法です。

テストが「入力を標本として試す」のに対し、モデル検査はそのモデルの範囲では、漏れなく調べる点が違います。

 

• 静的解析（とくに抽象解釈という手法）

個々の値を一つずつ調べる代わりに、「この変数は正の数だ」といった具合に、値の性質でまとめて解析します。

この方式は、安全側に倒すよう作られています。

つまり、本当に危険な箇所を見逃すことはない代わりに、「危ないかもしれない」と実際には問題ない箇所まで警告してしまう（誤警報が出る）ことがあります。

「見逃しゼロ、ただし空振りあり」 と考えてください。

「結局、全パターンをチェックするのか、しないのか？」

この質問に対する答えは、「作ったモデルの範囲では、全パターンを調べる。ただし、そのモデルは現実のシステムを簡略化したものである」

これが回答です。

どういうことでしょうか。

たとえば、「変数 $x$ は 0〜100 の整数」と決めてモデルを作れば、その101通りは一つ残らず調べます。

しかし現実のプログラムでは、$x$ が 64 ビット整数かもしれない。

そこまで含めると状態数が天文学的になり、調べ尽くせません（これを状態爆発と呼びます）。

そこで、検査できる大きさにモデルを簡略化してから、その範囲で全パターンを調べるのです。

実務では、この状態爆発を避けるために、状態を賢くまとめて扱う手法（シンボリックモデル検査）や、探索する範囲をあらかじめ区切る手法（有界モデル検査）など、さまざまな工夫が使われます。

結論として、「テストのように一部を試すだけ」ではないが、「現実のシステムのあらゆる可能性を完全に調べ尽くす」わけでもない。

「切り出したモデルの中では全数、ただしモデルの外は保証しない」

ここが、モデル検査の実像であり、限界でもあります。

モデル検査と静的解析は、「実行した入力に限って正しさを確認できる」テストとは異なり、「あらかじめ定めた範囲について、網羅的に正しさを保証する」 ことを目指します。

ただし、込み入った数学的な性質を自動で確かめることには限界があります。

その領域は①の証明支援系が担います。

（４つ目）ハードウェア検証

これだけ毛色が違います。

ソフトウェアではなく、半導体チップの回路が正しく設計されているかを検証する分野です。

Verilog や VHDL というのは、回路を設計するための専用言語（プログラミング言語がソフトを書くための言語であるように、これらは**「回路を書く」ための言語** です）。

その回路検証にも、③と同じく体系的に調べ尽くす手法（モデル検査や、２つの回路が同じ動作をするか確かめる等価性検査）が使われます。

扱う対象も道具も、ソフトの世界とはまったく別です。

EDA とは： Electronic Design Automation（電子設計自動化）の略で、半導体チップや電子回路を設計・検証するための専用ソフトウェア群を指します。Synopsys、Cadence、Siemens（旧 Mentor）などが主要なベンダーで、JasperGold、VC Formal、Questa といった検証ツールがこの分野の標準です。

回路は状態の数が本質的に有限なので、こうした網羅的なチェックがソフトウェアに比べてうまく働く分野といえます。

この違いを知らずに「日本にも形式検証の求人はある」と早合点すると、その多くがハードウェア検証（EDA）で、Lean や Rocq を書く仕事ではなかった、ということになりかねません。求人を見るときは、どちらの系統の話なのかを、必ず見極めてください。

ここまで見てきた４つに共通するのは、「実行した入力に限って正しさを確認するテスト」ではなく、「あらゆる場合について正しさを保証する」ことを目指す点です。

そのうえで、人間がどこまで手を出すかが、三段階に分かれます。

③と④では、人間はほとんど手を出しません。 検証したい性質はツールにあらかじめ組み込まれており、ボタンを押せば機械が調べます。

②では、人間が「何を保証したいか」を書きます。 ただし、その証明は機械が探します。

①では、人間が「何を保証したいか」を書き、さらにその証明も組み立てます。 機械は、その証明に穴がないかを検算する係にまわります。

この三段階の違いが、どこから生じるのか ── それが、第２部の主題です。

手軽さで選ぶなら、③④。

自分で仕様を書く必要はあるが、証明は任せたいなら、②。

証明まで自分で組み立てる覚悟があるなら、①。

このように、目的に応じて、どの手法を選ぶべきかが分かれてきます。

この記事が主題とするのは、最も手間がかかるが、その代わり、成立しているかどうかを証明したい性質を、最も自由に書き下すことができる①の対話的証明支援系です。

---

第２部 ── 機械で足りる場面と、人が仕様を書くしかない場面

ここからが、この記事の核心です。

機械が自動で調べてくれる道具があるのに、なぜわざわざ人間が証明を書くのか。

この問いに、正面から答えます。

分かれ目は「有限か無限か」ではありません

まず、よくある誤解を解いておきます。

「機械が自動で調べる手法は有限の対象しか扱えず、無限を扱うには人間の証明が要る」

── そう説明されることがあります。これは、半分は正しく、半分は不正確です。

確かに、古典的なモデル検査は、有限の状態を前提とします。無限の状態を持つ対象は、有限のモデルに切り出さなければ扱えません（無限状態を扱う拡張も研究されていますが、抽象化を伴います）。

しかし、静的解析（抽象解釈）は、入力が無限にあっても動きます。 先ほど見たとおり、値を「正」「零」「負」のような有限個の記号に置き換えてしまうからです。この方式なら、$x$ が 64 ビット整数であろうと、扱う記号の数は変わりません。

実際、Astrée は、入力を一つずつ試すことなく、C言語プログラムに実行時エラーが起きないことを示します。値の取りうる範囲が膨大であっても、記号に置き換えて解析するためです。

では、本当の分かれ目はどこにあるのでしょうか。

本当の分かれ目は、２つの問いにあります

答えを述べます。分かれ目は、次の２つの問いです。

問い１：証明したい性質を、自分で書き下す必要があるか。

問い２：その証明を、機械が自力で見つけられるか。

この２つで、道具が３つのタイプに分かれます。

③④のタイプ ── 証明したい性質が、ツールの側で決まっている場合

次のような問いは、「これを調べよ」という形で、ツールの側にあらかじめ組み込まれています。

• 配列の範囲外を読まないかどうか
• ゼロで割らないかどうか
• 数値があふれないかどうか
• まずい状態（デッドロックなど）に陥らないかどうか

利用者は、性質を書き下す必要がありません。ボタン一つで調べられます。

第１部の表の ③（Astrée、Frama-C、SPIN）と④（ハードウェア検証） が、ここに属します。

②のタイプ ── 証明したい性質は自分で書くが、証明は機械が探す場合

しかし、次のような問いは、あらかじめ組み込んでおけません。

• この関数の出力は、数学的に定義された AES 暗号と、どんな入力に対しても厳密に一致するかどうか
• このコンパイラは、あらゆるソースプログラムについて、変換後も元の動作を保つかどうか

性質そのものを、その都度、数学の言葉で書き下す必要があります。

ただし、書き下したあと、その証明を機械が自力で見つけてくれる場合があります。

Dafny や F* がこのタイプの道具です。

利用者は事前条件・事後条件・不変条件を注釈としてコードに書き込み、内蔵の SMT ソルバが証明を探します。見つかれば、それで終わりです。

第１部の表の②が、ここに属します。

学術的には、この方式を auto-active verification（自動能動検証）と呼びます。「人が注釈を書き、機械が証明を探す」という、①と③④の中間に位置する方式です。

①のタイプ ── 証明したい性質も、証明も、人が書く場合

しかし、SMT ソルバが自力で証明を見つけられないことがあります。

たとえば「すべての自然数について成り立つ」という主張は、数学的帰納法という論法を必要とします。
「どんなシステムコールの並びに対しても」という主張も同様です。

こうした数学的な論法をどこで使うかは、SMTソルバは自力で判断することができません。

そのとき、人間が証明の道筋を設計するしかありません。

なお、「人が全部を手で書く」わけではありません。

Lean には simp、omega、linarith、ring といった、証明の細部を自動で片づける仕組み（タクティクと呼びます）があり、Rocq や Isabelle にも同様の自動化があります。Isabelle の Sledgehammer は、外部の自動証明器を呼び出して証明を探してくれます。

人間が担うのは、証明全体の構造 ── どこで場合分けし、どこで帰納法を使うか ── を決めることです。細部は自動化に任せます。

Lean、Rocq、Isabelle、Agda ── 第１部の表の①が、このタイプです。

３つのタイプを、表にまとめます

タイプ	性質を書くのは	証明を作るのは	代表的な道具
③④	ツールにあらかじめ組み込み済み	機械	Astrée、Frama-C、SPIN、EDA ツール
②	人が自由に書く	機械（SMT）が探す	Dafny、F*
①	人が自由に書く	人が組み立てる（機械は検算）	Lean、Rocq、Isabelle、Agda

	③④	②	①
学習コスト	比較的低い	中程度	高い（論理学と型理論の素養が要る）
時間コスト	短い	中程度	長い（大規模なものでは人年単位）
書ける性質の自由度	低い	高い	高い

②と①を分けるのは、性質の自由度ではありません。 どちらも自由に書けます。分かれ目は、証明を機械が自力で見つけられるかどうかです。

そして、**③④と②・①を分けるのが、「性質を自分で書き下す必要があるか」**です。

では、「性質を自分で書き下す必要がある」場面とは、具体的に何か

ここが、多くの解説で曖昧にされる部分です。具体的に、四つ挙げます。

いずれも、実際に人年単位の投資が払われた、現実の事例です。②のタイプで足りたものと、①のタイプが必要だったものが混在します。その違いにも注目してご覧ください。

１. 暗号ライブラリ ── HACL*／EverCrypt

HACL*／EverCrypt は、F*（エフスター）という言語で検証された暗号ライブラリです。F* は、先ほどの②のタイプにあたります ── 人が仕様を注釈として書き、SMT ソルバが証明を探す方式です。

Curve25519、AES-GCM、SHA-2 といった標準的な暗号アルゴリズムを実装し、TLS 1.3 の必須暗号スイートを提供、Mozilla の NSS 暗号ライブラリにも組み込まれました。

ここで証明されているのは、次のような性質です。

• どんな長さの入力に対しても、配列の範囲外を読まない、ゼロ除算をしない
   
• どんな入力に対しても、計算結果が、数学的に定義された関数と厳密に一致する
   
• どんな秘密鍵に対しても、実行される命令の並びとメモリアクセスの位置が、鍵の中身によって変化しない（定時間暗号。これが崩れると、処理時間の差から鍵が推測されます）

一つ目は、静的解析でも扱えます。

しかし、二つ目と三つ目は違います。

「計算結果が、数学的に定義された関数と厳密に一致する」── これは、AES という暗号の数学的定義そのものを書き下し、実装がそれと一致することを示す作業です。「こういうバグを探せ」という話ではありません。

「鍵の中身によって実行の仕方が変わらない」も同様です。プログラムの実行そのものについての性質であり、あらかじめツールに組み込んでおける類のものではありません。

だから、性質を自分で書き下す必要がありました。 そしてこの事例では、書き下した性質の証明を、SMT ソルバがおおむね自動で見つけられた ── ②のタイプで足りた、ということになります。

２. OSカーネル ── seL4

検証済みマイクロカーネル seL4 が証明したのは、「どんなシステムコールの並びが、どんな順序で、何回呼ばれても、カーネルが仕様どおりに振る舞う」ことです。

これは「まずい状態に陥らない」より、はるかに強い主張です。「仕様どおりに振る舞う」という仕様そのものを、数学の言葉で書き下したうえで、実装がそれを満たすことを証明しています。

この検証に使われたのは Isabelle/HOL、つまり①のタイプです。人が証明の構造を設計しました。 費やされたのは、22人年です。

３. Cコンパイラ ── CompCert

CompCert は、「あらゆるソースプログラムについて、コンパイル後のコードが元の動作を保つ」ことを Rocq（旧 Coq）で証明した C コンパイラです。

これが画期的だった理由を説明します。

コンパイラには、コードを速く小さくする最適化という機能があります。ところが最適化の処理は複雑で、そこにバグが潜むと、書いたとおりに動かないプログラムが出来上がってしまいます。

そのため航空分野では、安全審査を通すために、あえて最適化をほとんど無効にするという運用が取られてきました。コンパイラを信用しきれないので、余計なことをさせない、というわけです。当然、出来上がるプログラムは遅く、大きくなります。

CompCert は、「最適化しても動作が変わらない」ことを証明しました。証明があるからこそ、最適化を有効にしたまま安全審査を通せる ── これが、この製品の価値です。商用製品として販売され、航空分野で実際に使われています。

こちらも Rocq（旧 Coq）、つまり①のタイプです。6人年と10万行の証明コードが費やされました。

４. クラウドの認可エンジン ── AWS Cedar

AWS の認可言語 Cedar は、Lean で検証されています。

証明されているのは、「どんなポリシーの組み合わせに対しても、どんなアクセス要求が来ても、許可・拒否の判定が仕様どおりになる」ことです。

ポリシーも要求も、無限に書けます。そして「仕様どおり」の中身は、認可という業務の意味そのものを書き下したものです。

こちらも Lean、つまり①のタイプです。

この４つに共通する構図

お気づきでしょうか。４つとも、その上に他のソフトウェアが積み重なる土台（基盤）となる部分です。

• 暗号ライブラリの上に、あらゆる通信が乗る
• OSカーネルの上に、あらゆるアプリが乗る
• コンパイラを通して、あらゆるコードが機械語になる
• 認可エンジンを、あらゆるアクセスが通過する

基盤であるがゆえに、「どんな入力が来るか」を、あらかじめ限定できません。

使う側が何を渡してくるか、作る側には分からない。だから「すべての入力について、仕様どおりである」と言うほかないのです。

そして、その「仕様」の中身が、暗号の数学的定義であったり、プログラムの意味の保存であったりする。 これは、ツールにあらかじめ組み込んでおける性質ではありません。

ここに、人間が性質を書き下すしかない理由があります。

そのうえで、４つの内訳を見てください。

事例	使われた道具	タイプ
HACL*／EverCrypt（暗号ライブラリ）	F*	②（人が仕様を書き、SMT が証明を探す）
seL4（OSカーネル）	Isabelle/HOL	①（人が証明を組み立てる）
CompCert（Cコンパイラ）	Rocq（旧 Coq）	①
Cedar（認可エンジン）	Lean	①

四つとも「性質を自分で書き下す必要がある」点では共通しています。
しかし、そのあとが分かれました。

暗号ライブラリでは、SMT ソルバが証明をおおむね自動で見つけられました。
暗号アルゴリズムの計算は、機械的な演算の積み重ねであり、SMT が得意とする形に落としやすかったからです。

一方、OSカーネル、コンパイラ、認可エンジンでは、それが届きませんでした。

「どんなシステムコールの並びでも」
「あらゆるソースプログラムについて」

といった主張は、数学的帰納法をはじめとする込み入った論法を必要とします。
その論法をどこでどう使うかは、人間が設計するしかなかったのです。

ここが、②と①を分ける実際の境目です。 道具の優劣ではなく、証明の深さが決めています。

さらに、一度証明すれば、その上に乗る無数のソフトウェアが恩恵を受けます。
22人年、6人年という莫大な投資が正当化される理由は、ここにあります。

---

第３部 ── では、日本はどうだったのか

ここで、日本の読者にとって最も切実な問いに進みます。

日本の高保証産業も、同じ問題に直面してきたはずです。それを、膨大なテストで乗り切ってきたのでしょうか。

公開情報から見るかぎり、答えは「そうではない」と考えられます。

より正確に言えば、日本の高保証産業が主に扱ってきた領域では、そもそも「性質を自分で書き下す必要がある場面」が前面に出てこなかったのです。

理由を、順に見ていきます。

理由１ ── 日本が強いのは、性質があらかじめ決まっている領域

自動車の電子制御、ロケットの姿勢制御、鉄道の進路制御、プラントの運転制御。

これらで求められる性質は、多くの場合、次のようなものです。

• センサ値が異常でも、制御が破綻しないかどうか
• どんな順序でイベントが起きても、危険な状態に至らないかどうか
• 実行時エラーで停止しないかどうか

いずれも、「あらかじめ決まった種類の性質」です。 ツールに「こういうものを探せ」と組み込んでおける類のものです。

しかも、入ってくる値の範囲が、物理的にあらかじめ決まっています。 センサが返す温度には上限と下限があり、速度にも、舵角にも、圧力にも、現実的な範囲があります。

つまり、モデル検査や静的解析が、有効に働く領域なのです。

実際、日本でもこの系統の適用事例があります。

ある形式手法の応用事例集には、JAXA の人工衛星の姿勢制御ソフトウェア、自動車 ECU のソフトウェア開発、鉄道の列車進路制御システムなどへの、モデル検査の適用例が挙げられています。

列車進路制御を SPIN（モデル検査ツール）で検証する研究も、学会で発表されています。

ツールにあらかじめ組み込まれた性質で足りるなら、自分で性質を書き下す必要は生じません。
ましてや、その証明を人が組み立てる必要もありません。

理由２ ── 基盤層を作る産業構造が、欧米とは異なっていた

ここが核心です。

先ほど挙げた四つ ── 暗号ライブラリ、OSカーネル、Cコンパイラ、認可エンジン ── を思い出してください。

日本の産業では、これらを海外から調達して使う場面が多くありました。

• OS は Linux、Windows、あるいは海外製の組込みOS
   
• コンパイラは GCC、LLVM、あるいは海外製の商用コンパイラ
   
• 暗号ライブラリは OpenSSL、あるいは海外製の実装
   
• クラウド基盤は AWS、Azure、Google Cloud

これらを「作る側」に立たなければ、「どんな入力が来るか分からない」という問題に直面しません。

与えられた基盤の上で、範囲の決まった制御系を作る ── そこに証明支援系の出番は、生じにくいのです。

ただし ── 日本にも、基盤にあたる技術はあります

ここは、公平に書いておかねばなりません。

日本が基盤層をまったく作ってこなかった、というのは誤りです。

組込みOS の ITRON は、1984年に坂村健氏が提唱した TRON プロジェクトから生まれた、日本発のリアルタイムOS仕様です。

家電、自動車、産業機器、医療機器など、日本の組込み産業を中心に広く使われてきました。
まぎれもなく、基盤にあたる技術です。

暗号アルゴリズムの Camellia は、NTT と三菱電機が2000年に共同開発した共通鍵ブロック暗号です。

欧州の暗号選定プロジェクト NESSIE で「米国標準の AES と多くの点で同等の安全性と性能を有する」と評価され、日本国産暗号として初めてインターネット標準暗号（IETF RFC）に承認され、OpenSSL、Firefox、Linux、FreeBSD にも搭載されています。

では、なぜこれらは形式検証されなかったのでしょうか。

いくつかの事情が考えられます。

第１に、時期の問題です。 ITRON が生まれた1984年、Camellia が開発された2000年の時点で、この規模の形式検証は、まだ実用の域に達していませんでした。

seL4 の検証が完了したのは2009年、CompCert も同時期です。暗号ライブラリ HACL* の論文が出たのは2017年です。当時、この選択肢は事実上存在しませんでした。

第２に、調達側の要求がなかったことです。

後述するとおり、米国では国防総省や NSA が調達の条件として高い保証水準を求めます。
日本の組込み機器市場には、そうした要求はありませんでした。

第３に、Camellia については、能力の所在を正確に見る必要があります。

日本に、暗号アルゴリズムを設計する能力がなかったのではありません。
むしろ Camellia は、国際標準に採用されるだけの水準にあります。

問題は別のところにあります。

「アルゴリズムを設計すること」と、「その実装を形式的に検証し、広く再利用される基盤ライブラリとして提供すること」は、別の能力だという点です。

HACL* のような検証済み暗号ライブラリを構築したのは、フランスの INRIA、Microsoft Research、カーネギーメロン大学の共同プロジェクトでした。

設計と、検証済み実装の提供とが、別の場所で行われた ── この分業の形が、需要の所在をそのまま映しています。

まとめると

日本で証明支援系の需要が乏しかったのは、技術力の問題でも、テストへの過信でもありません。

• 日本が強い制御系の領域では、求められる性質が「決まった種類」であり、機械が自動で調べられた
   
• 性質を自由に書き下す必要がある基盤層を、自国で作る機会が相対的に少なかった
   
• 数少ない基盤層の産物（ITRON、Camellia）は、この規模の形式検証が実用化する前に生まれ、調達側の要求もなかった

膨大なテストで乗り切ったのではなく、そもそも「性質を自分で書き下す必要がある場面」に直面する機会が、構造的に少なかった ── これが、公開情報から読み取れる説明のひとつです。

ただし、これは仮説です。

ここで述べたのは、単一の原因ではありません。 産業構造、調達制度、研究開発の歴史、教育のあり方 ── これらが複合した結果だと考えられます。

本記事は、そのうち産業構造の面に光を当てました。他の要因の重みについては、異なる見方もありうるとお考えください。

裏を返せば、日本が基盤層を自国で作ろうとするなら、あるいは AI の検証という新しい基盤層に踏み込むなら、そこで初めて証明支援系が必要になります。

そして ── これが本記事の後半の主題ですが ── AI の出力を検証するという領域は、まさに「どんな入力が来るか分からない」新しい基盤層です。 そこでは、まだどの国も先行を確定させていません。

第４部 ── これらの言語は、マイナーなのか

結論から申し上げます。

これらの言語は、決してマイナーではありません。

ただし、その理由は「求人が多いから」というものではありません。

確かに、証明支援系そのものを日々書く求人の数は多くありません。

しかし、これらの言語は、他では代えのきかない場所で使われているのです。

数学研究の最前線

2026年7月、ZEN大（神奈川県逗子市のオンライン大学）などの国際共同研究チームは、望月新一氏の ABC 予想証明について中間報告を公表し、証明支援ソフト Lean を用いた検証を継続していると発表しました。（判断は保留中です）

ABC予想 は、その正否をめぐって世界の数学者の意見が20年近く割れてきた難問です。

その検証の現場に、Lean が投入されているのです。

参照：ZEN大などによる ABC 予想の Lean 検証（共同通信、2026年7月）
https://news.jp/i/1450775181778223921

産業の基盤層

Lean は2025年、プログラミング言語ソフトウェアとして最も権威ある賞のひとつ、ACM SIGPLAN Programming Languages Software Award を受賞しました。

受賞理由には、AWS の認可言語 Cedar の検証、差分プライバシー実装の検証、そして StarkWare や Nethermind といった企業でのブロックチェーン検証が挙げられています。

「趣味の言語」どころか、クラウドの認可基盤や、最難関の数学の検証を支えている。

これが実像です。

実務で使われている業界

定理証明言語や形式検証が使われている業界は、はっきりしています。

バグが人命や巨額の損失に直結する領域です。

• 航空宇宙 ── Airbus は、飛行制御ソフトの検証に静的解析ツール（Astrée、Frama-C など）を使い、A380 の開発でも用いてきました。
   
• 半導体・ハードウェア ── 回路設計の検証（Verilog/VHDL・RTL）は、専門職として確立しています。求人も比較的多く、待遇も良い分野です。ただし前述のとおり、これは証明支援系とは別系統です。
   
• 暗号・ブロックチェーン ── スマートコントラクト検証、暗号ライブラリの検証など。誤りが即座に金銭的損失になるため、形式的な保証の価値が高い領域です。
   
• クラウド基盤 ── AWS は、分散システムの設計検証に TLA+ を長年使ってきました。S3、DynamoDB、EC2 といった中核サービスの設計で、深刻なバグを未然に防いだ実績が公表されています。

職種としては、「Formal Verification Engineer」「Formal Methods Engineer」といった名前で募集されることが多く、その多くは英語圏・EU に集中しています。

---

第５部 ── キャリアにつながるのか

日本の一般的なWeb・アプリ開発の現場に限れば、これらの言語が直接キャリアに結びつく機会は、多くありません。

しかし、視野を広げれば話は変わります。

バグが人命や、巨額の経済的損失に直結する ── そうしたミッション・クリティカルな分野では、形式証明・定理証明の言語が、現に使われています。

ミッション・クリティカル（mission-critical）とは、その働きが停止したり誤動作したりすると、人命が失われるリスクが高まったり、重大事故や甚大な経済損失など、取り返しのつかない結果を招く可能性が高いシステムを指す言葉です。

なぜ、一般的な開発では広まりにくいのでしょうか？

この論点については、すでに Qiita に優れた記事があります。

autotaker 氏の「形式手法はなぜ流行っていないのか」（323いいね・230ストック）です。

アジャイル開発や CI/CD、開発者体験（DX）の観点から、実務導入の難しさを的確に論じています。あわせてお読みになることを、強くおすすめします。

同氏の結論のひとつは、示唆に富んでいます。

「実用化した形式手法には、別の名前がつく ── それが型システムだ」（TypeScript や Rust の型がその例です）。

ところで、autotaker氏の記事と本記事は、光を当てている場所が異なります。

同氏の記事は、一般的なWeb・アプリ開発の職場を主な舞台に、「なぜそこでは流行らないのか」を論じています。

他方で、本記事が光を当てるのは、基盤層とミッション・クリティカルな分野で、これらの言語が現に求められているというニーズです。

両者は決して矛盾しません。「一般開発では広まりにくい」ことと、「基盤層では必要とされている」ことは両立するからです。

Python の型ヒントから、証明支援系へ

同氏の「実用化した形式手法は型システムになる」という指摘は、読者の皆様にとって、心強い足がかりになります。

皆様が Python で日々書いている型ヒントは、形式手法の最も普及した形なのです。

その延長線上に、証明支援系があります。

定理証明言語への道のりは、縁もゆかりもない無縁の世界へ飛び込むことではありません。すでに触れている Python の「型」の考え方を、より深く推し進めた先に、証明支援系がある。

両者は地続き なのです。

ひとつ、想像してみてください。

深層学習の学習パイプラインを回し、数時間待ったあげく、テンソルの次元（shape）の不一致でプログラムが落ちた ── そんな経験はないでしょうか。

行列の形が合わないという、たったそれだけの理由で、GPU 時間と待ち時間が無駄になる。

もしその不一致を、コードを実行する前に、型の段階で数学的に検出できたとしたら。

証明支援系が持っている力は、まさにそういう性質のものです（この記事の後半で、Agda を使って「そもそも書けなくする」実例をご覧に入れます）。

伸び筋は、３つの方向にあります

1. 海外 ── 求人の絶対数が、日本国内とは桁違いです。
    
2. 基盤産業 ── 航空宇宙、半導体、暗号、ブロックチェーン、OSカーネル。
    
3. AI × 証明支援系 ── これが、いま最も熱い方向です。

３つ目について、少し詳しくお話しします。

機械学習と証明支援系の交差点で、新しい職域が生まれつつあります。

DeepMind の AlphaProof は、Lean を証明環境として使う強化学習エージェントです。

自然言語で「もっともらしい誤り」を出しがちな AI の正しさを、Lean で検証することで機械的に保証する。

この発想が、AI 研究の一つの主題として浮かび上がりつつあります。

Harmonic、Mistral（Lean 向けモデル Leanstral）、DeepSeek-Prover など、主要な AI 企業が Lean を形式的な裏付けとして採用し始めています。

Python で機械学習をしてきた読者の皆様にとって、これは最良の接続点です。

「機械学習の素養＋証明支援系」という組み合わせは、いま新しく価値が生まれている領域だからです。

「LLM が賢いなら、機械が全部やればいいのでは？」

ここまで読んで、こう思われた読者の方も、おられるかもしれません。

**「これほど賢い LLM が普及したいま、その LLM に証明を書かせれば、人間がやらなくてもよいのではないか」**と。

とても自然な疑問です。そして、この答えこそが、なぜ LLM 時代にこそ証明支援系の価値が高まっているのかを理解する鍵になります。

答えは、こうです。LLM は「もっともらしい嘘」をつくからです。

LLM は、流暢で説得力のある文章を生成しますが、その内容が正しいという保証はありません。事実でないことを、さも事実であるかのように出力する ── いわゆる「幻覚（ハルシネーション）」です。プログラムのコードでも、数学の証明でも、これは起こります。

では、その誤りを、どうやって捕まえるのか。ここで、証明支援系が決定的な役割を果たします。

証明支援系の中核には、証明が正しいかどうかを機械的に判定する「検証器（チェッカー）」 があります。
この検証器は、それ自体が小さく、厳密に作られたプログラムで、誤った証明を、絶対に通しません。

つまり、構図はこうなります。

• LLM（賢いが、嘘をつく） が、証明やコードの候補を高速で生成する
• 証明支援系の検証器（融通は利かないが、絶対に誤らない） が、それを厳格に検算する
• 検証器が通した証明だけが、数学的に正しいと保証される

この２つは、弱点を補い合う関係にあります。

実際、AI 研究の最前線は、まさにこの方向に動いています。DeepMind の AlphaProof、Harmonic の Aristotle（2025年の国際数学オリンピックで金メダル級の成績を、証明つきで達成）、DeepSeek-Prover
── いずれも、「LLM が生成し、Lean が検証する」 という組み合わせです。

ある研究者は、この状況を的確に言い表しています。

AI が幻覚でたわごとを出しても構わない。証明チェッカーが無効な証明をすべて拒否し、AI に何度でもやり直させるからだ。そして、その証明チェッカー自体が検証済みの小さなコードなので、無効な証明をこっそり通すことは、事実上不可能である。
と。
（分散システム研究者 Martin Kleppmann のブログより：https://martin.kleppmann.com/2025/12/08/ai-formal-verification.html ）

**人が一から証明を書く負担は、LLM が肩代わりしつつある。

しかし、最後に正しさを保証する検証器の役割は、むしろ重みを増している**

これが、いまこの分野を学ぶ価値の核心のひとつです。

では、仕様そのものも AI に書かせればよいのでは？

ここで、当然の疑問が浮かびます。

第２部で見たとおり、①と②のタイプでは、人間が「証明したい性質」を書き下す必要がありました。これが、学習コストと人手のコストの源です。

しかし、これほど賢い AI エージェントがいるのなら、その「性質を書き下す」作業も、代行させればよいのではないでしょうか。

もっともな問いです。そして実際、その研究は進んでいます。仕様を生成する側と、実装と証明を生成する側を分けて自己対戦させる手法や、自然言語の問題文から Dafny の仕様とコードを生成する研究が、すでに現れています。

では、人間は不要になるのでしょうか。

答えは「ならない」と考えられます。ただし、その理由は、多くの人が思うところとは違います。

まず、退けておくべき答え ── 「AI は嘘をつくから」

「AI はハルシネーションを起こすから、任せられない」

これは、一見もっともらしく聞こえますが、この文脈では、答えになっていません。

なぜなら、証明におけるハルシネーションは、まさに検証器が解決する問題だからです。

AI がどれほど嘘の証明を書こうと、Lean の検証器が弾きます。何度でもやり直させればよい。「AI が嘘をつく」ことは、証明支援系を使う理由ではあっても、人間が必要な理由にはなりません。

問題は、まったく別の場所にあります。

本当の理由 ── 「仕様が正しいか」は、形式的な問いではないから

証明支援系が保証するのは、次のことです。

この証明は、この仕様を満たすことを、正しく示している

保証しないのは、次のことです。

この仕様は、人間が本当に望んでいることを、表している

この２つは、質の違う問いです。

前者は、形式的な対象どうしの関係です。仕様も証明も数学の言葉で書かれており、機械が突き合わせられます。

しかし後者は、そうではありません。

比較すべき相手 ── 「人間が本当に望んでいること」 ── が、形式的な対象として存在しないからです。

意図は、人の頭の中と、社会の文脈の中にあります。

照合すべき原本が、形式の世界に存在しない。 だから、機械が突き合わせようがないのです。

ソフトウェア工学では、この２つを古くから区別してきました。

• 検証（verification）── 作ったものが、仕様どおりか。形式化できる
• 妥当性確認（validation）── その仕様が、そもそも正しいか。形式化できない

証明支援系が扱うのは、前者だけです。
これは技術の未熟さではなく、構造的な事実です。

どれほど AI が賢くなっても、この壁が動くことはありません。

具体的に、何が起きるのか ── ３つの失敗の形

抽象論だけでは足りないので、実際に報告されている失敗の形を挙げます。

第１に、空虚な仕様（vacuous specification）です。

仕様の生成と証明の生成を両方ともAIに任せると、構造的な誘因が生じます。
「証明が通ること」が目標なら、証明しやすい弱い仕様を書けば、目標は達成できてしまうのです。

たとえば「この関数は何かを返す」という仕様は、たいてい真であり、簡単に証明できます。そして何の役にも立ちません。

これは、机上の懸念ではありません。

自然言語から Dafny のコードと仕様を生成する研究では、「モデルが自明な仕様で検証器を満足させてしまう空虚な検証（vacuous verification）に対処するため」、機能的な妥当性を別途確認する仕組みを組み込んだ、と報告されています。

金融エージェントの Lean 4 による検証を扱った研究でも、「同語反復的な仕様を構造的に排除する情報障壁」 を設計に組み込んだ、とされています。

わざわざそう設計しなければならなかったという事実が、この問題の実在を示しています。

これは、強化学習で古くから知られる仕様ゲーミング（specification gaming）と同じ構図です。

目標を文字どおり満たしながら、その意図を満たさない
── 検証器を相手にしても、同じことが起こります。

第２に、前提（assumption）の設定です。

どんな証明にも、証明していない前提があります。

seL4 の検証も、ハードウェアの振る舞い、メモリ配置、証明に用いた定理そのもの
── そうした明示的・暗黙的な前提の上に成り立っています。

OSカーネルの仕様生成を LLM に行わせる研究でも、この前提の多さが困難の中心として挙げられています。

「何を前提として置き、何を証明するか」の線引きは、現実世界についての判断です。

どのハードウェア故障を考慮に入れるか。どの攻撃者モデルを想定するか。
これらは、形式の内側からは決められません。

第３に、保証の鎖は、最も弱い環で決まることです。

これが、最も重要な点かもしれません。

形式検証の価値は、「たぶん正しい」ではなく「証明されている」と言えることにあります。
確率的でないこと、それ自体が価値なのです。

ところが、仕様の生成を確率的な仕組みに委ねると、鎖の最初の環が確率的になります。

ここでいう「確率的」とは、何を指しているのでしょうか。

LLM は、次に来る語を確率で選びながら文章を生成する仕組みです。

同じ問いを与えても、出力が毎回まったく同じとは限りません。設定によって振る舞いを揃えることはできますが、「この入力なら必ずこの出力になる」という保証は、原理的に与えられていません。

ですから、LLM が書いた仕様について言えるのは、「意図をよく捉えているだろう」という見込みまでです。「必ず捉えている」とは言えません。

一方、Lean の検証器は違います。

同じ証明を与えれば、必ず同じ判定を返します。
通るか、通らないか。それだけです。

曖昧さも、揺らぎもありません。

この２つを直列につなぐと、何が起こるか。 ここが問題の核心です。

$「仕様はたぶん意図を捉えている（確率的）」 → 「実装は仕様を満たす（証明済み）」$

この鎖全体の強さは、最初の環で決まります。

後半をどれほど厳密にしても、全体としては「たぶん正しい」に落ちてしまうのです。

形式検証を使う理由そのものが、ここで損なわれます。

人間が引き受けるべき役割とは？

ここまでの議論から、人間に残る役割 が浮かび上がってきます。

第１に、何を保証すべきかを決めること。
数ある性質のうち、どれが本当に重要なのか。

これは、その領域の実務と責任を知る者にしか決められません。

第２に、書かれた仕様が意図と合っているかを確かめること。
AI が仕様を起草してもかまいません。
しかし、それを読んで「これでよい」と判断する者が要ります。

第３に、前提の線引きを引くこと。
何を信頼し、何を証明の対象とするか。

第４に、責任を引き受けること。
証明書は責任を負いません。規制当局が求めるのは、署名する人間です。

要するに、人間が担うべき役割は、何かを「証明する」ことではなく、「何を証明すべきかを決め、それでよいと引き受ける」ことです。

そして皮肉なことに、この役割を果たすには、証明支援系が何を保証し、何を保証しないのかを、正確に理解している必要があります。

そのことの理解なくして、皆様が数式で表した内容が、本当に守らせたかったことと一致しているかどうかを判断できないからです。

証明を書く手を AI に譲ったあとも、仕様を読み、その妥当性を判断する目は、必要であり続ける
── これが、この分野を学ぶ意味の、もうひとつの側面です。

言い換えれば、こうなります。

AI に証明を書かせることよりも、AI が書いた「仕様が、本当に人間の意図を表しているか」を確認することのほうが、難しい問題になる可能性があります。

前者は、検証器が解決します。
後者を解決する仕組みは、いまのところ存在しません。

ここで、公平を期して留保を述べます。

人間が仕様を書けば正しい、という話ではありません。

仕様の誤りは、人間が書いた場合にも頻繁に起こります。
実際、形式検証の失敗事例の多くは、証明の誤りではなく仕様の誤りです。

ここで述べたのは、「AI に任せれば人間より良くなる」とは言えない、ということです。
仕様と意図の隔たりは、形式的な仕組みでは埋まりません。

埋められるのは、意図を持つ当事者だけです。

また、AI が仕様の起草を大幅に助けることは、すでに現実です。 ここで論じたのは「起草を任せられるか」ではなく、「確認する者を不要にできるか」という問いへの答えです。

Physical AI と AI エージェント ── 伸びるのは、どちらの手法か

ここで、この記事でいちばん先の話をします。

ロボットや自動運転（Physical AI）、そして LLM を使ったエージェント。

これらの検証で産業ニーズが伸びるのは、第２部で見た③④・②・①のうち、どれでしょうか。

調べたかぎり、答えは「システムの層によって違う」です。

順に見ていきます。

知覚と制御の層 ── ここは、機械が自動で調べる手法の領域

ロボットや自動運転のニューラルネットワークそのものを検証する研究は、この10年で厚く積み上がりました。

そこで使われているのは、抽象解釈（AI2、DeepPoly といった手法）、到達可能性解析、SMT ソルバ（Reluplex、Marabou）、混合整数計画、そして有限状態への抽象化です。

たとえば、LiDAR 画像を処理して制御指令を出すニューラルネットワーク制御器について、**「この初期状態から出発すれば、障害物に衝突しないことが保証される」**初期状態の集合を、有限状態に抽象化したうえで到達可能性解析によって求める
── そうした研究が、実際に行われています。

なぜ、知覚と制御の検証では、自動手法が使われるのでしょうか。

第２部で述べた区別を思い出してください。
証明したい性質の種類が、あらかじめ決まっているからです。

• 入力が少し変わっても、出力が破綻しないかどうか（頑健性）
• 危険な領域に入らないかどうか（到達可能性）
• 実行時にエラーで止まらないかどうか

いずれも、成り立っているかどうかを証明したい性質の型が、ツールの側にあらかじめ用意されています。

利用者が書くのは、その型に当てはめる数値だけです。

たとえば頑健性なら、「入力が指定した範囲にあるとき、出力は指定した範囲に収まる」という形式がツールに備わっており、利用者は入力と出力の範囲を数値で指定します。性質そのものを一から記述するわけではありません。

第２部の分類では、③④に近い位置づけです。しかも、センサ値の範囲は物理的に限られています。

ただし、ひとつ補足しておきます。

この、知覚と制御を検証する領域は、日本が伝統的に強い制御工学の延長線上にあります。

ニューラルネットワークの検証ツール自体が正しいかを問う研究 ── 検証器が出す結論に、独立に検算できる証明を添える試み ── が存在します。

これは、第２部で見た「基盤層」の構図と同じです。検証ツールもまた、その上に多くの判断が乗る基盤なのです。

方針と規則の層 ── ここは、人が性質を書き下す領域

しかし、エージェントが社会の中で動き始めると、まったく別の問題が現れます。

ある研究は、この違いを鋭く指摘しています。

ニューラルネットワークの形式検証は、個々のネットワークの頑健性を対象とするものであって、「エージェントは、申込者の返済比率の基準を超える融資を決して承認しない」といった、エージェントの振る舞いのレベルの性質は対象にしていない、というのです。

「返済比率の基準を超えない」── これは、頑健性でも到達可能性でもありません。
業務の規則そのものを、その都度、書き下したものです。

だから、性質を自分で書き下す必要が生じます。
第２部の分類でいえば、①か②です。

実際、2026年に入ってから、この方向の研究と実装が急速に立ち上がっています。

• 金融エージェントの規制適合を Lean 4 で保証する試みがあります。
  Harmonic AI の Aristotle というモデルで institutional policy を Lean 4 のコードへ自動形式化し、エージェントが提案するあらゆる行動を「数学的な予想」として扱い、Lean 4 のカーネルが「その行動が規制を満たす」と証明したときにのみ実行を許すという設計です。
   
• エージェントのワークフローと実行軌跡を Lean で検証する研究もあります。
  依存型による述語システムで各実行ステップの事前条件・事後条件を記述し、違反したステップを特定するという３層構造です。
   
• AWS の Automated Reasoning checks のように、SMT ソルバの上に構築されたものもあります。
  こちらは②の系統です。
  人が方針を書き、SMTが判定を自動で行います。

ここで見落としてはならない点があります。

①であれ②であれ、「規則を人が書き下す」ことは避けられません。
分かれるのは、その証明を機械が自力で見つけられるかどうかだけです。

規則が SMT で扱える形に収まるなら②で足り、収まらなければ①が必要になる。
第２部で見た、暗号ライブラリと OS カーネルの分かれ目と、まったく同じ構図です。

そして、両者をつなぐ層が、最大の未解決問題です

ここが、いま最もホットで、そして最も難しい領域です。

自然言語で書かれた規則（法令、社内規程、契約）を、形式的な仕様に翻訳する
── この工程は、まだ誰にも解けていません。

ある解説は、2026年夏の時点の状況をこう総括しています。

**証明器は数学オリンピックの金メダル級に達した。
翻訳器には信頼度スコアがつくようになった。

本番に投入しているチームは、SMT による方針検査と忠実性レポートを組み合わせている。**

そして、安全性の担当者は、モデルそのものではなく、ガードレールのほうを検証している。

「モデルが何を考えているかは証明できない。しかし、モデルに何をさせてよいかは証明できる」
この割り切りが、現在の実務の到達点です。

それでもなお残るのが、翻訳の工程です。

文法や構文の検査は、形式的な出力が構文として正しいことを保証できます。
しかし、意味が正しく移されたかどうかを保証する確立した方法は、まだありません。

そして、この困難の根底にあるのが、ひとつ前の節で述べたことです。

「意味が正しく移されたか」は、形式的な問いではありません。
照合すべき原本 ── 人間の意図 ── が、形式の世界に存在しないからです。

つまり、翻訳の層が難しいのは、技術が未熟だからだけではありません。
そこに、形式化できない問いが横たわっているからです。

だからこそ、この層は「自動化して終わり」にはなりません。
AI が翻訳し、人が読んで判断する
── その協働の形を設計することが、当面の課題になります。

ここが、機械学習の素養と、証明支援系の素養が、両方必要になる場所です。

キャリアとして、どう読むか

以上を、職域として整理します。

システムの層	主に使う手法	性質を書くのは	求められる素養	現在の状況
知覚・制御（NN そのもの）	③④	ツールに組み込み済み	制御工学、最適化、抽象解釈	研究が厚く、産業適用が進みつつある
方針・規則（エージェントの行動）	②と①	人	論理学、型理論、Lean/Rocq	2026年に立ち上がったばかり
翻訳（自然言語→形式仕様）	──	人（AI が起草を補助）	機械学習 ＋ 証明支援系の両方	確立した方法はまだない

この表が示すことは、はっきりしています。

知覚と制御の検証だけを見るなら、証明支援系の出番は限られます。

しかし、エージェントが社会の規則の中で動く以上、規則の層は避けて通ることはできません。
規則の検証は、2026年に立ち上がったばかりの領域です。

いま需要が高まっているのはどちらなのか

ここまでの整理を踏まえて、現時点での見立てを述べます。

現時点で実務を動かしているのは、③④と②です。

①の需要は立ち上がり始めた段階であり、需要はまだ小さい
── これが、公開されている論文と事例から読み取れる状況です。

ただし、②と③④を一括りに「自動」と呼ぶと、大事なことを見落とします。

②では、人が性質を書く必要があります。
自動なのは証明を探す部分だけです。

以下、この区別を意識してお読みください。

順に、根拠を示します。

第１に、AI モデルそのものの検証は、③④が担っています。

前節で見たとおり、ニューラルネットワークの検証に使われているのは、抽象解釈、到達可能性解析、SMT ソルバ、混合整数計画です。検証したい性質が、頑健性や到達可能性といった決まった種類だからです。

筆者が確認できた範囲では、この層に証明支援系を実用規模で持ち込んでいる事例は見当たりませんでした。

第２に、規則の層では、②が主流です。

AWS の Automated Reasoning checks は、SMT ソルバの上に構築されています。

2026年夏時点の総括にも、本番環境に投入しているチームは、SMT による方針検査と忠実性レポートを組み合わせている と書かれています。

ここで、重要な区別があります。

②では、規則そのものは人が書きます。
自動化されるのは、その規則が守られているかを判定する部分です。

つまり「規則を形式的に書き下せる人」の需要は、②の段階ですでに発生しています。
必ずしも「Lean で証明を組み立てられる人」である必要はありません。

SMT が扱える形に収まる規則であれば、②で足りるのです。

ここで、注意すべき点をひとつ。

「SMT ソルバを使うから自動手法である」と単純に言うことはできません。

SMT ソルバは、多くのツールの内部エンジンとして使われています。第１部の表で②に分類した Dafny や F* も、SMT ソルバを内蔵しています。そして、第２部で見た暗号ライブラリ HACL* を検証したのは、その F* です。

つまり SMT は、自動手法と、人が仕様を書く手法の、両方にまたがっています。

正確な言い方はこうです。

「SMT が自力で証明を見つけられる範囲の性質なら、自動で判定できる。見つけられなければ、人間が補助を書き足すか、証明支援系に移るしかない」

自動化の度合いは、道具の名前ではなく、扱う性質の複雑さによって決まります。

第３に、②では届かず、①でなければ扱えない場面が存在します。

筆者が確認できたかぎり、次の３つです。

（１）規則が複雑で、その都度書き下すしかない場合。
前述の金融エージェントの事例がこれにあたります。
多層の規制条件を Lean 4 で記述し、カーネルが証明した行動のみを実行する、という設計です。

（２）証明そのものを成果物として渡す必要がある場合。
「判定しました」ではなく「独立に検算できる証明書が付いています」という形です。
LLM のパイプラインに証明つきの証明書を添える研究が、現れ始めています。

（３）AI に証明を書かせる、その研究と製品そのもの。
AlphaProof、DeepSeek-Prover、Harmonic の Aristotle。
現時点で、証明支援系の需要が最も厚いのは、実はここです。

ただし、この３つ目については、慎重に書いておく必要があります。

「研究の需要にすぎない」と切り捨てるのも、また不正確です。

Harmonic は製品を出しており、その技術が前述の金融エージェントの形式化に使われています。
研究と産業の境目は、この分野では曖昧です。

まとめると、こうなります。

「AI 時代の到来によって、証明支援系の需要が高まっている」
この言い方は、いまの時点では強すぎます。

より正確には、①の需要は、ゼロに近いところから立ち上がり始めた段階です。

規則を検証する仕組みが実際に現れたのは2026年であり、絶対量はまだ小さい。
実務の多くは、③④と②が回しています。

ただし、②では届かない場面が確実に存在し、そこに①が入り始めている
これが、現状をそのまま述べたものです。

学ぶかどうかの判断に引き直すなら、こうなります。

• 「規則を形式的に書き下す」能力は、②の段階ですでに求められています。
  ここは、①ほど習得が重くありません
   
• ①（Lean などで証明を組み立てる）が、いますぐ職に直結する量を持つかといえば、そうではありません。 需要の絶対量は、まだ小さいためです
   
• 数年先を見て、まだ人が少ない領域に先に入っておきたいなら、合理的な選択です。 立ち上がり始めた段階だからこそ、先行者が少ない
   
• そして、①を学ぶ過程で身につく「性質を形式的に書き下す力」は、②でもそのまま使えます。 学習が無駄になる構造ではありません

さらに、自然言語の規則を形式的な仕様へ翻訳する仕事は、機械学習と証明支援系の両方を身につけた人にしか手が出せません。

世界的にも、そうした人材はまた多くないのが実情です。

なお、ここで述べた需要の大小は、公開されている論文と事例からの筆者の見立てです。
求人数や市場規模を示す統計を確認したわけではありません。

この点は、割り引いてお読みください。

---

第６部 ── 世界のどこで求められているのか

ここで、視野を世界に広げます。

同じ技術なのに、なぜ国によって需要がこれほど違うのか？

鍵を握るのは、「安全のための規格や法令が、形式手法をどれだけ求めているか」 です。

需要を生む、いちばんの源は「規格」

形式証明・定理証明が職業として成立している国には、共通の背景があります。

バグが許されない製品に、安全規格が形式手法を要求・推奨しているという点です。

DO-178C ／ DO-333（航空・宇宙）

DO-178C は、航空機に搭載するソフトウェアの認証基準です。

（正式名称は "Software Considerations in Airborne Systems and Equipment Certification"。米国の業界団体 RTCA（Radio Technical Commission for Aeronautics、航空無線技術委員会）が策定）

ちなみに、この "DO" は "Document"（文書） の略で、RTCA が発行する文書の連番です。

この DO-178C に、形式手法の使い方を定めた補足文書 DO-333（"Formal Methods Supplement to DO-178C and DO-278A"）が付属します。

米国の RTCA と、その欧州版にあたる EUROCAE（European Organisation for Civil Aviation Equipment、欧州民間航空機器機構）が共同で策定しました。

Common Criteria（情報セキュリティの国際規格）

正式名称は "Common Criteria for Information Technology Security Evaluation"。ISO/IEC 15408 として標準化されています。

この規格では、評価の厳しさを EAL（Evaluation Assurance Level、評価保証レベル）という7段階で表します。

最高レベルの EAL6 と EAL7 は、形式手法の使用を要求します（EAL6 は準形式的、EAL7 は完全に形式的な設計・検証）。

EAL6 は暗号システムや政府 IT、EAL7 は軍事・機密の政府システムに用いられます。

ISO 26262（自動車）

車載の電気・電子システムの機能安全規格です。汎用の機能安全規格 IEC 61508 を自動車向けに特化させたものです。

この規格は日本メーカーも準拠しており、形式手法を推奨しています。 日本の学会誌でも、車載システム開発において形式手法が注目されたのは、機能安全規格において形式手法が推奨されていることが大きく影響している、と指摘されています。

EN 50128（鉄道）

欧州の鉄道用ソフトウェアの安全規格です（EN は European Norm、欧州規格）。
安全度水準（SIL、Safety Integrity Level）の高い区分では形式手法が推奨されています。

つまり、「形式手法を求める規格」は、グローバルな国際標準として存在します。
そして Common Criteria や ISO 26262 は、我が国も参加・準拠しているのです。

なぜ国ごとに需要が違うのか

第１に、規格が「実際にどれだけ運用で使われるか」の差です。

規格が「形式手法を推奨する」と書いていても、それを本気で実践するかは産業の慣行や発注側がどこまで求めるかによります。

米国では、国防総省や NSA、NASA が調達の条件として高い保証水準を求めるため、形式手法が「絵に描いた餅」で終わらず、実務に降りてきます。

第２に、基盤層を「自国で設計する」度合いの差です。

第３部で述べたとおり、これが決定的です。OSカーネル、暗号基盤、コンパイラ、認可エンジン ── こうした「基盤そのもの」を自国で設計する国ほど、性質を自由に書き下す必要が生じ、証明支援系の需要が国内で発生します。

第３に、教育と人材供給のパイプラインです。

証明支援系を使うには、論理学と型理論の素養が要ります。
計算機科学の教育にこれらの理論科目が厚く組み込まれている国ほど、実務で証明を書ける人材が継続的に供給されます。

これらを、主要国について整理したのが次の表です。

（各国の状況は変化しますし、筆者の把握には限界があります。大まかな傾向としてお読みください。）

なお、米国・欧州・日本については、規格や公開事例、学術論文などから比較的たしかなことが言えます。

他方で、中国・ロシア・インドの3か国については、公開情報が限られており、以下は Web 上で確認できた範囲からの推測を多く含みます。

国・地域	形式手法を求める主な規格・制度	需要が生まれる分野	実務での位置づけ
米国	DO-178C/DO-333、Common Criteria（EAL6/7）、国防・NASA の調達要件	航空宇宙、防衛、暗号、OS、AI検証	最も厚い。 調達要件が実務を牽引し、研究と産業の距離も近い
欧州（英・仏・独など）	DO-333、EN 50128（鉄道）、Common Criteria、ISO 26262	航空（Airbus）、鉄道、自動車、スマートカード	厚い。 規格運用が定着し、Airbus など旗艦事例がある
日本	ISO 26262、Common Criteria（いずれも準拠）	自動車、半導体、宇宙（JAXA）	規格はあるが、証明支援系の実務採用は限定的。 制御系中心の産業構造
中国	独自の安全規格整備を進行、OS・チップの国産化政策	OS、チップ、通信インフラ	国家戦略として投資が拡大中とされる。 基盤国産化と結びつく（※確度は低い）
ロシア	独自のセキュリティ認証制度	防衛、政府システム	国内向け中心で、国際的な可視性は低い（※確度は低い）
インド	航空・防衛の国産化、IT サービス産業	航空防衛、受託開発の一部	発展途上。研究層は厚いが、国内実務需要はこれから（※確度は低い）

各国間で差が生まれた歴史的背景

なぜ、米国と欧州が突出しているのでしょうか。

形式手法が「学術的な演習」から「産業で使えるもの」へ移り始めたのは、そう古いことではありません。自動定理証明器の近年の進歩が、形式手法を産業利用の近くまで運んできた、とされます。

そして、航空機搭載ソフトウェアは、早くから形式手法の適用先として認識されてきました。

Airbus は、単体テストを置き換えるものとして形式手法 Caveat を検討しており、Airbus が欧州の航空業界で先導的立場にあることから、将来、高度に安全上重要な搭載ソフトの開発に形式手法の使用が義務づけられることが予想されると論じられています。

つまり、

「事故が許されない基盤産業（航空・防衛・宇宙）を国内に厚く抱え」、「その調達者（政府・軍）が高い保証を要求し」、「規格がそれを制度化している」
── これら三拍子が揃った国で、形式手法は産業として根を張ったのです。

米国と欧州が先行したのは、この３つの条件を最も早く満たしたからだと考えられます。

「Airbus はわかったが、Boeing は？ HondaJet はどうなのか？」

ここで、Airbus ばかりが例に挙がることを、不思議に思われたかもしれません。補足しておきます。

形式手法を使っているのは、Airbus だけではありません。

そもそも、航空ソフトの認証基準 DO-178C とその形式手法補足 DO-333 は、米国の FAA（連邦航空局）、欧州の EASA、カナダ運輸省、さらに中国の民航局（CAAC）などが共通で用いる国際的な枠組みです。

Boeing も、この同じ基準の下で開発を行っています。 Boeing は DO-333 の発行にも関与しており、形式手法や静的解析を、認証プロセスの中で用いています。

では、なぜ Airbus の事例ばかりが引用されるのか。理由は単純で、Airbus（および検証ツール Astrée の開発陣）が、その実践を学術論文として詳しく公開してきたからです。

Boeing は、同種の取り組みを社外に詳しく公開する度合いが低く、事例として引用しにくい
── ただそれだけのことです。

HondaJet（Honda Aircraft） も同様です。米国で型式証明を取得して就航している以上、その搭載ソフトは DO-178C に準拠して開発・検証されています。日本発の航空機が、この国際基準の枠組みの中で認証を通しているわけです。

つまり、形式手法を含む高保証の開発文化は、特定の一社の専有物ではなく、航空という産業の共通基盤なのです。

規格が推奨しても、なぜ求人に直結しないのか

ここで、当然の疑問が残ります。

ISO 26262 のように、日本も準拠する規格が形式手法を推奨しているのなら、なぜそれが証明支援系の求人につながらないのでしょうか。

第１に、「形式手法」と「証明支援系」は、同じではないからです。

第１部で見たとおり、「形式手法」という言葉は非常に広く、モデル検査、静的解析、抽象解釈、そして証明支援系まで、性格の違う複数の技術を含みます。

そして、規格が「形式手法を推奨」と書くとき、実際に現場で採用されやすいのは、性質があらかじめ決まっている手法のほうです。

人が仕様を書き、証明の道筋も設計する証明支援系は、最もコストが高く、規格が認める選択肢の「一つ」ではあっても、多くの現場が真っ先に選ぶものではありません。

「規格が形式手法を推奨する」ことと、「証明支援系エンジニアの求人が出る」ことのあいだには、大きな距離があるのです。

第２に、規格の「推奨」は「義務」ではないからです。

ISO 26262 において形式手法は、安全度水準の高い区分で「推奨（recommended）」される技法の一つであって、多くの場合、必須ではありません。

企業は、同等の安全性を別の手段（徹底したテストなど）で示せれば、規格に適合できます。

第３に、コストを誰が負担するか、という会計の問題です。

形式検証は、開発の前半に大きなコストがかかり、その見返りは「起きなかった障害」という目に見えない形で返ってきます。とくに受託開発の構造では、「検証にかけたコスト」と「防げた損失」の受益者がずれてしまい、投資判断が働きにくくなります。

第４に、人材供給と言語の壁です。

この分野の一次情報 ── 教材、コミュニティ、求人 ── の大半は英語です。
「需要が少ないから人材が育たず、人材が少ないから企業も導入をためらう」という低い水準での均衡が生じています。

裏を返せば、これらはすべて参入の余地です。
日本語で正確な解説が乏しいなら、書けば価値になります。

---

第７部 ── では、あなたはどう位置取るか

ここまでの整理を、キャリアの選択肢として組み直します。

選択肢１：海外の基盤産業を目指す。

米国・欧州には、航空・防衛・暗号・OS の分野に、証明支援系を使う職が現に存在します。求人の絶対数は日本国内と桁違いです。ただし、多くは英語での実務となり、分野によっては国籍やセキュリティクリアランスの制約もあります。

選択肢２：AI × 証明支援系に賭ける。

これが、日本にいる読者の皆様にとって、最も現実的で、かつ伸びしろの大きい道かもしれません。

理由は３つあります。

第１に、この領域はまだ世界的に人材が不足しています。

第２に、規格や国籍の壁が、従来の基盤産業ほど高くありません。

第３に、そして最も重要なことに、Python で機械学習をしてきた読者の皆様は、すでに片方の素養を持っているのです。あとは証明支援系を足すだけです。

選択肢３：国内の基盤層に踏み込む。

第３部で見たとおり、日本で需要が乏しかったのは、基盤層を自国で作る機会が少なかったからです。逆に言えば、日本が基盤層を自国で持とうとするとき、そこに需要が生まれます。 その最初の担い手になる、という道です。

いずれの道も、出発点は同じです。証明支援系を、実際に書けるようになること。

日本の産業は、この地図のどこに立っているのか

最後に、視野をもう一段広げます。日本の産業界は、この新しい地図のどこに立っているのでしょうか。

第一に、日本は「検証すべき対象」を、世界有数の規模で持っています。

産業用ロボット、自動車、工作機械、工場の自動化設備 ── 物理世界で動く機械の現場を、これほど厚く抱えている国は多くありません。

Physical AI の検証という分野は、検証したい実物がなければ、そもそも成立しません。

アルゴリズムだけを研究しても、現場のセンサ特性、実際の事故のモード、認証の実務を知らなければ、意味のある仕様は書けないのです。

「対象を持っていること」は、この分野では希少な資産です。 ここは、日本が失っていない強みです。

第二に、知覚・制御の層は、日本の伝統的な強みの延長線上にあります。

前節で見たとおり、この層で使われるのは、到達可能性解析や抽象解釈といった自動手法です。制御工学、信号処理、安全設計 ── いずれも、日本の製造業が長く蓄積してきた領域と地続きです。

しかも第３部で見たとおり、日本にはモデル検査を制御系に適用した実績（JAXA の衛星姿勢制御、鉄道の進路制御など）があります。まったくの白紙からではありません。

第三に、しかし価値が移りつつあるのは、規則の層と翻訳の層です。

ここが、正面から見据えるべき論点です。

機械が優秀に動くことと、その機械に何をさせてよいかを規則として書き下し、証明すること ── 後者の比重が、これから上がります。エージェントが社会の規則の中で動く以上、避けられません。

そして、この層では、性質を人が書き下す必要があります（②か①）。 第３部で見たとおり、日本が最も手薄にしてきた領域です。

第四に、それでも、この新しい層では、まだどの国も先行を確定させていません。

規則の層の実装が本格的に立ち上がったのは2026年です。
翻訳の層に至っては、世界の誰も解けていません。

従来の基盤層 ── 暗号、OS、コンパイラ ── では、米欧に半世紀の蓄積がありました。
後から参入するのは容易ではありません。

しかし、AI エージェントの規則を検証するという層は、まだ数年の歴史しかないのです。

まとめると

検証すべき対象（Physical AI の現場）を持っているという強みを、規則の検証まで押し上げられるかどうか ── ここが分かれ目になるのではないか、と考えられます。

具体的には、次のような構図です。

• 現場だけを持ち、規則の検証を他国に委ねる ── 暗号やOSやコンパイラで起きたことが、繰り返されます。機械は作るが、その機械に何をさせてよいかの規則は、他国が定義し、他国が証明する
   
• 現場を持ち、規則の検証も自国で押さえる ── 日本の産業が持つ「実際に何が危険か」の知見を、形式的な仕様として書き下せる人材がいれば、この仕事を自国で担えます

そして、その人材に必要なのが、まさにこの記事で扱っている技術です。

読者の皆様が Python で機械学習を書いてこられたのでしたら、皆様は、すでに機械学習の素養をお持ちです。

あとは、証明支援系に関する理解を構築されれば、この仕事にも手が届くのではないでしょうか。

なお、これを「勝機」と呼べるかどうかは、まだ分かりません。

この領域が本当に大きくなるのか、規則の検証で価値が生まれるのか
── いずれも、これから決まることです。

ここで述べたのは、「暗号やOSやコンパイラのときと違い、まだ横並びに近い」という一点にすぎません。
それ以上でも、それ以下でもありません。

---

第８部 ── では、実際にどう書くのか

言葉だけでは、イメージがつかめないと思います。

「仕様どおりに動くこと」を、コードでどう保証するのか ── 短い例で、雰囲気だけお見せします。

注記： 以下のコードは、公式資料・定番教材の記法に基づいて書いていますが、バージョンによって細部が異なる場合があります。

最終的な動作確認は、ご自身の環境でお願いします。

また、これらは「雰囲気をつかむ」ための最小例です。

各言語の本格的なコードの書き方と、一行ずつのコードリーディングは、次回の記事で詳しく解説します。

例１： Lean で「a + b = b + a」を証明する

まず、証明支援系の最も基本的な体験です。自然数の足し算が順番によらないこと（可換律）を、Lean で証明します。

theorem add_comm_demo (a b : Nat) : a + b = b + a := by
  induction a with
  | zero      => simp
  | succ n ih => rw [Nat.succ_add, Nat.add_succ, ih]

一行ずつの意味は次回に譲りますが、雰囲気だけ。by から下は、証明を組み立てる操作の列です。induction a は「$a$ について場合分けして帰納法を使う」、rw は「等式で書き換える」という操作です。

プログラムを書く感覚に近いのが伝わるでしょうか。

実際、Lean の証明は「デバッガのセッションのようだ」とよく言われます。

画面には常に「いま証明すべきこと（ゴール）」と「使える前提」が表示され、操作を一つ加えるたびに、ゴールが変化していきます。

これが、Natural Number Game でブラウザから体験できる中身です。

例２： Rocq（旧 Coq）で「リストを2回反転すると元に戻る」を証明する

次は、プログラムの性質の証明です。

Theorem rev_involutive : forall (A : Type) (l : list A),
  rev (rev l) = l.
Proof.
  intros A l. induction l as [| x xs IH].
  - simpl. reflexivity.
  - simpl. rewrite rev_app_distr. rewrite IH. simpl. reflexivity.
Qed.

「当たり前」に見えても、それを機械が納得する形で証明するには、リストの構造に沿った場合分けと、帰納法が必要です。

Software Foundations で最初に出会う、定番の練習です。

例３： Agda で「空のリストから先頭を取り出せない」を型で保証する

ここが、Python エンジニアの読者の皆様に、最も響く例かもしれません。

Python で、空のリストの先頭要素を取ろうとすると、実行してみて初めてエラーになります。

lst = []
print(lst[0])   # 実行時に IndexError で落ちる

Agda では、長さを型に持つベクタ（Vec）を使うと、これがコンパイル時に、型の段階で弾かれます。

-- 長さ n を型に持つベクタ
data Vec (A : Set) : ℕ → Set where
  []  : Vec A zero
  _∷_ : {n : ℕ} → A → Vec A n → Vec A (suc n)

-- head は「長さが 1 以上のベクタ」しか受け取らない
head : {A : Set} {n : ℕ} → Vec A (suc n) → A
head (x ∷ _) = x

head の型は Vec A (suc n)
── つまり「長さが 1 以上のベクタ」しか受け取りません。空のベクタを渡すコードは、そもそも型が合わず、コンパイルが通りません。

Python では「実行時に落ちる」ものが、Agda では「そういうコードは書けない」に変わります。

第５部で触れた、テンソルの次元不一致で学習が落ちるという話を思い出してください。

行列の形（shape）を型に持たせれば、次元の合わない計算は、実行するまでもなく、型検査の段階で弾かれます。 数時間待ってから落ちるのではなく、書いた瞬間に分かる
── これが、型で仕様を表現することの実利です。

ここで、専門用語をひとつだけ ── 「依存型」とは何か

いま見た Vec A (suc n) という書き方が、依存型（dependent type）と呼ばれるものです。

ふつうのプログラミング言語では、型は int や str のように、中身の値とは無関係に決まります。 [1,2,3] も [1,2,3,4,5] も、どちらも「整数のリスト」で、同じ型です。

ところが依存型では、**型が「値」に依存して決まります。

** 「長さ3のベクタ」と「長さ5のベクタ」は、別の型になるのです。

型が値に依存する ── だから「依存型」です。

この仕組みがあるからこそ、仕様そのものを、型として書き表せるわけです。

Lean、Rocq、Agda、Idris は、いずれもこの依存型を基盤としています。

一方、Isabelle/HOL は違う基盤を採ります。

こちらは高階論理（higher-order logic、HOL）と呼ばれる体系です。

「高階」というのは、関数それ自体を、値と同じように扱って議論できるという意味です。

依存型ほど型で細かく縛ることはできませんが、そのぶん自動証明との相性がよく、Isabelle の強力な自動化（Sledgehammer）は、この基盤の上に成り立っています。

例４： TLA+ で「分散システムが不整合な状態に陥らない」ことを検査する

最後は、少し毛色が違います。
プログラムのコードではなく、システムの設計を検証する例です。

TLA+ では、システムが取りうる状態と、状態が遷移する規則を記述し、「どんな順序で処理が起きても、決して不整合な状態に到達しない」ことを、ツールが総当たりで検査します。

前述のとおり、AWS が S3 や DynamoDB の設計で、人間のレビューでは見逃していた深刻なバグを、この方法で発見しています。

---

第９部 ── 論理学の理解がどこまで進んだら、定理証明・形式検証を学べ始められるのか

いちばん多く寄せられる誤解を解消しておきます。

論理学を体系的に修めてから証明支援系に入る、という順序は、必要ありません。
むしろ、それをやろうとして途中で力尽きる方が多いのです。

数理論理学は、それ自体が広大な分野です。

完全性定理、不完全性定理、モデル理論
── これらを一通り学ぼうとすれば、それだけで年単位になります。

そして、その大半は、証明支援系を使うのに必要ありません。

必要なのは、次の項目だけです。

項目	必要か	理由
命題論理の記号が読める	必須	記号が読めないと、画面の表示が読めません
述語論理（一階）の量化子	必須	$\forall$ と $\exists$ は、証明支援系の中核です
自然演繹の推論規則	必須	これが、そのまま操作に対応します
直観主義論理と古典論理の違い	必須	排中律が使えるかどうかが、体系ごとに違います
Curry-Howard 対応	強く推奨	「証明はプログラムである」という発想の核心です
完全性定理の証明	不要	使う分には知らなくて構いません
不完全性定理	不要	教養としては面白いのですが、実作業には出てきません
モデル理論	不要	意味論を研究する段階になってからで十分です

いちばん重要なのは、自然演繹の推論規則です。
なぜなら、それがそのまま、証明支援系の操作になっているからです。

たとえば「$A \to B$ を証明するには、$A$ を仮定して $B$ を導けばよい」という含意の導入規則。

これは、Lean や Rocq では intro という操作に、Agda では関数を書くことに、そのまま対応します。

目安としては？

教科書の第３章あたりまで、と考えてください。

命題論理と述語論理を扱い、自然演繹の規則を一通り見て、健全性・完全性の主張だけを知る。その証明を追い切る必要はありません。

そこまで来たら、証明支援系を触り始めてください。

残りの論理学は、必要になったときに戻ればよいのです。

むしろ、触り始めたほうが論理学の理解も速くなります。

論理学の教材

和文

• 小野寛晰『情報科学における論理』日本評論社 ── 計算機科学向けで、直観主義論理と型理論への接続まで扱います。この分野に進むなら、最も近い一冊です。
   
• 前原昭二『記号論理入門』日本評論社 ── 薄く、記号の読み方から入れます。最初の一冊に。

英語

• Girard, Lafont, Taylor『Proofs and Types』── 無料公開。Curry-Howard 対応の古典で、薄いのに密度が高い一冊です。

---

第１０部 ── どの言語を、どの順で学ぶか

その前に ── ５つ全部を学ぶ必要は、ありません

ここまで５つの言語を比べてきたので、こう思われた方がいるかもしれません。
「結局、全部やらないといけないのか」 と。

結論から申し上げます。その必要は、まったくありません。

５つを浅く触るより、１つを深く学ぶほうが、はるかに価値があります。

証明支援系で本当に難しいのは、個々の言語の文法ではなく、「証明を組み立てる」という考え方そのものです。それは、どれか１つの言語で身につければ、他の言語へもかなりの部分が持ち越せます。

まず、Lean 4 から

迷ったら Lean 4 を勧めます。理由は、言語設計の優劣ではありません。始めやすさと、続けやすさです。

第１に、Natural Number Game があります。 ブラウザで動くゲーム形式の入門で、インストール不要です。環境構築と最初の一週間で挫折するという、この分野で最も多い脱落を、跳ばせます。

第２に、Mathlib があります。 現代数学を形式化した巨大ライブラリで、25万を超える定理が入っています。「証明したいことの前提が、もう証明されている」状態から始められます。

第３に、コミュニティが最も活発です。 これが、実はいちばん重要かもしれません。この分野は、詰まったときに検索してもほとんど何も出てきません。 Lean には Zulip という公式コミュニティがあり、初心者の質問にも丁寧な回答がつきます。質問できる場所があるかどうかが、続けられるかどうかを決めます。

第４に、数学・プログラム検証・AI の交差点に位置しています。 記事の前半で見たとおり、AlphaProof をはじめとする AI 側の取り組みは Lean を証明環境として使っており、AWS の Cedar も Lean で検証されています。進む方向を後から選べる、という利点があります。

ただし、Lean だけが正解ではありません。

プログラム検証そのものが目的なら Rocq（Software Foundations という教材があります）、型理論を深く学びたいなら Agda、大規模な高保証システムに関心があるなら Isabelle/HOL ── それぞれに合理的な選択があります。

Lean を最初に勧めるのは、**「迷っている段階で、最も脱落しにくいから」**であって、言語として優れているからではありません。

次に、目的に応じて分岐する

• 数学の形式化を深めたい → Lean のまま進めます。Mathlib という最大の資産があります。
• プログラム検証をしたい → Rocq（旧 Coq） へ。Software Foundations という全６巻の無料教材が、この分野の金字塔です。
• 大規模システムの検証を見たい → Isabelle/HOL へ。seL4 マイクロカーネルの完全検証で使われた実績があります。なお、第８部で述べたとおり、Isabelle は他の４つとは理論的な基盤が異なります（Lean・Rocq・Agda・Idris が依存型、Isabelle/HOL は高階論理）。

Idris 2 の、独自の価値

Idris は、証明支援系というより、依存型を持った実用プログラミング言語です。「証明を書く」のではなく、**「型で仕様を表現する」**という発想が身につきます。

この発想だけを、業務のコードに持ち帰ることができます。

各言語の性格、一覧

言語	論理の基盤	強み	学ぶ順番
Lean 4	依存型	Mathlib、Natural Number Game、活発なコミュニティ、AI連携	1番目
Rocq（旧Coq）	依存型	Software Foundations、産業実績（CompCert 等）	2番目（検証志向）
Agda	依存型	「穴を掘りながら書く」対話的開発、型理論の学習	2番目（型理論志向）
Isabelle/HOL	高階論理	Sledgehammer による強力な自動化、seL4 の実績	3番目
Idris 2	依存型＋量的型理論	実用言語としての設計、型による仕様表現	3番目

学ぶ順序、まとめ

どれくらいの期間を見ればよいか

段階	内容	期間の目安
第１段階	論理学の入口（命題論理・述語論理の記号、自然演繹の規則）	1〜2週間
第２段階	Lean 4 に触れる（Natural Number Game を一通り）	1〜2週間
第３段階	Lean 4 を本格的に学ぶ（Theorem Proving in Lean 4）	1〜2か月
第４段階	目的別に深める（Mathematics in Lean、Software Foundations など）	数か月〜
第５段階	自作の小さな命題を証明する／ライブラリに貢献する	継続的に

この期間は、あくまで目安です。 重要なのは期間そのものより、第１段階と第２段階を、あまり時間をかけずに通り抜けることです。論理学を完璧にしてから進もうとすると、たいてい、そこで力尽きます。

主要な教材

いずれも無料で、質が高いものばかりです。

Lean 4

• Natural Number Game ── ブラウザで動くゲーム形式の入門
• Theorem Proving in Lean 4 ── 公式教科書（無料）
• Mathematics in Lean ── 数学の形式化に特化（無料）
• Lean Zulip ── 公式コミュニティ

Rocq（旧 Coq）

• Software Foundations（全６巻、無料）── この分野の金字塔
• 萩原学、アフェルト・レナルド『Coq/SSReflect/MathComp による定理証明』森北出版 ── 数少ない和書

Agda

• Programming Language Foundations in Agda（PLFA、無料）

Isabelle/HOL

• Nipkow, Klein『Concrete Semantics』（無料公開）

Idris 2

• Brady『Type-Driven Development with Idris』

---

第１１部 ── 学び続けるために

この分野は、教材を読むだけでは身につきません。

第１に、小さな自作課題を作ってください。 リストを2回反転すると元に戻る。ソートの結果が整列している。こうした小さな命題を、自分で立てて証明します。地味ですが、この分野の実力は、ここでしか育ちません。

第２に、既存の証明を壊して、直してください。 ライブラリの証明から一行消すと、エラーの出た場所が、その一行の役割です。

第３に、ライブラリに貢献してください。 Mathlib などはオープンです。誤字の修正、証明の短縮から始められます。

第４に、コミュニティに入ってください。 この分野は独学の難易度が突出して高い。質問できる場所を確保してから始める ── これが、続けられるかどうかを最も強く左右します。

---

次回予告 ── 各言語のコードを、一行ずつ読む

この記事では、コードは「雰囲気をつかむ」程度にとどめました。次回の記事では、各言語のコードの書き方を、ユースケース別に、一行ずつ丁寧に解説します。

対象は、各言語を初めて見る方、そして形式証明・定理証明をまったく学んでこなかった方です。

• Lean 4 ── タクティク（intro、rw、induction、simp など）が、証明のなかで何をしているのか
• Rocq ── Software Foundations の定番例を題材に、プログラムの性質の証明を一歩ずつ
• Agda ── 依存型と「穴を掘りながら書く」対話的開発の実際
• Idris 2 ── 型駆動開発。型を先に設計し、実装を型に導かせる書き方
• Isabelle/HOL ── Sledgehammer が証明を自動で見つける様子
• TLA+ ── 分散プロトコルの仕様を書き、不整合状態への到達を検査する

---

おわりに ── 需要は、これから広がるか

最後に、少し先の話をします。

高保証領域の人材ニーズは、これから広がる方向にあると考えられます。ドローンの目視外飛行、自動運転、そして実世界で動く AI エージェント ── これらは人命や社会インフラに関わるため、「テストで大量のケースを通した」だけでは済まない領域を含みます。

ただし、期待しすぎは禁物です。「AI を丸ごと検証して、絶対の安全を証明する」ことは、現状ではできません。 いま形式検証が担えるのは、システムの一部の性質を保証することです。

それでも、自律システムが社会に広がるほど、「この部分は数学的に保証されている」と言える人材の価値は、静かに上がっていくはずです。過大な万能感としてではなく、限定された確実性の担い手として。

そして、第３部で見たとおり、日本で需要が乏しかったのは、基盤層を自国で作る機会が少なかったからでした。

AI の検証という新しい基盤層は、いま生まれつつあります。そこでは、まだどの国も先行を確定させていません。

その入口は、いま無料で開かれています。Natural Number Game を開けば、今日から始められます。

まずは、そこから触れてみてください。

---

参考

数学の最前線での Lean 活用

• ZEN大などによる ABC 予想の Lean 検証（共同通信、2026年7月）：https://news.jp/i/1450775181778223921
• Lean が ACM SIGPLAN Programming Languages Software Award 2025 を受賞：https://dev.to/adolfont/lean-won-the-sigplan-programming-languages-software-award-2025-3gf
• Lean 公式サイト：https://lean-lang.org/

基盤層の形式検証（本記事第２部の事例）

• HACL*／EverCrypt：F* で検証された暗号ライブラリ（TLS 1.3、Mozilla NSS に採用）：https://hacl-star.github.io/
• EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider（IEEE S&P 2020）：https://project-everest.github.io/assets/evercrypt.pdf
• seL4：検証済み OS マイクロカーネル（Klein ほか, Comm. ACM 2010）：https://dl.acm.org/doi/10.1145/1743546.1743574
• CompCert：意味の保存を証明した C コンパイラ（公式）：https://compcert.org/motivations.html
• AWS「Lean Into Verified Software Development」（Cedar の Lean による検証）：https://aws.amazon.com/blogs/opensource/lean-into-verified-software-development/

産業での形式手法の実践

• AWS における TLA+ の活用（S3・DynamoDB・EC2 の設計検証）：https://www.amazon.science/publications/how-amazon-web-services-uses-formal-methods
• Astrée による Airbus 機の飛行制御ソフト検証（開発元 AbsInt 公式）：https://www.absint.com/astree/index.htm
• Astrée と Airbus の実務適用に関する論文：https://www.astree.ens.fr/papers/astree_airbus_sas2007.pdf

安全規格と形式手法

• DO-333「Formal Methods Supplement to DO-178C and DO-278A」（RTCA 公式）：https://www.rtca.org/do-178/
• DO-178C の概要（"DO" は Document の略）：https://en.wikipedia.org/wiki/DO-178C
• DO-178C は FAA・EASA・カナダ運輸省・中国民航局が用いる国際的な認証基準：https://www.ansys.com/simulation-topics/what-is-do-178c
• Common Criteria（EAL6/7 が形式手法を要求。ISO/IEC 15408）：https://www.commoncriteriaportal.org/
• 評価保証レベル EAL の各段階：https://en.wikipedia.org/wiki/Evaluation_Assurance_Level
• ISO 26262（自動車の機能安全規格）：https://www.iso.org/standard/68383.html
• 「車載システム開発における形式手法実践の現状と課題」（計測自動制御学会誌）：https://www.jstage.jst.go.jp/article/isciesci/62/4/62_134/_pdf/-char/ja
• 形式手法の応用事例データベース（三菱総研。JAXA 衛星、自動車 ECU、鉄道制御へのモデル検査適用例）：https://formal.mri.co.jp/db/fmcategory/cat65/

日本の基盤層（本記事第３部）

• ITRON：1984年に坂村健氏が提唱した TRON プロジェクトから生まれた、日本発の組込みOS仕様：https://ja.wikipedia.org/wiki/ITRON
• Camellia：NTT・三菱電機が開発した共通鍵ブロック暗号。国産暗号として初めて IETF 標準・OpenSSL に採用：https://info.isl.ntt.co.jp/crypt/camellia/intro.html

AI × 証明支援系

• Martin Kleppmann "Prediction: AI will make formal verification go mainstream"：https://martin.kleppmann.com/2025/12/08/ai-formal-verification.html
• Lean 4 と AI・幻覚対策の解説（VentureBeat）：https://venturebeat.com/ai/lean4-how-the-theorem-prover-works-and-why-its-the-new-competitive-edge-in
• Lean Copilot（LLM が生成し、証明支援系が検証する neuro-symbolic の構成。arXiv 2404.12534）：https://arxiv.org/abs/2404.12534

仕様の妥当性と、AI に仕様を書かせる試み（本記事第５部）

• From Natural Language to Verified Code（自然言語から Dafny の仕様とコードを生成する研究。「モデルが自明な仕様で検証器を満足させてしまう空虚な検証（vacuous verification）」への対処を明示）：https://arxiv.org/pdf/2604.22601
• Propose, Solve, Verify: Self-Play Through Formal Verification（仕様を生成する側と、実装・証明を生成する側を分けた自己対戦）：https://arxiv.org/html/2512.18160v1
• OSVBench（OS カーネルの仕様生成を LLM に行わせる評価。ハードウェアの振る舞いやメモリ配置など、明示的・暗黙的な前提の多さが困難の中心と指摘）：https://arxiv.org/pdf/2504.20964
• LLMs Gaming Verifiers: RLVR can Lead to Reward Hacking（検証器の「正しさ」の暗黙の前提を突く、意味的に空虚な出力）：https://arxiv.org/pdf/2604.15149
• Towards Understanding Specification Gaming in Reasoning Models（仕様ゲーミングの体系的研究）：https://arxiv.org/html/2605.02269
• 「形式検証が保証するのは仕様に対する正しさであり、人間の意図との一致までは保証しない」（Logical Intelligence の解説）：https://logicalintelligence.com/blog/automatic-formal-verification-for-code-generation

Physical AI の検証（本記事第５部）

• Formal Verification of Neural Network Controlled Autonomous Systems（LiDAR 画像を処理する NN 制御器を、有限状態抽象化と到達可能性解析で検証）：https://arxiv.org/abs/1810.13072
• Scalable and Interpretable Verification of Image-based Neural Network Controllers for Autonomous Vehicles（抽象解釈・到達可能性解析・SMT・MILP の整理）：https://arxiv.org/html/2501.14009
• Formal Verification Techniques for Vision-Based Autonomous Systems（視覚ベース自律系の検証手法の概観）：https://mitras.ece.illinois.edu/research/2024/Vision_survey.pdf

AI エージェントの検証（本記事第５部）

• Type-Checked Compliance: Deterministic Guardrails for Agentic Financial Systems Using Lean 4 Theorem Proving（Harmonic の Aristotle で規程を Lean 4 に自動形式化し、Lean カーネルが証明した行動のみ実行を許す設計。2026年）：https://arxiv.org/html/2604.01483v1
• Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory（エージェントのワークフローと実行軌跡を Lean で三層検証）：https://arxiv.org/pdf/2606.06523
• Toward Pre-Deployment Assurance for Enterprise AI Agents（NN の頑健性検証では、エージェントの振る舞いレベルの性質は対象にできない、という指摘）：https://arxiv.org/html/2606.04037v1
• Neurosymbolic approaches to natural language formalization: what is state-of-the-art?（2026年夏時点の総括。「安全性の担当者はモデルではなくガードレールを検証している」「翻訳工程で意味が漏れる問題は未解決」）：https://blog.icme.io/neurosymbolic-approaches-to-natural-language-formalization-what-is-state-of-the-art/

実務導入のハードル（棲み分け先の記事）

• autotaker 氏「形式手法はなぜ流行っていないのか」：https://qiita.com/autotaker1984/items/52cd65486a3186af080b

学習教材（いずれも無料または公開）

• Natural Number Game：https://adam.math.hhu.de/#/g/leanprover-community/nng4
• Mathlib：https://leanprover-community.github.io/
• Theorem Proving in Lean 4：https://leanprover.github.io/theorem_proving_in_lean4/
• Mathematics in Lean：https://leanprover-community.github.io/mathematics_in_lean/
• Software Foundations：https://softwarefoundations.cis.upenn.edu/
• Programming Language Foundations in Agda：https://plfa.github.io/
• Concrete Semantics：http://concrete-semantics.org/
• Girard, Lafont, Taylor『Proofs and Types』：http://www.paultaylor.eu/stable/prot.pdf

出典についての注記：

本記事の規格・産業に関する記述は、上記の公開情報および各規格の解説に基づいています。

各国の制度・運用、および各ツールの最新状況は変化しますので、正確な情報は各規格の一次資料や公式サイトでご確認ください。

とくに、日本の産業構造に関する第３部の分析は、公開情報からの筆者の推察を含みます。

コード例の構文は公式資料に基づいていますが、バージョンにより細部が異なる場合があります。動作確認はご自身の環境でお願いします。