Vitalik：イーサリアムの次の段階の鍵は何ですか？

2026.05.20

共有先

TechFlow厳選深潮セレクト

Vitalik：イーサリアムの次の段階の鍵は何ですか？

「コードは法律である」——これはブロックチェーン世界における最も初期の信念の一つである。しかし、もしコード自体にバグが存在する場合はどうなるだろうか？

2026.05.20 - 09:00:03

以太坊

Web3業界の深掘り報道に専念し潮流を洞察

著者：Vitalik Buterin

編訳：佳懽、ChainCatcher

Yoichi Hirai、Justin Drake、Nadim Kobeissi、Alex Hicks の各位より得たフィードバックおよびレビューに特に感謝します。

過去数か月の間に、イーサリアムの最前線における研究開発コミュニティや、その他の多くの計算分野において、新たなプログラミングパラダイムが急速に注目を集めています。それは、EVMバイトコードやアセンブリ言語といった極めて低レベルの言語、あるいはLeanを用いて直接コードを記述し、Leanで自動検証可能な数学的証明を用いてその正しさを検証するという手法です。

適切に実施されれば、このアプローチは単に極めて効率的なコードを生成するだけでなく、従来のプログラミング手法よりもはるかに高い安全性を提供することが可能です。Yoichi Hirai氏はこれを「ソフトウェア開発の究極形態」と呼んでいます。

本稿では、このアプローチの基本原理を明らかにし、ソフトウェアの形式的検証（フォーマル・バーリフィケーション）が何を可能にするのか、またイーサリアムその他の分野において、その弱点と限界がどこにあるのかを探ります。

形式的検証とは何か？

形式的検証とは、コンピュータによって自動的に検証可能な形で数学的定理の証明を記述することを意味します。比較的単純ながらも興味深い例として、フィボナッチ数列に関する基本的な定理を挙げましょう。「3番目ごとの数字は偶数であり、それ以外はすべて奇数である」というものです。

1 1 2 3 5 8 13 21 34 55 89 144 233 377 610 987 1597 2584 …

この定理を証明する簡単な方法は、数学的帰納法を用い、3ステップずつ進めるものです。

まず、基本ケース（ベースケース）から始めます。F₁ = F₂ = 1、F₃ = 2と定義します。観察により、「iが3の倍数のときFᵢは偶数、そうでないときは奇数」という命題がx = 3より前では成立していることが確認できます。

次に、帰納的ケース（インダクティブケース）を考えます。この命題が3k+3より前で成立すると仮定します。すなわち、F₃ₖ₊₁、F₃ₖ₊₂、F₃ₖ₊₃の偶奇性がそれぞれ「奇数」「奇数」「偶数」であると既知とします。このとき、次の3つの数の偶奇性を計算できます：

F₃ₖ₊₄ = F₃ₖ₊₂ + F₃ₖ₊₃ = 奇数 + 偶数 = 奇数
F₃ₖ₊₅ = F₃ₖ₊₃ + F₃ₖ₊₄ = 偶数 + 奇数 = 奇数
F₃ₖ₊₆ = F₃ₖ₊₄ + F₃ₖ₊₅ = 奇数 + 奇数 = 偶数

したがって、命題が3k+3より前で成立することを仮定すれば、それが3k+6より前でも成立することを導くことができます。この推論を繰り返し適用することで、この規則がすべての整数に対して成立することを確信できます。

この議論は人間にとって十分に説得力があります。しかし、100倍も複雑なものを証明したい場合、そして自分がまったく間違いを犯していないことを極めて確実に保証したい場合にはどうすればよいでしょうか？そのような場合、コンピュータが信頼できる証明を提供することができます。

以下に、その具体的な表現を示します：

-- フィボナッチ数列（fib 0 = 0, fib 1 = 1, fib 2 = 1、添字が1だけずれている）
def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n + 2 => fib (n + 1) + fib n

-- 主張：fib (3k+1) は奇数、fib (3k+2) は奇数、fib (3k+3) は偶数。
-- 同等の言い換え：fib 3 から始まる、3番目ごとのフィボナッチ数はすべて偶数。
-- これら3つの主張を同時に、kに関する帰納法で証明する。
-- 次のブロックの各ケースは前のブロックに基づいて構成されるため。
theorem fib_triple (k : Nat) :
    fib (3 * k + 1) % 2 = 1 ∧
    fib (3 * k + 2) % 2 = 1 ∧
    fib (3 * k + 3) % 2 = 0 := by
  induction k with
  | zero => decide
  | succ k ih =>
    -- 新しい添字を(something) + 2の形に書き直し、fibが展開されるようにする。
    refine ⟨?_, ?_, ?_⟩
    · show (fib (3 * k + 3) + fib (3 * k + 2)) % 2 = 1
      omega
    · show (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)) % 2 = 1
      omega
    · show (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)
        + (fib (3 * k + 3) + fib (3 * k + 2))) % 2 = 0
      omega

