イーサリアム共同創設者のヴィタリック・ブテリン氏は、新たなプログラミング言語を提案した。これは、形式的証明支援ツールであるLeanやHOLに直接コンパイルされる構想である。
この提案は、AI出力の読み取りにおける特定のギャップを狙うもの。人工知能は現在、手作業では人間が書くよりもはるかに速く、大規模な自動証明を生成する。しかし、こうした証明が何を主張しているのか、すぐに確認できる読者はほとんどいない。
AI証明を読むためだけの言語
Leanとは、数学者やエンジニアが、コンピューターが一行ごとにチェックできる証明を書くために用いるソフトウェアである。イーサリアムの研究者も、暗号コードやコンセンサスロジックの検証にすでに利用している。証明支援ツールは約60年前から存在するが、依然としてニッチな分野にとどまっている。
ブテリン氏は自身の投稿で、証明の内部ステップには数学的に正しいこと以外に必要条件はないと主張した。読者がそれらの証明過程を直接確認することはない。定義や定理は別で、人間はそれを読んでソフトウェアの保証内容を把握する。
ブテリン氏は5月のブログ記事でも、同様のテーマを考察している。そこでは、効率的な低水準コードが可読性の高い仕様と合致することを数学的に証明し、1回のレビューで両者を同時に保証する。
こうした提案はイーサリアム自体の再構築、いわゆるLean Ethereumロードマップとも連動している。研究者らは同時に、同様の手法で形式検証済みZK-EVM（ゼロ知識証明可能なイーサリアム仮想マシン）の構築にも取り組んでいる。
AIが証明を作成し、人間が主張を確認
大規模言語モデルはすでに、実用的なLean証明を生成できる。ブテリン氏は、ClaudeやDeepseek 4 Proのほか、Lean専用に調整された小規模モデルLeanstralを有効なツールとして名指しした。実例としてevm-asmという、可読性の高い参照仕様で検証されたEVM実装がある。この能力は、ブテリン氏のAIチャレンジで開発者が示した推論力とも一致する。テスターはこの課題を数時間で解決した。
しかし重要性は利便性だけにとどまらない。セキュリティ研究者は、今年に入りAI支援型エクスプロイト（悪用）試行の増加を特定している。形式的に証明されたコードは、それらへの防御の1つになる。より親しみやすい仕様言語があれば、開発者は証明の詳細を読むことなく主張内容の監査が可能となる。
イーサリアム研究界の枠を超えて
ブテリン氏は最近、ゼロ知識証明を活用した匿名掲示板のデモンストレーションを実施するなど、こうしたアイディアを公開の場で試し続けている。このデモは、検証可能な主張が研究用途から実際のプロダクトに移行可能であることを示した。研究者らもコンセンサスクライアントのLeanによる形式検証を開始し、早期段階のバグ発見を目指している。
それでも、方針は一貫している。高速なコードと可読性の高い主張を切り離し、その一致を証明する流れである。
新言語のプロトタイプは現時点で存在せず、ブテリン氏も詳細な構文は明らかにしていない。開発者が標準仕様に集約するのか、複数の非互換方言が並存するのかが今後の焦点となる。どちらの道を取るかが、AI検証済みコードの実用化速度を左右する可能性がある。
