形式的検証

CryptoBriefingによると、イーサリアム財団の研究者ジャスティン・ドレイクは11月3日に、leanVMがエンドツーエンドの形式的検証を実現したと発表しました。leanVMは、ハッシュベースの後量子署名を効率的に集約し、マルチシグネチャをコンパクトな証明にパッケージ化するための極めてシンプルなzkVMです。性能面では、leanVMは毎秒1000回以上のleanXMSS集約を処理できます。leanXMSSは、コンセンサス層でBLSに代わるハッシュベースの署名スキームとして計画されています。Devcon 8では、ドレイクはイーサリアムの完全な後量子安全への移行目標を2028年12月に調整し、移行に必要なネットワークフォークのためのスペースを確保します。この計画は、leanVM、leanXMSS、leanSpecの3つのオープンソースプロジェクトに依存しており、イーサリアム財団はオープンソースの実装を開発し、形式的検証を進めています。また、Poseidon Prizeなどのインセンティブを通じて革新を促進しています。報道によれば、leanVMの形式的検証はコードが仕様に準拠していることを証明しましたが、2028年12月は目標であり、約束ではありません。

イーサリアムの機関プライバシー技術機関 EthSystems は、そのプライバシープール（shielded pool）について、文書化された仕様から Sepolia テストネットでのバイトコードの実行までの形式的検証を完了したことを発表しました。検証は層ごとに異なるツールを使用して行われました：モデル、回路、ハッシュには Lean を、契約には Halmos と Kontrol を、ウォレットには Aeneas と Verus を、検証者とデプロイにはバイト単位の再構築による照合を使用しました。二重支払いと価値保存は Lean 定理機械によって検証されました。検証中に6つの問題が発見され、そのうち3つは検証ツール自体に起因していました。チームは同時に依存している仮定を列挙しました：ハッシュの衝突がないこと、検証者が偽造証明を拒否すること、契約の動作がモデルと一致すること。

OpenAI は最近、同社の AI モデルがコンピュータサイエンスにおいて20年以上続いている推測指数時間仮説、英語の略称 ETH を解明したと発表しましたが、これはイーサリアムではありません。この仮説は、特に計算が難しい問題がどれほど難しいかに焦点を当てており、ブール充足可能性問題 SAT を例に挙げています：与えられた論理条件のセットに対して、すべての条件が同時に成立するような割り当てが存在するかどうか。問題の規模が大きくなると、既知の最良の方法は基本的に可能な解を一つずつ試すしかなく、時間のコストは規模に対して指数的に増加します。指数時間仮説はさらに、この種の問題は本質的に大幅に加速できず、真の意味での亜指数時間効率的なアルゴリズムは存在しないと主張しています。この仮説は1999年に提唱されて以来、理論計算機科学の重要な基盤となっており、多くの論文がそれに基づいて特定の問題が非常に難しいことや、特定のアルゴリズムが最適に近いことを証明しています。もし指数時間仮説が覆されると、ほとんど不可能と考えられている多くの問題に対して、理論的にはより良い解法が存在するかもしれません。OpenAI は、そのモデルが k-SAT 問題の解の数を亜指数時間内で正確に統計する決定論的アルゴリズムを見つけ、Lean を用いて形式的に検証したと主張しています。この結果が最終的に専門家の審査に耐えられるなら、指数時間仮説を直接揺るがすことになります。

人工知能会社 Anthropic の Frontier Red Team は 10 月 22 日に研究を発表し、大規模な形式的証明を自動的に作成できる大規模言語モデルが存在することを示しました。チームは Theorem と協力し、Claude を使用して RISC-V アセンブリレベルで 100 以上の実際のオープンソースライブラリの安全性を証明し、これは AI を用いてアセンブリレベルで生産ソフトウェアに対して大規模な形式的検証を行った初めての事例であると述べています。証明の過程で、数年にわたり発見されていなかった脆弱性も発見されました。実験では、Google OSS-Fuzz に既に存在するコンパイル可能なファズテストを仕様に変換しました：単一スレッドの静的バイナリ、固定メモリ予算、RISC-V CPU および Linux などの仮定の下で、64 MB 未満の任意の入力に対して、プログラムは正常に終了し、メモリ安全性エラーやアサーション失敗を引き起こさないべきです。数週間以内に、Claude は発見された問題を修正した後、123 の OSS-Fuzz ライブラリの 239 のエントリポイントに対して上述の性質を証明しました。証明はコンパイル後の RISC-V 命令に対して行われ、約 1.8 億行の Rocq によってチェックされました。ページでは、これらのライブラリに脆弱性がないことを意味するものではなく、残りの問題は信頼されたコンポーネントや証明の範囲外にある可能性があると述べています。ページではさらに、チームが Claude に RFC 1950 を形式化させ、x86 バイナリレベルで Linux カーネル内の zlib 実装がその仕様に準拠していることを証明させたと述べています。また、Rust で書かれた Python の大部分をカバーするインタプリタは、170 万以上のランダム生成プログラムと CPython の動作が一致する割合が 99.95% であることを示しました。36 の小規模な検証タスクにおいて、Opus 5.5 はその半分に必要なトークンが Opus 5 より約 40% 少ないことを証明しました。チームは同時に、証明が単一スレッド、静的リンクの RISC-V バイナリに対して行われ、証明チェッカーが仕様が現実に適合しているかどうかを判断できないことを指摘しました。