これは先ほどの「人間向け」の証明と同じ推論を、Leanというプログラミング言語で記述したものです。Leanは、数学的証明の記述・検証に広く用いられる言語です。

この証明は上記の人間向け証明とは異なるように見えますが、その理由は十分に理解できます。コンピュータ（伝統的な意味での「決定論的」プログラム、つまりif/then文から構成されるものであり、大規模言語モデルではない）にとって直感的なものと、人間にとって直感的なものは、根本的に異なるからです。

上記の証明では、「fib(3k+4) = fib(3k+3) + fib(3k+2)」という事実を強調しません。代わりに、「fib(3k+3) + fib(3k+2) は奇数である」という事実を強調しており、Lean内で「omega」と呼ばれる名前の壮大な戦略（タクティク）が、これとfib(3k+4)の定義に関する知識を自動的に組み合わせてくれます。

より複雑な証明では、各ステップでどの数学的法則がそのステップを許容するかを明示的に指定しなければならない場合もあり、Prod.mk.injなど、難解な名前のタクティクを用いることもあります。

一方で、巨大な多項式の式を一括して展開したり、"omega"や"ring"といった一行の命令だけでそれが妥当であることを証明したりすることも可能です。

このような不直感的さと煩雑さこそが、機械検証可能な証明が約60年もの間存在しているにもかかわらず、依然として小規模な分野に留まっている主な理由です。しかし一方で、AIの急速な発展により、かつて不可能と思われていた多くのことが、今や現実のものになりつつあります。

数学的証明がコードを守り始めるとき

これまで読まれてきた方の中には、「コンピュータが数学的定理の証明を検証できるようになった。だから、素数に関する新しい驚くべき結論のうち、どれが真で、どれが百ページにも及ぶPDF論文の中の誤りなのかをついに特定できるようになった」とお考えの方もいらっしゃるかもしれません。

あるいは、望月新一氏によるABC予想に関する主張が正しいかどうかを、ついに判別できるようになるかもしれません！

しかし、単なる好奇心を離れて、それがいったい何を意味するのでしょうか？

この問いに対する答えはいくつかあります。私にとって非常に重要なのは、特に暗号技術やセキュリティに関連するタスクを実行するコンピュータプログラムの正しさを検証することです。

そもそも、コンピュータプログラム自体が数学的対象であり、あるプログラムがある特定の方法で動作することを証明することは、それ自体が数学的定理なのです。

例えば、Signalのような暗号化通信ソフトウェアが本当に安全かどうかを証明したいとしましょう。その文脈における「安全」という概念を、数学的に定義することができます。

高レベルで言えば、ある暗号学的仮定が成立するという前提のもとで、秘密鍵を持つ者だけがメッセージの内容について何らかの情報を得られることを証明しようとしているのです。現実には、非常に多くの異なるセキュリティ属性が極めて重要です。

実際、まさにこの問題に取り組んでいるチームが存在します！彼らの一つのセキュリティ定理は以下の通りです：

theorem passive_secrecy_le_ddh
  (g : G)
  (adv : PassiveAdversary G SK) :
  passiveSecrecyAdvantage (F := F) g adv ≤
    ProbComp.boolDistAdvantage
      (DiffieHellman.ddhExpReal (F := F) g (ddhReduction adv))
      (DiffieHellman.ddhExpRand (F := F) g (ddhReduction adv))

Leanstralによるその意味の要約は以下の通りです：

passive_secrecy_le_ddh 定理は、X3DHの受動的メッセージ秘匿性が、ランダムオラクルモデル下のDDH仮定と同等以上に困難であることを示す緊密な還元（コンパクト・リダクション）です。もし攻撃者がX3DHの受動的メッセージ秘匿性を破ることができれば、DDHも破ることができます。

DDHが破られにくいと仮定しているため、X3DHは受動的攻撃に対しても安全です。この定理は、攻撃者がSignalの鍵交換メッセージを受動的に観測しても、生成されたセッション鍵をランダムな鍵と区別できる確率は無視できるほど小さいことを保証しています。

