Loading...
シリーズ： 形式検証 · 全3回中の第3回 対象読者： 初心者。第1回と第2回では形式検証とOrchardのバグを扱いました。この最終回では、2つの考え方が実際のシステムで出会う様子を示します。必要なことは進行に合わせて振り返ります。 この記事で得られること： Zcashが新しい「Ironwood」プールについて実際に何を証明したのか、その証明の構造、対象となる範囲と対象外の範囲、旧プールを安全に廃止した方法、そしてこれが暗号資産を構築する新たな標準を示す理由を正確に理解できます。
第1回では、システムが正しいことを証明するとは何を意味するのかを学びました。第2回では、テストが4年間見逃していた実際の欠陥、つまり無制限の不可視な偽造を許しかねなかった、制約が不十分な楕円曲線乗算を見ました。この記事はその結末です。Zcashが単なるパッチではなく、この種のバグ全体が排除されたことを機械検証済みの証明で示して、どのように対応したのかを説明します。
バグが貨幣を脅かすとき、通常はパッチを当てて先へ進みます。Zcashはさらに野心的なことをしました。2026年7月28日に有効化されたIronwoodという新しいシールドプールとともに、エンジニアたちはLean証明支援系で記述された2,700件超の定理からなる機械検証済み数学的証明を公開し、明示された仮定の下で新プールが偽造コインを作り出せないことを確立しました。証明はオープンソースのironwoodリポジトリで公開されており、3チームの研究者と暗号学者が完了までに1か月以上を費やしました。
これはZcashを超えて重要です。稼働中の金融システムを取り上げ、「偽造なし」が何を意味するかを正確に書き下し、テストが十分だったことを期待するのではなく、それを証明できることを示す、最も明確な実例の一つです。約束を定理へと変えるのです。
第2回は、これを可能にした洞察で終わりました。ここで扱うすべてはこれに基づくため、思い出しておきましょう。
検出不可能な偽造バグは、プロトコルの仕様、すなわち回路が強制すべき内容の数学的記述にしか存在できません。検出可能なものなら公開会計に現れるからです。したがって、仕様の健全性を証明すれば、隠れた偽造バグという類型全体を一挙に排除できます。
なぜ「仕様にしか」存在できないのでしょうか。なぜなら、すべてのブロックには証明を含むすべての取引の完全な内容が恒久的に記録されるからです。ソフトウェアが誤って不正な取引を受け入れたなら、誰でも修正済みソフトウェアで履歴を再実行し、それを確認できます。その証拠は恒久的かつ公開されています。根本の数学における欠陥だけが永遠に隠れられます。照合すべき「正しいバージョン」が存在しないためです。形式検証が対象とするのはこの欠陥です。
テストはサンプル入力に対する挙動を検査しますが、Orchardのバグが隠れたのは、まさにどのサンプル入力もそれに到達しなかったからです。仕様に関する証明は、誰も試そうとは思わない境界事例を含め、すべての入力を同時に対象とします。4年間にわたる不可視の欠陥を自信をもって廃止するには、これほど強い保証が必要です。
この証明は、その下にあるより深い性質から構成された、一つの主要な性質を確立します。
残高整合性： シールドプールに保存される隠匿された価値は、そこへ流入した純粋な公開価値を決して超えません。
これは平易に表した偽造防止の性質です。貨幣はシールドプールに入ることができ（公開可視）、そこから出ることもできます（公開可視）。しかし金額が隠されている内部では、価値を無から生み出すことはできません。検証済みの小さな台帳で具体化しましょう。
5 + 3 = 8相当の入力から4 + 4 = 8相当の出力が生じます。流入価値と流出価値は等しく、残高整合性は保たれます。✓8相当の入力に対し、出力は4 + 4 + 2 = 10です。これは無から2単位を発行することになります。残高整合性はこれを禁じます。プールは、そこへ入った額を超えて支払うことはできません。✗残高整合性は、2番目のシナリオが有効な取引を決して生成できないという数学的な主張です。
残高整合性を保証するため、研究者たちはまずゼロ知識証明システム自体について、より深く微妙な性質を証明する必要がありました。通常の健全性（第2回の「真の命題だけが証人を持つ」）は、興味深い理由からシールドプールには十分ではないことが判明しました。隠された取引には何でも含められるため、ほとんどすべての命題は技術的には何らかの証人を持つからです。そこで研究者たちは、より強い性質を証明しました。
知識健全性： 有効な取引証明を生成できる者は、正しい方法で導出され、正しいアドレスにある実在のコイン、すなわち有効な証人を実際に保有していなければなりません。
このための形式的な道具が抽出器です。これは、検証者を納得させられる任意の証明者から、その実際の証人を取り出せる手続きです。証人を常に抽出できるなら、納得させる証明者は本当にそれを持っていたはずです。第2回の言葉でいえば、知識健全性は、偽の命題を通過させる制約の欠落である健全性ギャップが存在しないという形式的な約束です。これはOrchardのバグに欠けていた性質そのものです。すべての可能な証明者に対してこれが存在することを証明することで、その扉は完全に閉ざされます。
この検証はボタン一つで得られた結果ではなく、本格的な人間の努力によるものでした。
ironwoodリポジトリで公開されています。この性質を論じるため、Leanモデルは台帳全体を取引のリストとして記述します。各取引はアクション、宣言された公開価値、署名を含みます。研究者がValidLedgerと呼ぶ述語は、ネットワークのコンセンサスルールを直接書き起こします。すべてのアクションの証人は必要な条件を満たさなければならず、支出マーカー（nullifier）が二度現れてはならず、参照されるすべてのツリー状態はシステムが真に到達したものでなければならず、すべての署名が検証されなければなりません。次に定理はすべての有効な台帳について量化します。「すべての有効な台帳」という表現こそ要点です。サンプルではなくそのすべてであり、実際の攻撃者が組み立てられるものをすべて包含する上位集合です。
残高整合性の結果は、偽造への各経路が閉ざされていることを示す複数の台帳レベルの定理から組み立てられています。すべての支出が実在する過去の出力に対応すること、総価値が保存されること、受け取ったノートが支出可能なままで盗まれないこと、支出には適切な認可が必要なことを、それぞれ証明します。別の構成要素であるバインディング署名は、各取引の隠れた価値を宣言された公開額に結び付けるため、隠匿会計と公開会計が密かに不一致となることはありません。
微妙で誠実な疑問があります。証明は数学モデルについてのものですが、ネットワークはRustコードを実行します。コードがモデルと一致することを、どう確認するのでしょうか。
チームは、検証者のフィンガープリントと呼ぶ慎重な境界を引きました。境界より上では、Lean証明は検証者を正確な数学的オブジェクトとして扱います。境界の下には通常のRust実装があります。重要な議論は第2回と同じです。
実際のソフトウェアが証明済みモデルから逸脱しうる方法はすべて実装上のバグであり、実装バグが生み出せる偽造は常に検出可能です。受理されたすべての証明は恒久的に記録され、修正済みソフトウェアで再実行できるからです。
したがって、証明は検出不可能な類型（仕様）を扱い、恒久的な公開記録は検出可能な類型（実装）を扱います。この二つの間に、検出不可能な偽造バグが隠れる場所はありません。チームは、実際の検証者を実行し、取得したケースでフィンガープリントを正確に再現することも確認しました。
第1回では、証明はシステムが明示された仮定の下で仕様を満たすことを保証するものであり、「バグが一切存在しない」ことを意味するものではない、と強調しました。Zcashのチームはこの点を見事なまでに正確に扱っており、誠実な教育的文章も同様でなければなりません。
証明はIronwoodの安全性を、標準的で明確に名前が付けられた小さな仮定の集合へと還元します。特に、その健全性はIronwoodが用いる楕円曲線上の離散対数問題の困難性に依存します。これは広く研究された仮定であり、既知の最良の攻撃にはおよそ2^126回の演算が必要で、実現可能な計算能力をはるかに超えます。さらにハッシュ関数に対する標準的なモデリング仮定も必要です。二つの境界を明確に述べる価値があります。
この成果を損なうどころか、こうした境界を明示することが信頼性を生みます。主張は正確です。*標準的な暗号学的仮定の下で、このプールは検出不可能な偽造コインを作り出せません。*これは希望ではなく定理であり、その正確な範囲は公開の場で明示されています。
新しいプールの健全性を証明しても、4年間にわたり欠陥が存在した古いOrchardプールについての疑問は残ります。その過去を隠し直すことはできません。しかし、その将来を制限することはできます。
Zcashはターンスタイルと呼ばれる仕組みを導入しました。ルールは単純かつ強力です。
古いプールから出せる価値は、検証可能にそこへ入った額までに限られます。
シールドプールへの資金流入と流出は公開可視であるため（隠されているのは内部の活動だけです）、ターンスタイルにより、過去に入った額を超えて出ていないことをネットワーク全体が確認できます。古いプール内部で偽造コインが作られていたなら、それらはこの上限に達して外へ出られなくなります。そして正直な資金が移行し、超過分が現れないことで、コミュニティは欠陥が決して悪用されなかったという強い公開証拠を得られます。これはプライバシーを壊さずに私的プールの供給量を監査することに最も近いものであり、Zcashのプライバシーを維持しながら、供給整合性をBitcoinのようなチェーンの透明なモデルに近づけます。
Ironwood自体は修正済みの証明回路を再利用し、空のプールから新たに始まり、将来を見据えた保護も加えています（将来の量子コンピューターが現在の暗号技術を脅かす場合にも、資金を回収可能なままにするための規定を含みます）。新しいシールド活動は現在Ironwoodを通じて流れ、古いOrchardプールは引き出し専用に制限されています。
Ironwoodは、Zcashの構築方法におけるより広い変化の一部です。再帰的証明とRaguというツールキットに基づくTachyonと呼ばれる次世代スケーリングの取り組みは、高保証暗号技術と呼ばれることもある哲学の下で開発されています。これは、機械検証済み形式検証を後付けの作業ではなく、新規の暗号システムを提供する際の標準的な一部として扱う考え方です。
その論理は説得力があります。最先端の暗号技術は、まさに人間の直感が最も弱く、Orchardが示したように、微妙で未検証の境界事例が何年も隠れうる領域です。仕様を証明することは、「すべての可能な入力」に対応し、そのようなギャップを構造的に閉じる唯一の技術です。チームは、時間をかけてこの精査を実装やその先へさらに広げる意向を示しています。この水準は、Zcashの内外でより広く採用されることが期待されます。
分かりやすさのために簡略化しました。実際のLean開発はここでの概略よりはるかに詳細であり、アクション、命題、コミットメント、nullifier、署名の正確な定義を含みます。「残高整合性」と「知識健全性」には、ここでは言葉でのみ述べた厳密な形式定義があります。離散対数の困難性への還元は、いくつかの中間モデル（証明者の代数的モデルとハッシュのランダムオラクルモデル）を経由しますが、ここでは「標準的な仮定」に圧縮しました。また、フィンガープリントとターンスタイルも概念レベルで説明しました。こうしたことは本質的な物語を変えません。「偽造なし」の仕様、すべての有効な台帳に対する機械検証済み証明、範囲と仮定の明示的かつ誠実な記述、そして欠陥のあるプールの安全な廃止です。権威ある説明については、Project Tachyonが公開した検証に関する解説とironwood証明リポジトリを参照してください。
| 用語 | 平易な英語での意味 |
|---|---|
| Ironwood | Zcashの新しいシールドプール（2026年）。欠陥のあったOrchardプールを置き換えるもの |
| Balance integrity | プールが公開可視に流入した価値を超えて支払うことはない |
| Knowledge soundness | 有効な証明には、証明者が本物の証人を保有することが必要 |
| Extractor | 納得させる任意の証明者から証人を取り出す手続き |
| Lean | 検証を機械検査するために使われた証明支援系 |
| ValidLedger | 定理が対象とするコンセンサスルールの形式モデル |
| Fingerprint | 証明済みの数学と稼働中のRustソフトウェアの間の境界 |
| Under stated assumptions | 指定された暗号学的仮定が成り立つ限り証明が成立すること |
| Turnstile | プールの流出を検証可能な預入額で上限設定するルール |
| High-assurance cryptography | 形式検証を標準手順として用いる暗号技術の構築 |
この証明はIronwoodにバグがないことを意味しますか？
いいえ。そのように主張しているわけでもありません。これは明示された仮定の下で、残高整合性という一つの正確な性質を証明します。検出不可能な偽造は排除しますが、考えられるあらゆるバグを排除するものではありません。
この証明は私の取引のプライバシーを保証しますか？
いいえ。この検証は供給の健全性（偽造貨幣がないこと）を対象とし、プール固有のプライバシー保証を対象とはしていません。これらは異なる方法で議論されます。
人間（およびAI）が書いた証明をなぜ信頼できるのですか？
機械検証されるからです。Lean証明支援系がすべてのステップを機械的に検査するため、信頼は各ステップにおける人間やAIの注意深さではなく、仕様と明示された仮定に置かれます。
古いOrchardプールに残っているコインはどうなりますか？
引き出すことはできますが、ターンスタイルにより、検証可能に流入した額までに制限されます。これは供給整合性を保護するとともに、古い欠陥が決して悪用されなかったことを示す助けにもなります。
これで話は終わりですか？
これは終着点ではなく、重要な節目です。Zcashの将来のアーキテクチャ（Raguツールキットを備えたTachyon）は、形式検証を標準的な実践として構築されており、このアプローチをさらに広げていきます。
ある人がこう主張します。「Ironwoodは形式検証済みなのだから、Zcashで何かが間違うことは今後一切不可能だ」。全3回の考え方を使い、この主張が強すぎる理由を二つ挙げてください。(答えは下にあります。)
第一に、この証明は明示された仮定（離散対数の困難性と標準的なハッシュのモデル化）の下で、特定の性質（残高整合性）を対象としています。暗号学的仮定が破られた場合や、仕様化された範囲外で問題が生じた場合（たとえばプライバシー、ウォレットソフトウェア、あるいは未証明の構成要素）には、この証明は何も述べません。第二に、形式検証はシステムが書かれた仕様を満たすことを保証します。仕様自体が現実の要件を何か捉え損ねていたなら、証明は誤った対象を忠実に認証してしまいます。どちらも第1回の注意点を言い換えたものです。証明は正確かつ範囲が限定されており、その範囲が誠実だからこそ強力であって、何も間違わないという包括的な保証ではありません。
全3回を通じて、一般的な考え方から実稼働の応用へと進みました。ソフトウェアをテストするのではなく正しいと証明することの意味（第1回）、制約が不十分な実際の回路がどのように不可視の貨幣を発行し得たか（第2回）、そして残高整合性の機械検証済み証明がそのバグの類型を完全に廃止した方法（第3回）です。一貫するのは一つの誠実な約束です。「バグが一切ない」ではなく、「明示された仮定の下で、この正確な性質があらゆる場合に成り立つ」です。自身の金額を隠す貨幣にとって、それこそが証明する価値のある約束です。
ZecHubのための Formal Verification シリーズの一部です。