孫宇晨賞の公式発表によると、この賞の最初の受賞者は9月19日に正式に14日間の公示に入った。現在の公示題目は題庫第305、371、381、526、866、1001号であり、その中で305、371、381号の問題の候補者は形式的検証者、866、1001号の候補者は数学問題解決者、526号は両方の役割を持つ。公示情報は公式GitHubの候補登録表で公開されており、一般の人々は正式な挑戦を提起することができる。孫宇晨賞は、世界初の問題リストに基づくゼロトラストの非中央集権的学術報奨メカニズムであり、最高単題賞金は100万ドルである。設立当日に最初の66の数学問題が発表され、最高賞100万ドルはOpenAI研究チームに授与され、その「三次元ナビエ–ストークス方程式の存在性と滑らかさの問題」に対する解決成果と形式的証明を称賛するものである。同時に、賞の運営者は賞金プールのブロックチェーン上のアドレスを公開し、1000万ドルが預け入れられた。公示期間終了後、賞金はUSDT（TRC20）またはUSDC（ERC20）で支払われ、受賞者には証明書とメダルも授与される。

Zcash 開発チームは、近日発表予定の新しいプライバシープール Ironwood を通じて、形式的検証を導入し、数学的証明によって「検出不可能な増発の脆弱性」のリスクを排除する計画を発表しました。以前の情報によると、Orchard シールドプールに存在する脆弱性は修正され、利用された証拠はありませんが、理論的にはチェーン上の履歴を通じて隠れた増発が発生したかどうかを確認することができないため、コミュニティは全く新しい Ironwood シールドプールを導入し、そのプロトコルに対して全面的な形式的検証を行うことを決定しました。

ZEC 財庫会社 Cypherpunkは X プラットフォームで ZEC トークン市場の変動に応じて発表し、すべてのソフトウェアには脆弱性が存在すると述べ、歴史的にビットコインは誤って「多くの」1,840 億 BTC を鋳造したことがあると指摘しました。しかし、これはブロックチェーン技術を放棄すべきだということではなく、形式的検証と証明可能な正確性を通じて安全性を強化すべきだとしています。Cypherpunkは、AI 技術の発展に伴い、脆弱性検出がより迅速かつ広範囲に行われるようになると強調しましたが、重要なのは悪意のある行為者よりも早く問題を発見できる人が誰であるかです。Zcashは、今後発表される更新を通じてこの能力を示すことができます。以前の報道によると、プライバシーコイン ZEC は無限増発を引き起こす可能性のあるセキュリティ脆弱性が発覚し、市場での売りが発生し、コイン価格は一時的に1日で50%以上下落しました。

ヴィタリック・ブテリンは、ブロックチェーンのセキュリティ分野における形式的検証（Formal Verification）の応用の展望について考察を発表しました。記事では、イーサリアムの最前線の研究開発において、新しいパラダイムが登場しており、EVMバイトコード、アセンブリ、またはLeanを直接使用してコードを記述し、Lean内で自動的に検証可能な数学的証明を用いてその正確性を検証することが指摘されています。研究者のヨイチ・ヒライは、このパラダイムを「ソフトウェア開発の最終形態」と呼んでいます。ヴィタリックは、AI支援の形式的検証がコードの効率と安全性を同時に向上させる可能性があり、特にSTARK、ZK-EVM、耐量子署名、コンセンサスアルゴリズムなどの安全なコアモジュールに適していると考えています。記事はまた、形式的検証が万能ではなく、証明範囲の不完全さ、仕様の誤り、ハードウェアのサイドチャネルなどの問題により失敗する可能性があることを強調しています。将来的には、ソフトウェアが「安全コア」と「非安全エッジ」に分化する可能性があり、イーサリアムは重要な安全コアの一つになるでしょう。

AptosはXプラットフォームで発表し、Aptosは動的スケジューリング形式的検証をサポートする最初のL1であり、設計通りに動作することを数学的に証明できると述べています。Aptosは、AIが仕様を作成し、その正確性を数学的に証明することができ、Move Proverはオラクルであり、これは市場と機械の信頼層です。

ChainCatcher のメッセージによると、CertiK の公式情報によれば、CertiK はアリババグループの革新的なオープンソースクロスプラットフォーム信頼実行環境（TEE）HyperEnclave の高度な形式的検証を完了しました。報告によると、アリババグループの信頼できるネイティブ技術チームは、オープンなクロスプラットフォームソフトウェア信頼実行環境 HyperEnclave を開発し、アリババグループのプライバシー保護計算ワークロードの効率と互換性を向上させることを目的としています。