これをAES暗号化実装の正しさの証明と組み合わせれば、Signalプロトコルの暗号化が受動的攻撃者に対して安全であるという証明を得ることができます。

同様のプロジェクトは、TLSやブラウザ内暗号化の他の部分の実装の安全性も証明しています。

端から端まで完全に形式的に検証を行えば、単にプロトコルの理論的記述が安全であることを証明するのではなく、ユーザーが実際に実行する具体的なコードが実際の運用においても安全であることを証明することになります。

ユーザーの立場からは、これは非信頼性（トラストレスネス）を大きく高めます。コード全体を信頼するためには、コードベース全体をチェックする必要はなく、証明された声明（ステートメント）のみをチェックすればよいのです。

ただし、「安全」という極めて重要な語が実際に何を意味するのかについて、いくつかの重要な大前提を常に念頭に置いておく必要があります。

本当に重要な声明を証明し忘れることは容易です。また、証明すべき声明がコード自体よりも単純な記述を持たないこともしばしばです。

証明の中に、最終的には成立しない仮定をこっそり導入してしまうことも容易です。さらに、システムの一部だけを形式的検証する必要があると判断した結果、他の部分（あるいはハードウェア）に深刻な脆弱性が存在し、それが原因でシステム全体が攻撃を受けることもあり得ます。

Lean自体の実装にもバグが存在する可能性すらあります。しかし、こうした厄介な詳細を議論する前に、まずは形式的検証が理想通りに正しく行われた場合に実現しうるユートピアについて深く掘り下げてみましょう。

セキュリティのために設計された形式的検証

コンピュータコード内のバグは恐ろしいものです。

暗号資産を不変のブロックチェーン上のスマートコントラクトに預け、コードにバグがあれば北朝鮮が自動的にあなたの全資金を奪い去り、あなたが異議を申し立てることさえできないという状況では、その恐ろしさはさらに増します。

それがゼロ知識証明（ZKP）でラップされた場合、バグはさらに恐ろしくなります。なぜなら、誰かがゼロ知識証明システムをハッキングできた場合、彼らはすべての資金を引き出せる一方で、我々には一体何が起きたのかがまったく分からない（さらに悪いことに、いつ起きたかも分からない）からです。

強力なAIモデル（例えば、2年後のClaude Mythos）が、こうしたバグを自動的に発見できるようになれば、コードのバグはさらにさらに恐ろしくなります。

こうした現実に対する一部の人の反応は、スマートコントラクトという基本的な概念を放棄すべきだ、あるいはネットワーク領域そのものが、防御者が攻撃者に対して非対称な優位性を持つ領域になりえないという主張です。

いくつかの引用を紹介します：

「システムを強化するには、攻撃者が脆弱性を悪用するために費やすよりも多くのトークンを、その脆弱性を発見するために費やす必要がある。」

そして：

「我々の業界は、決定論的コードを基盤として築かれている。それを書く、テストする、リリースする、そしてそれが動作することを確信する。しかし私の経験では、この契約はすでに崩れ始めている。」

「AIネイティブ企業のトップ運営者の間では、コードベースはもはや『動作すると信じられる』ものとなり、その成功確率を正確に説明できなくなっている。」

さらに悪いことに、一部の人々は唯一の解決策としてオープンソースの放棄を提唱しています。

サイバーセキュリティにとって、これは暗澹たる未来です。とりわけ、インターネットの分散化と自由を重んじる私たちにとっては、極めて悲観的な展望です。

全体として、サイファーパンク精神は、インターネット上で防御者が攻撃者に対して優位に立つという理念を根本に据えています。すなわち、暗号化・署名・証明といったデジタル「城塞」を築くことは、それを破壊することよりもはるかに容易であるという考え方です。

もし我々がこの優位性を失ってしまえば、インターネットのセキュリティは規模の経済にのみ依存することになり、世界中を駆け巡って潜在的な攻撃者を追跡しなければならず、より広い意味では、支配と破滅の二者択一しか残らないことになります。

私はこれに同意しません。私はサイバーセキュリティの将来について、より楽観的なビジョンを持っています。

強力なAIによる脆弱性探索能力がもたらす課題は確かに厳しいものですが、それは過渡的な課題に過ぎません。一旦塵が落ち、新しいバランスが取れた段階に入れば、我々は過去よりも防御者に有利な環境を得ることになります。

