Loading...
シリーズ： 形式検証シリーズ · 全3回中 第1回 対象読者： 完全な初心者。数学、プログラミング、暗号技術の知識は前提としません。 この記事を読み終える頃には： ソフトウェアが正しいことを証明するとはどういう意味か、それがテストと根本的にどう異なるか、機械検証済みの証明とは何か、そしてそのような証明が約束できることの正確な（そして誠実な）限界を明確に理解できます。
ほとんどのソフトウェアは、テストされているから信頼されています。多くの入力で実行し、その振る舞いを確認するのです。形式検証は、さらに大胆な問いを投げかけます。誰も試そうと思いつかなかった入力も含め、あらゆる可能な入力に対して、システムが期待どおりに動作することを数学的な確実性をもって証明できるでしょうか？この記事では、その考え方を基礎から築いていきます。まずは直感から。必要になるまで記号は使いません。
これは実話であり、このシリーズが存在する理由でもあります。
2022年、プライバシー重視の暗号通貨Zcashは、Orchardという新しいシールドプールを導入し、金額を隠したまま取引できるようにしました。4年間、完璧に動作し、専門家による監査も繰り返し通過していました。ところが2026年5月、基礎となる数学を注意深く考察したセキュリティ研究者が（AIツールの助けも借りて）、システムの数学にある一箇所の制約不足を発見しました。その一つの欠落により、攻撃者は無制限の偽造通貨を作れた可能性があり、金額は隠されているため、誰にも起きていることは見えなかったでしょう。この欠陥はずっと存在していたのです。
テストによって発見されたのではありません。すべてのテストは4年間通過していました。発見したのは、数学について推論した人でした。そしてチームは修正した際、単にパッチを当てて終わりにはしませんでした。置き換えたものにこの種類の欠陥がまったく含まれ得ないことを示す、2,700個を超える個別の定理からなる機械検証済みの数学的証明を書いたのです。
それが形式検証であり、得られるものは「多くのケースを試してうまく動いた」ではなく、「すべてのケースで成り立つことを証明した」です。一つでも見落としたケースが壊滅的な結果を招くシステム（通貨、航空機、医療機器、暗号技術）では、この違いがすべてです。
テストの盲点は、数十年前に計算機科学者エドガー・ダイクストラが名付けたもので、今も真実です。
テストはバグの存在を示せますが、その不在を示すことは決してできません。
テストが通ったなら、その入力に対してシステムが動作することだけが分かります。試していない入力については何も分かりません。そして危険なバグは、ほとんど常に誰も試していないケースにあります。
あなたが千の扉がある建物を任され、夜にはすべての扉が施錠されていることを保証する役目だと想像してください。
違いは、現実をサンプリングすることと、設計の性質を証明することの間にあります。テストはサンプリングします。形式検証は証明します。それが全体の考え方であり、ほかのすべてはそれを厳密に行うための仕組みです。
どれほど高度な形式検証であっても、正確に3つの要素から成り立っています。これらを明確に押さえれば、残りは詳細です。
| 柱 | 平易な意味 | 建物のたとえ |
|---|---|---|
| 仕様 | 「正しい」とは何を意味するかを正確に記述したもの | 「夜にはすべての扉が施錠されなければならない」 |
| システム | 実際に確認される対象（プログラム、回路、プロトコル） | 建物とその施錠機構 |
| 証明 | システムが常に仕様を満たすことを示す厳密な論証 | 「ロック」を押すと全扉が施錠されることの論理的な実証 |
そして、もう一つ静かな要素が、全体を信頼できるものにします。
名前を耳にする証明支援系には、Lean、Rocq（旧Coq）、Isabelleがあります。これらは実質的に、非常に厳格な論理検査エンジンです。冒頭の話に出たZcashの証明は、Leanで書かれました。特筆すべきことに、現代のAIモデルは人間の指導のもと、これらの証明を書く支援にもますます使われており、以前は何年もかかった作業を数週間に短縮しています。機械はなおもすべてのステップを検査するため、速度向上によって確実性が損なわれることはありません。
「証明」という言葉は威圧的に感じられるかもしれません。そこで、具体的に確認可能な例でその正体を明らかにしましょう。暗号技術ではなく、学校で習う算数だけです。
主張： すべての自然数nについて、和0 + 1 + 2 + ... + nはn(n+1)/2に等しい。
これをテストすることはできます。n = 5なら0+1+2+3+4+5 = 15となり、5 × 6 / 2 = 15です。✓ 一致しています。n = 10も試してみましょう。和は55で、式からは10 × 11 / 2 = 55となります。✓（これらは計算・確認済みであり、実際にこの主張は直接確認すると0から999までのすべてのnで成り立ちます。）
しかし、たとえ千個の値をテストしても、「すべての自然数」に到達することはできません。無限にあるからです。証明は、帰納法と呼ばれる手法を用い、有限の論証によってその無限の隔たりを埋めます。
n = 0では、和は単に0であり、式からは0 × 1 / 2 = 0となります。一致します。✓kについて、式が成り立つと仮定します。次の数k+1を加えます。k+1までの和は(sum up to k) + (k+1) = k(k+1)/2 + (k+1)です。一行の代数計算でこれを(k+1)(k+2)/2に変形でき、これはkの代わりにk+1を入れた式そのものです。✓最初（0）で成り立ち、各ステップが次の数へと成り立つことを引き継ぐため、一つの有限な論証によって、永遠にすべての自然数で成り立ちます。それが証明です。証明支援系もまさにこの推論を行いますが、「一行の代数計算」を含む各ステップが、それまでの内容から本当に導かれることを機械的に検証します。
身につけるべき飛躍はこれです。証明は「無限に多くのケース」を有限で検証可能な論証へ変換します。これはテストが構造上持ち得ない超能力です。
形式検証が強力なのは、そもそもバグがどこから生じるかについて、明確な洞察を与えるからでもあります。ルールを検査するシステムのあらゆる欠陥は、次の3つの場所のいずれかにたどり着きます。
| バグの発生源 | 意味 | 証明によって排除できるか？ |
|---|---|---|
| 仕様 | 数学またはルール自体が間違っている（条件の欠落、不適切な定義） | はい。直接的に可能で、ここが形式検証の主戦場です |
| 実装 | 正しい仕様をコードが忠実に実行できていない | 部分的には可能。こうした失敗はしばしば検出可能な痕跡を残します |
| 破られた仮定 | システム全体が依存する何かが、誤りだと判明する | いいえ。仮定は還元不可能な基礎です |
この分類は見た目以上に重要で、第2回と第3回はこれを軸に展開します。最も深く、最も危険で、永久に隠れうるバグは、仕様に存在しがちです。つまり、システムが何をすべきかという数学的記述です。そして仕様こそ、機械検証済みの証明が直接、すべてのケースを一度に検査できる対象です。だからこそ本格的な形式検証の取り組みは、まずそこを目指します。
形式検証は強力ですが、その約束は正確なものであり、それを誤解すると人は道を誤ります。したがって、慎重に述べましょう。
証明が保証するのは、明記された仮定のもとで、システムが仕様を満たすことだけです。それ以上ではありません。
ここから4つの帰結が導かれ、どれも重要です。
形式検証を弱めるどころか、この正確さこそがその強みです。何が得られるのかを正確に教えてくれます。第3回で見るように、Zcashチームが範囲と仮定を明確に述べること（「これらの名前付き仮定のもと、供給の健全性を証明したのであり、プライバシーは証明していない」）は、その誠実さの模範です。
読みやすくするために単純化しました。実際の仕様は英語の文ではなく正確な形式言語で書かれます。形式検証には、異なる問題に適した複数のスタイル（対話型定理証明、モデル検査、SMTベースの手法）があります。また、AIの支援があっても、これらの証明を書くことは熟練と労力を要する作業です。証明支援系が内部で論理をどのように表現するかも省略しました。これらのどれも、明記された仮定のもとで、仕様、システム、そして両者が一致することを示す機械検証済みの証明という核心を変えるものではありません。必要に応じて詳細に戻ります。
| 用語 | 平易な意味 |
|---|---|
| Formal verification | システムがすべてのケースで仕様を満たすことを、数学的に証明すること |
| Specification | 「正しい振る舞い」とは何を意味するかを正確に記述したもの |
| System | 検査される実際のプログラム、回路、またはプロトコル |
| Proof | すべてのケースにおける主張を確立する、有限な論理ステップの連鎖 |
| Proof assistant / theorem prover | 証明の各ステップを検査するソフトウェア（Lean、Rocq、Isabelle） |
| Machine-checked | 人間が読むだけでなく、コンピュータにより一歩ずつ検証されていること |
| Induction | 最初で真であり、各ステップが次のものへ真であることを引き継ぐ証明手法 |
| Assumption | 証明が依存する条件。偽であれば保証は成り立たない場合がある |
形式検証はテストに取って代わりますか？ いいえ。両者は補完し合います。テストは実用上の問題や誤った仮定を低コストで発見し、検証はテストでは決してサンプリングされないかもしれないバグのクラス全体を排除します。
これほど強力なら、なぜすべてを形式検証しないのですか？ 費用がかかり、専門的なスキルを必要とするからです。ただし、AI支援によりそのコストは下がりつつあります。まれなバグが壊滅的な結果を招くシステムのために使われ、そのような場面こそコストに見合います。
形式検証されたシステムでも失敗することはありますか？ はい。仕様が間違っていた場合、定義が誤って記述されていた場合、仮定が成り立たなかった場合、または失敗が仕様の対象外にある場合です。証明がカバーするのは、主張している範囲だけです。
機械検証済みの証明は、人間による証明より信頼できますか？ 大規模で複雑な証明については、一般にそうです。機械は微妙な欠落を見落としたり、曖昧な説明を受け入れたりしません。ただし、与えられた仕様と定義は依然として信頼します。
AIが証明を書くのを支援するなら、なぜ信頼できるのですか？ 証明支援系がすべてのステップを機械的に検査するからです。AIはステップを提案し、機械がそれを検証します。誤ったステップは単に拒否されるため、AIは保証を弱めることなく作業を高速化します。
銀行のソフトウェアが「口座残高を決してマイナスにしない」ことを証明したとします。1年後も、お金が消え続けています。両方が同時に真であり得るのはなぜでしょうか？ (答えは下にあります。)
証明が保証したのは、残高が決してマイナスにならないという、正確に一つの性質だけです。たとえば資金を誤った（ただし依然としてマイナスではない）口座へ移すバグや、一度も仕様化されなかったシステム部分の欠陥など、その性質がまったく扱わない方法でお金が消えることがあります。検証は約束したことを正確に行い、それ以上は行いません。これは第6節の注意点が実際に現れたものです。証明が対象にするのは仕様であり、「正しい」という考え得るあらゆる概念ではありません。
第2回 · Orchardバグ： 2026年の実話を詳しく見ていきます。あるプライバシーシステムは暗号学的証明によって金額を隠していましたが、その数学の一行が制約不足だったため、それらの証明は嘘をつくように作ることができ、無制限で見えない偽造を可能にしていました。「制約不足の回路」とは正確には何を意味するのか、この種のバグがなぜ永久に隠れ得るのか、そしてなぜこれが一度以上起きているのかを見ていきます。
ZecHubのための Formal Verification シリーズの一部。