イーサリアム、Lean 4を用いたコンセンサス検証を進展

プロジェクト概要

イーサリアムの研究チームは、Lean 4の証明補助ツールを使用してFulu、Gloas、Hezeアップグレードのコンセンサス仕様を実装し、数学的に検証する重要なプロジェクト「Etheorem」に取り組んでいます。この取り組みは、複数のクライアントが同じ仕様を異なる方法で解釈することによって発生するチェーン分裂のリスクを軽減することを目指しています。

Etheoremの目標

Etheoremの主な目的は、イーサリアムのコンセンサス仕様をLean 4で機能的に実装し、単なるコードテストを超えてコアロジックを数学的に検証することです。このプロジェクトは、イーサリアムプロトコルフェローシップ（EPF）とインビジブルガーデン研究チームによるイーサリアム研究フォーラムへの投稿を通じて進捗を公開しています。

技術的実装

Etheoremは、3つのアップグレードに対するコンセンサス仕様を成功裏に実装しました。状態遷移とフォーク選択ロジックを実行でき、公式のイーサリアムコンセンサステストベクターと結果を比較しています。アップグレードの主な特徴は以下の通りです：

• Fulu: データ可用性サンプリングに関連する仕様。
• Gloas: 実行ペイロードオークション構造（ePBS）に関する要素。
• Heze: インクルージョンリスト構造を通じた検閲抵抗を目指す機能。

検証技術

このプロジェクトは、コンセンサスデータのシリアル化、デシリアル化、およびマークルツリー計算に必要な重要な特性を検証するために、SSZ（Simple Serialize）ライブラリであるSizzLeanを利用しています。検証は、シリアル化されたデータが元の値に戻るかどうか、異なる値が同じエンコーディングを共有しないこと、エンコーディングサイズが事前定義された制限を超えないことを確認します。

この取り組みは、検証環境と実行環境の両方で同じ仕様定義を使用することにより、検証されたコードと実際の実行コードの間の不一致を減少させることにも焦点を当てています。ただし、この形式的検証はイーサリアムクライアントエコシステム全体を置き換えるものではなく、テストベクターに合格することが運用の安定性や正式リリースの準備を保証するものではないことに注意が必要です。プロジェクトは将来的に証明の範囲を拡大する計画です。