Mozillaも私の見解に賛同しています。彼らの言葉を引用します：

「あなたは他のすべての業務の優先順位を再調整し、この課題に継続的かつ集中した精力を投入する必要があるかもしれないが、トンネルの向こうには光がある。」

「我々のチームがこの課題にどう立ち向かってきたかに、我々は非常に誇りを感じており、他社も同様に行えるだろう。我々の仕事はまだ終わっていないが、最も困難な時期を乗り越え、単に追いつくだけでなく、はるかに素晴らしい未来を垣間見るところまで来ている。」

「防御者はついに決定的な勝利を収める機会を得た。…脆弱性は有限であり、我々はついにそれらすべてを特定できる世界へと入りつつある。」

さて、Mozillaの投稿でCtrl+Fを使って「形式的（formal）」および「検証（verification）」という語を検索すると、マッチする箇所はゼロ件です。サイバーセキュリティの明るい未来は、形式的検証、あるいは他のいかなる単一技術にも完全に依存するものではありません。

では、何に依存するのでしょうか？基本的に、以下の図です：

CVE脆弱性の数の時間的減少傾向

長年にわたり、脆弱性の数の減少を促進してきた技術は多数あります：

型システム
メモリ安全なプログラミング言語
ソフトウェアアーキテクチャの改善（サンドボックス化、権限制御、および「信頼できる計算基盤（TCB）」と「その他のコード」を明確に区別することを含む）
より優れたテスト手法
安全／非安全なコーディングパターンに関する知識体系の継続的拡充
事前に作成・監査済みのソフトウェアライブラリの継続的増加

AI支援による形式的検証は、全く新しいパラダイムと見なされるべきではなく、すでに進行中のトレンドおよびパラダイムを強力に加速するものとして捉えるべきです。

形式的検証は万能ではありません。しかし、目標が実装よりもはるかに単純な場合に特に有効です。これは、イーサリアムの次期主要バージョンで展開される予定の、極めて複雑で難しい技術（耐量子署名、STARK、コンセンサスアルゴリズム、ZK-EVMなど）において、特に顕著です。

STARKは非常に複雑なソフトウェアです。しかし、それが実現する核心的なセキュリティ属性は、理解・形式化ともに容易です：「プログラムPへのハッシュH、入力x、出力yを指す証明を見た場合、(i) STARKで使用されるハッシュアルゴリズムが破られたか、(ii) P(x) = y のいずれかが成立する」ということです。

そこで、完全に形式的に検証されたSTARK実装を作成しようとするArklibプロジェクトが登場しました（VCV-ioは、STARKを含む様々な他の暗号プロトコルの形式的検証に利用可能な基礎的なオラクル計算インフラストラクチャを提供しています）。

さらに野心的なのがevm-asmプロジェクトです。これは、完全に形式的に検証されたEVM全体の実装を構築しようとするプロジェクトです。

ここでのセキュリティ属性はそれほど単純明快ではありません：基本的に、目標は、Leanで書かれた別のEVM実装と等価であることを証明することです。ただし、その実装は、実行効率を一切考慮せず、最大限の直感性と可読性を重視して記述されます。

我々は、互いに証明可能な等価性を持つ10個のEVM実装を得る可能性がありますが、たまたまそれらすべてに同じ致命的な欠陥が含まれており、攻撃者がアクセス権のないアドレスからすべてのETHを引き出すことができるという事態も理論的には起こり得ます。

しかし、これは現在のどこかのEVM実装にそのような欠陥が存在する可能性よりもはるかに低いです。また、我々が苦い教訓を通じてその重要性を理解したもう一つのセキュリティ属性、すなわちDoS攻撃耐性については、仕様化が非常に容易です。

その他の重要な分野は以下の通りです：

ビザンチン耐性コンセンサス：期待されるすべてのセキュリティ属性を形式的に仕様化するのは困難ですが、バグがかつて非常に普遍的であったことを考えると、試みる価値は十分にあります。そのため、Leanによるコンセンサスプロトコルの実装および証明が進行中です。
スマートコントラクトプログラミング言語：VyperおよびVerityにおける形式的検証を参照してください。

これらのすべての場合において、形式的検証がもたらす大きな付加価値の一つは、これらの証明が真正にエンドツーエンドである点です。通常、最も厄介なバグはインタラクションバグであり、独立して検討された二つのサブシステムの境界線上に潜んでいます。

人間にとって、システム全体をエンドツーエンドで推論するのはあまりにも困難ですが、自動化されたルール検査システムはこれを実現できます。

効率性のために設計された形式的検証

evm-asmに戻りましょう。これはEVMの実装です。しかし、それはRISC-Vアセンブリ言語で直接記述されたEVM実装です。

文字通り、そうです。

これはADDオペコードの実装です：

import EvmAsm.Rv64.Program
namespace EvmAsm.Evm64
open EvmAsm.Rv64

/-- 256ビットEVM ADD：2項演算、スタックから2つポップ、1つプッシュ。
  リムブ0：LD, LD, ADD, SLTU（キャリー）、SD（5命令）。
  リムブ1-3：LD, LD, ADD, SLTU（キャリー1）、ADD（キャリー入力）、SLTU（キャリー2）、OR（キャリー出力）、SD（各8命令）。
  その後、ADDI sp, sp, 32。
  レジスタ：x12=sp, x7=acc, x6=operand, x5=carry, x11=carry1。-/
def evm_add : Program :=
  -- リムブ0（5命令）
  LD .x7 .x12 0 ;; LD .x6 .x12 32 ;;
  ADD .x7 .x7 .x6 ;; SLTU .x5 .x7 .x6 ;; SD .x12 .x7 32 ;;
  -- リムブ1（8命令）
  LD .x7 .x12 8 ;; LD .x6 .x12 40 ;;
  ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;
  ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;
  OR' .x5 .x11 .x6 ;; SD .x12 .x7 40 ;;
  -- リムブ2（8命令）
  LD .x7 .x12 16 ;; LD .x6 .x12 48 ;;
  ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;
  ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;
  OR' .x5 .x11 .x6 ;; SD .x12 .x7 48 ;;
  -- リムブ3（8命令）
  LD .x7 .x12 24 ;; LD .x6 .x12 56 ;;
  ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;
  ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;
  OR' .x5 .x11 .x6 ;; SD .x12 .x7 56 ;;
  -- スタックポインタの調整
  ADDI .x12 .x12 32
end EvmAsm.Evm64

RISC-Vが選ばれた理由は、構築中のZK-EVM証明器が、通常RISC-Vの証明を行い、イーサリアムクライアントをRISC-Vにコンパイルすることによって機能するためです。したがって、RISC-Vで直接記述されたEVM実装があれば、これが得られる最速の実装となるはずです。

RISC-Vは、通常のコンピュータ上で非常に効率的にシミュレートすることも可能です（市販のRISC-VノートブックPCも存在します）。

もちろん、真正にエンドツーエンドを達成するためには、RISC-Vの実装（または証明器の算術化）自体を形式的に検証する必要がありますが、心配は無用です。この分野の作業もすでに存在しています。

アセンブリ言語で直接コードを書くことは、50年前によく行われていたことです。以来、我々はこの手法を放棄し、代わりに高水準言語でコードを記述するようになりました。

高水準言語は効率性を若干犠牲にしますが、その代償として、コードを書く速度が格段に速くなり、さらに重要なことに、他人のコードを理解する速度も大幅に向上します。これはセキュリティにとって不可欠です。

形式的検証とAIの結合により、我々は「未来へ戻る」機会を得ました。

具体的には、AIにアセンブリコードを書かせ、そのアセンブリコードが所望の属性を持つことを検証する形式的証明を書くことができます。

少なくとも、所望の属性とは、可読性を重視して、人間にとって親しみやすい高水準言語で書かれた実装と完全に等価であるという単純なもので構いません。

我々は、可読性と効率性の間でバランスを取る単一のコードオブジェクトを必要としなくなります。代わりに、二つの独立したオブジェクトを持つことになります：一つは（アセンブリ実装）効率性のみを最適化し、その実行環境の特定の要件を考慮したもの、もう一つは（セキュリティ声明、あるいは高水準言語実装）可読性のみを最適化したものであり、それらの間の等価性を数学的証明によって保証します。

ユーザーは、この証明を一度（自動的に）検証すればよく、その後は高速版を実行するだけで済みます。

この手法は非常に強力であり、Yoichi Hirai氏がこれを「ソフトウェア開発の究極形態」と呼ぶ理由もここにあります。

形式的検証は万能薬ではない

暗号学およびコンピュータ科学の分野には、形式的手法そのものと同じくらい長い歴史を持つ伝統があります。それは、形式的手法（あるいはより広く、「証明」への依存）を批判する伝統です。

こうした文献には、実際の事例が豊富に含まれています。初期の手書きの暗号学的証明から始めましょう。Menezes氏とKoblitz氏による2004年の批評を引用します：

1979年、Rabin氏はある暗号関数を提案しました。これはある意味で「証明可能」に安全であり、すなわち還元主義的安全性属性を持つものでした。

還元主義的安全性声明とは、暗号文yからメッセージmを復元できる者は、必ずnを素因数分解できる者でなければならないというものです。… Rabin氏がその暗号方式を提案した直後、Rivest氏は皮肉にも、その暗号方式に追加の安全性を与えるはずのこの特性が、別の「選択暗号文攻撃」にさらされた際に、全体を崩壊させてしまうことを指摘しました。

つまり、攻撃者が何らかの方法でAliceに任意の暗号文を復号させることに成功した場合、攻撃者は上記の段落でSamがnの素因数分解を行うために用いたのと同じ手順を踏むことができるのです。

Menezes氏とKoblitz氏はさらに多くの例を提示しています。共通のパターンは、暗号プロトコルをより「証明可能」にしようと設計する試みが、しばしばそれらをより「自然でない」ものにし、設計者がまったく考慮していなかった状況でクラッシュする可能性を高めてしまうという点です。

さて、機械検証可能な証明とコードに戻りましょう。2011年に、形式的に検証されたCコンパイラにバグが存在していたことを発表した論文があります：

我々が発見したCompCertの2番目の問題は、以下のコードを生成する2つのバグに由来します：stwu r1, -44432(r1)。これは大型のPowerPCスタックフレームを割り当てています。

問題は、16ビットのオフセットフィールドがオーバーフローしている点にあります。CompCertのPPCセマンティクスでは、この即値幅の制限は規定されておらず、彼らはアセンブラが範囲外の値を検出すると仮定していました。

また、2022年の論文もあります：

CompCert-KVXでは、コミットe2618b31が「nand」命令が「and」として出力されるというバグを修正しました。「nand」は極めて稀な~(a & b)パターンでのみ使用されます。このバグは、ランダムに生成されたプログラムをコンパイルすることで発見されました。

そして、今日、2026年において、Nadim Kobeissi氏がCryspenの形式的に検証されたソフトウェアの脆弱性について述べています：

2025年11月、Filippo Valsorda氏が独立してlibcrux-ml-dsa v0.0.3において、同一の決定論的入力が与えられた場合に、異なるプラットフォーム上で異なる公開鍵および署名を生成することを報告しました。

このバグは、SHA-3のKeccak-f置換で使用されるXAR操作を実装する内部関数_vxarq_u64ラッパー関数に存在します。フォールバック機構がシフト操作に誤った引数を渡しており、ARM64プラットフォームでハードウェアSHA-3サポートがない場合にSHA-3ハッシュ値を破損させました。

これはタイプIの障害に該当します：この内部関数はマークされていましたが、NEONバックエンド全体には、実行時安全性または正しさの証明が完了していませんでした。

そして：

libcrux-psqライブラリは、耐量子型の事前共有鍵プロトコルを実装しています。decrypt_outメソッドにおいて、AES-GCM 128の復号パスが復号結果に対して.errorを伝播させる代わりに.unwrap()を呼び出しています。不正な形式の暗号文によってプロセスがクラッシュします。

以上の4つの問題は、以下の2つのタイプのいずれかに属します：

（検証が非常に困難であるため）コードの一部のみが検証された場合。その結果、未検証のコードが著者たちが想定していたよりも多くの（そしてより致命的な）脆弱性を含むことが判明した。
証明すべき重要な属性を規定し忘れた場合。

Nadim氏の記事には、形式的検証の失敗パターンの分類が含まれています。彼は他のタイプの失敗パターン（例えば、「形式的仕様自体が間違っている、あるいは証明に、構築されたシステムが黙認する偽の声明が含まれている」）も提示しています。

最後に、ソフトウェアとハードウェアの境界における形式的検証の失敗を見てみましょう。ここでよく見られる問題の一つは、サイドチャネル攻撃に対する耐性の検証です。

メッセージを保護するための完全に安全な暗号方式を持っていても、数メートル離れた人が電気信号の変動を捉えて数十万回の暗号化操作の後にあなたの秘密鍵を抽出できれば、あなたは依然として安全ではありません。

これは「差分電力解析（DPA）」に関する資料で、現在では十分に理解されているこのような技術の一例です。

差分電力解析はサイドチャネル攻撃の一般的なタイプの一つ。出典：ウィキペディア

このような攻撃者に対する安全性を証明しようとする試みは常に存在しています。しかし、そのような証明には、攻撃者を数学的にモデル化する必要があり、それに対して安全性を証明できる必要があります。

時折、「d検出モデル（d-probe model）」が用いられます：攻撃者が回路内で照会できる位置の数に既知の制限があると仮定します。しかし、このモデルでは捉えきれない漏洩の形態も存在します。

この記事で観察されているように、よくある問題は「遷移的漏洩（transient leakage）」です：ある位置の値だけでなく、その値の変化を反映する信号を観測できる場合、通常これは、単一の値ではなく、新旧の二つの値から必要な情報を回復するのに十分な情報量を提供します。

この記事は、その他の漏洩形態の分類も提示しています。

数十年にわたるこうした形式的検証への批判は、形式的検証をより良いものへと進化させてきました。過去と比べて、我々は現在、こうした問題を防ぐことにずっと長けています。しかし、今日においても、それは完璧ではありません。

全体を俯瞰すると、一つの主な筋があります。形式的検証は強力です。

しかし、マーケティング用語がいかに形式的検証を「証明可能な正しさ」のように聞こえさせるとしても、この「証明可能な正しさ」は、根本的にソフトウェア（あるいはハードウェア）が「正しい」ということを証明するものではありません。

大多数の人間が理解する「正しい」という意味は、およそ「物事が、ユーザーが開発者の意図をどのように理解しているかに合致して動作すること」に相当します。

そして「安全」という意味は、およそ「物事がユーザーの期待に反して、ユーザーの利益に反する行動を取らないこと」に相当します。

この二つの場合において、「正しさ」と「安全性」は、いずれも数学的対象と人間の意図あるいは期待との比較に帰着します。

人間の意図と期待も技術的には数学的対象ですが、人間の脳も宇宙の一部であり、十分な計算能力があればシミュレート可能な物理法則に従うためです。

しかし、それらは信じられないほど複雑な数学的対象であり、コンピュータも我々自身も、それらを理解することも、読み取ることもできません。

実用上、それらはブラックボックスであり、我々が自分自身の意図や期待について何らかの理解を持っているのは、ただ単に、各自が自分の思考を長年にわたり観察し、他人の思考を推論してきた経験があるからにすぎません。

そして、我々が原始的な人間の意図をコンピュータに押し込めることができない以上、形式的検証は人間の意図との比較を証明することができません。

したがって、「証明可能な正しさ」と「証明可能な安全性」は、実際には、我々人間が理解する「正しさ」と「安全性」を証明しているわけではありません。人間の脳を完全にシミュレートできるようになるまでは、どんなものもそれを実現できません。

では、結局それは何の役に立つのか？

私は、テストスイート、型システム、形式的検証のすべてを、プログラミング言語の安全性という同じ基本的なアプローチの異なる実装形態（おそらく唯一合理的なアプローチ）と見なしています。

これらはすべて、私たちの意図を異なる方法で冗長に仕様化し、それらの異なる仕様化が相互に整合しているかどうかを自動的にチェックすることについてのものです。

以下のPythonコードを例に挙げましょう：

def fib(n: int) -> int:
  if n < 0:
    raise Exception("Negative values not supported")
  elif 0 <= n < 2:
    return n
  else:
    return fib(n-1) + fib(n-2)
if __name__ == '__main__':
  assert [fib(i) for i in range(10)] == [0, 1, 1, 2, 3, 5, 8, 13, 21, 34]
  assert fib(15) == 610

ここで、あなたは意図を三つの異なる方法で表現しています：

明示的に、コード内にフィボナッチ数列の公式を実装することによって
暗黙的に、型システムを用いて（入力、出力、および再帰的な中間ステップがすべて整数であると指定することによって）
「サンプルパッケージ（sample package）」方式、すなわちテストケースを用いて

ファイルを実行すると、公式とサンプルが照合されます。型チェッカーは型の整合性を検証できます：二つの整数を加算することは許容される操作であり、その結果は別の整数となります。

型システムは物理学における宿題の検査に似ています：加速度を計算しているのに、答えの単位がm/s²ではなくm/sとなっていたら、何かを間違えたと分かるでしょう。

テストケースは、「サンプルパッケージ」定義の具体例であり、人間にとって、概念を扱う際に、これは直接的な明示的定義よりもはるかに自然な方法です。

あなたの意図を、理想的には異なる思考スタイルを要求する、できるだけ多くの異なる方法で仕様化できれば、それらすべての表現が相互に整合していることが証明された時点で、あなたが本当に望んでいるものを実際に表現できている可能性は高まります。

安全なプログラミングとは、意図をさまざまな方法で表現し、それらの表現がすべて相互に整合していることを自動的に検証することである。

形式的検証により、この手法をさらに一歩進めることができます。形式的検証を用いれば、意図をほぼ無限に多くの異なる冗長な方法で仕様化でき、プログラムはそれらすべてが整合している場合にのみ検証を通過します。

高度に最適化された実装と、効率性は極めて低いが人間にとって読みやすい実装を両方仕様化し、それらが一致することを検証できます。また、あなたの友人10人に、あなたのプログラムが満たすべき数学的属性のリストを提出してもらい、それがすべて満たされているかをチェックすることもできます。

満たされていない場合は、プログラムが間違っているのか、あるいは数学的属性の定義が間違っているのかを特定します。さらに、AIを用いれば、こうしたすべての作業を極めて効率的に行うことができます。

では、どうやって始めればよいのか？

現実的に考えて、あなた自身が証明を書くことはありません。形式的手法が普及しなかった主な理由は、ほとんどの人がこうした難解な記述の書き方を理解できないからです。以下のコードの意味をあなたは説明できますか？

  /-- ヘルパー：アキュムレータを伴うfoldlレベルでのpointwise ≤。-/
private theorem foldl_acc_le (ds1 ds2 : List Nat) (w : Nat) (a b : Nat) (hAcc : a ≤ b)
    (hLE : Forall₂ (· ≤ ·) ds1 ds2) :
    List.foldl (λ acc d => acc * w + d) a ds1 ≤
    List.foldl (λ acc d => acc * w + d) b ds2 := by
  match ds1, ds2, hLE with
  | [], [], .nil => exact hAcc
  | d1::ds1', d2::ds2', .cons hd htl =>
    simp [List.foldl]
    refine foldl_acc_le ds1' ds2' w (a * w + d1) (b * w + d2) ?_ htl
    exact Nat.add_le_add (Nat.mul_le_mul hAcc (Nat.le_refl _)) hd

（ご参考までに、これはSPHINCS署名の一種の特定のセキュリティ声明の証明に含まれる、多くの補題（サブレマ）の一つです。

具体的には、この声明は以下の通りです：ハッシュ衝突が発生しない限り、あるメッセージの署名は、他の任意のメッセージの署名よりも、少なくとも一つのハッシュ階段上でより高い値を必要とし、したがって、その他の署名からは計算できない情報を含む。

手動でコードと証明を書く代わりに、AIにプログラム（Leanで直接書くか、あるいは速度を重視してアセンブリで書くか）を生成させ、その過程で任意の所望の属性を証明させればよいのです。

このタスクの利点は、それが自己検証的であるという点にあります。したがって、あなたが監督する必要はなく、AIに数時間連続して実行させればよいのです。

最悪の結果としては、AIが原地で止まって何も進展しない（あるいは、私のleanstralがそうしたように、作業負荷を軽減するために、証明すべき声明を勝手に置き換えてしまう）ということだけです。

最後にあなたが確認すべき唯一のことは、AIが証明した声明が、あなたの要件に合致しているかどうかです。

SPHINCS署名のバリエーションでは、最終的な声明は以下の通りです：

theorem wots_fullDigits_incomparable
  {dig1 dig2 : List Nat} {w l1 l2 : Nat}
  (hw : 0 < w)
  (hLen1 : dig1.length = l1) (hLen2 : dig2.length = l1)
  (hBound1 : ∀ d ∈ dig1, d < w) (hBound2 : ∀ d ∈ dig2, d < w)
  (hL2suff : l1 * (w - 1) < w ^ l2)
  (hNeq : dig1 ≠ dig2) :
  ¬ Forall₂ (· ≤ ·) (wotsFullDigits dig1 w l1 l2) (wotsFullDigits dig2 w l1 l2) ∧
  ¬ Forall₂ (· ≤ ·) (wotsFullDigits dig2 w l1 l2) (wotsFullDigits dig1 w l1 l2)

これは実際には、何とか読み取れるギリギリのラインにあります：

あるハッシュ摘要（dig1）から生成された数字が、別のハッシュ摘要（dig2）から生成された数字と等しくないならば、

以下の二つの条件はどちらも成立しない：