原文
Mechanized Proofs for Atomic Cross-Domain State Synchronization — jay-oraclizer (2026-06-02)
はじめに
ある資産が複数のドメインに同時に存在する場合、その状態はそれらのドメイン間で何らかの形で「結合」されている必要があります。この投稿で扱うのは、その結合が単なる観察ではなく、「因果的」でなければならないケースです。あるドメインで有効になった状態遷移が別のドメインに到達しなかった場合、その間の期間は市場と規制当局の両方にとって未定義の領域となり、2つのドメインは同じ資産を2つの異なる事実として扱い始めます。既存のクロスドメインメッセージングインフラストラクチャ（クロスチェーンブリッジ、データオラクル、オンチェーン/オフチェーンコネクタ）は、「2つの独立した単方向チャネル」を介して動作するため、中間状態は「構造的に」到達可能です。**この投稿が形式化するのは、その中間状態が定義上到達不可能な同期モデルです。**つまり、2つのドメインの状態遷移が「単一の因果単位」に結合される、「アトミックな」同期のモデルです。
この軸は価格オラクル軸とは直交します。価格オラクルは「観測された値」を扱います。その値をより信頼最小化したり、より遅く、より異議申し立て可能にしたりする改善は、「その数値が何であるか」という観測の安全性を高めます。ここでの主題は観測された値ではなく、「効果」です。あるドメインで有効になった状態遷移が、同じ力で同時に別のドメインでも有効になるかどうかです。価格オラクルをどれほど安全にしても、それは「値が何であるか」に答えるだけです。効果が2つのドメイン間で同時に発生するかどうかは、別の保証です。価格情報の不一致とは異なり、「効果」の不一致は市場自体を分裂させます。あるドメインがある事実の効果を受け入れる一方で、別のドメインがそれがまだ起こっていないかのように取引を続ける場合、その間の期間はまさにアービトラージウィンドウになります。効果が発生する事実は、同時に反映されるか、全く反映されないかのどちらかでなければなりません。
これは私たちの主張ではなく、国際的な規制基準が明示している要件です。FATF勧告16（トラベルルール）は、取引情報が資産の移動と「共に移動」することを要求しており、2025年までに、117の管轄区域のうち85がその法案を可決し、さらに14が進行中です。FATFは、仮想資産は本質的にボーダーレスであるため、ある管轄区域での規制上の失敗が世界的な結果を生むという公式見解をとっています。BIS-IOSCO PFMI原則8（決済の最終性）は、最終決済を「取り消し不能かつ無条件の転送」と定義しています。この定義に照らして読むと、分散型台帳の「確率的決済」（フォークによる取り消しの可能性）は、この基準と矛盾します。PFMIは分散型台帳を対象とした文書ではありませんが、その最終決済基準は、ドメイン間の効果の転送が「取り消し不能かつ無条件に」反映されるという要件として読み取れます。2つの分野（AMLと市場インフラ）は、異なる出発点から、最終的に同じ特性を要求しています。アトミックな同時強制です。「状態の因果的結合」が、この投稿が扱う本当の問題です。
この問題は2つの側面で分かれます。「安全性」：同期が正しく実行された場合、結果の状態はすべてのドメインで一貫しているか？「活性」：ビザンチンノードを含む分散環境で、同期は「実際に進行するか」？システムは停止を回避し、資産が永続的なロックに陥らず、リクエストが無期限に遅延しないか？
この投稿は、2つの側面を単一のモデルに結びつけ、Isabelle/HOLで機械的に証明した結果を共有します。主題は「アトミックなクロスドメイン状態同期」であり、コンセンサス層は、この同期が必要とする「活性保証のための運用エンジン」としてのみ現れます。より正確には、安全性証明が仮定する「正直なノード」がビザンチン環境下で「無条件に」解除できることを示す作業です。副次的な結果として、「リーダーベースのBFTコンセンサスの活性」は、機械的証明で扱われることがめったにありませんでした（HotStuff、Tendermintファミリー、およびそれらに基づく多くのL2シーケンサー設計が普及しているにもかかわらず）。この研究は、その小さな成果物に1つのケースを追加します。しかし、この投稿の主な主題はアトミックな状態同期そのものです。
完全な成果物はIsabelle/HOL 2025-2で3,215行にわたって構築されており、sorry/oopsはゼロです。結果はarXiv:2604.03844プレプリントとして公開されており、GitHubリポジトリ（Oraclizer/formal-verification）で直接確認できます。統合されたAFPエントリCross_Domain_State_Preservationはレビュー中で、2026-05-09の改訂版はビルドを通過しています。
* * *
1. 問題
クロスドメインの状態整合性は、あらゆるマルチチェーン、L2、またはL3の設計者が「暗黙的に依存している」ものの、ほとんど誰も「形式的に述べていない」特性です。2つのロールアップがメッセージを交換するとき、一方の側で有効になった状態遷移が他方に反映されるのは「いつ」、どのような保証の下ででしょうか？共有シーケンシングの下で、2つのドメインが単一の状態を同時に変更するとき、中間状態は何であり、それを観測する第3のドメインは何を信じるべきでしょうか？これらの疑問は、クロスチェーンブリッジ設計、共有シーケンシング、およびロールアップ間のアトミックな構成の根底にありますが、それらはほとんど実装上の慣行として扱われ、「定理の形では述べられていません」。この投稿の出発点は、その特性を明示的な記述にまで高めることです。
この問題は、資産が複数のドメインに同時に存在する「あらゆるシナリオ」で発生します。上記の純粋なインフラストラクチャの例を超えて、金融資産では、資産の「因果的な状態遷移」が発生するあらゆる場所に潜在的な不一致点があります。清算、凍結、満期時の権利行使、デリバティブ決済、KYCステータス更新、規制措置の執行、資産クラス再分類、トークンのバーンとリリースなどです。このセクションでは、「2つの代表的なシナリオ」を通じて問題の構造を示します。どちらも金融資産を使用しますが、その構造は上記のロールアップ間の状態遷移と同一です。
問題をより具体的に見てみましょう。同じ資産 a が2つのドメイン D₁ と D₂ に「結合された形式」で存在するとします。「結合された」とは、各側の a の状態が他方に「反映」されなければならないことを意味します。どのような意味で反映されるのでしょうか？価格情報のように「値」だけが一致すればよいのでしょうか、それとも「アクションの効果」も一致しなければならないのでしょうか？
代表的なシナリオ1、同時清算。 資産 a は2つのドメインで担保としてロックされています。価格が下落し、両方で清算トリガーに達しました。清算が「アトミックに」実行されない場合、D₁ の清算が D₂ の清算の直前に決済され、スリッページが発生するか、保護された清算人が両側で清算を競い合います。これは「価格情報の不一致」ではありません（価格は両方のドメインで同じでした）。不一致は「効果のタイミング」で発生します。
代表的なシナリオ2、規制による凍結。 資産 a は2つのドメインでトークン化されています。ある管轄区域の規制当局が a に対するFREEZE命令を発行します。D₁ ではFREEZEが反映され取引が停止しますが、D₂ ではまだ反映されていません。その期間中、D₂ でのすべての取引は「法的効果」と「システム状態」の間にギャップが生じます。FATFトラベルルールおよび各国のAML規制の観点からは、これはコンプライアンス上のリスクです。
2つのシナリオの共通構造は1行に集約されます。
2つのドメインの状態遷移は、単一の因果単位に結合されなければならない。
この条件が破られないことを保証することが、アトミックな同期の定義です。既存のデータオラクルはこの要件を満たすことができません。 データオラクルの主なシナリオは「単方向の観測」（価格フィード）です。双方向配信が可能であっても、それは「2つの独立した単方向チャネル」であり、「因果的に結合された双方向同期」ではありません。各方向が独立したイベントとして扱われるため、一方が成功し、他方が失敗する中間状態は「構造的に到達可能」です。
この研究が形式化するのは、その中間状態が定義上到達不可能な同期モデルです。 私たちはこれを「アトミックなクロスドメイン状態同期」（双方向、因果的に結合された、アトミック）と呼びます。
問題は2つの側面に分けて分析されます。
安全性：同期が正しく実行された場合、結果の状態はすべてのドメインで一貫しているか？これは「条件付き」のステートメントです。同期が「正しく実行される」という仮定の下でのみ成立します。
活性：ビザンチンノードを含む分散環境で、同期は実際に進行するか？つまり、システムは停止を回避し、資産が永続的なロックに陥らず、正直なリクエスト（市場アクションも規制アクションも同様）が無期限に遅延しないか？
先行研究はどちらか一方を扱っています。LochbihlerとMarićのMerkle Functorパターン（FMBC 2020）は、Canton分散型台帳内の「単一ドメイン、単方向のデータ整合性」をIsabelle/HOLで形式化しました。Velisarios（ESOP 2018）はCoqでPBFTの安全性を検証しましたが、活性は範囲外でした。Carrら（NFM 2022）はAgdaでHotStuffの安全性を検証し、明示的に「活性は特定のインプリメンテーションに関する証明に委ねる」と述べています。Wannerら（SRDS 2020）は、Isabelle/HOLで「Heard-Ofモデル」ベース（リーダーレス）のログ複製プロトコルの安全性と活性を検証しました。
この研究は、上記の先行研究とは2つの点で区別されます。(i) 単一のロケール階層内で、クロスドメイン、双方向、マルチドメイン、および資産ごとの分離された「アトミックな」状態同期を扱います。(ii) リーダーベースのBFTの機械的証明として活性を扱い、安全性証明の正直なノードの仮定を「解除」します（仮定-保証推論）。この2番目の貢献の重みは、「同期と非同期の難しさ」にあるのではありません。同期仮定は、このモデルの意図された抽象化の選択です（§8）。重みは、「検証された特性の性質」にあります。一般的なBFT活性検証が扱わないのは、「アクション優先順位の決定性」（2つの競合するリクエストのうちどちらが最初に処理されるかがすべての正直なノードで同一であること）と、その優先順位が資産ごとの分離とどのように連動するかを機械的証明で結合した方法です。一般的なコンセンサスが扱う「誰が次のブロックを構築するか」という問題と、このモデルが必要とする「競合するアクションのどちらが最初に有効になるかが決定論的に固定されているか」という問題は異なる特性であり、後者は別のロケールとして形式化する必要がありました。これが、一般的なBFTコンセンサスがそのまま使用されない形式的な理由でもあります。
* * *
2. システムモデル
システムを次のように抽象化します。ドメインは4つ組で定義されます。有限状態集合 S、有限アクション集合 A、決定論的遷移関数 δ: S × A ⇀ S、および終端状態述語 terminal: S → bool です。ドメイン識別子の集合 D 上の「マルチドメインシステム」では、各ドメイン d ∈ D が独自の4つ組を持ち、各資産識別子 id に対して「接続されたドメインのサブセット」 connected(id) ⊆ D が定義されます。
この抽象化は意図的に「最小限」です。ドメインがEVMチェーンであろうと、L2 ロールアップであろうと、非ブロックチェーン台帳（例えば、DAML/Cantonのようなエンタープライズ台帳）であろうと、4つ組を満たす限りモデルに入ります。これが、続く「7つの汎用ロケール」の再利用性の基盤となっています。
ビザンチン環境仮定は、標準的なBFT仮定 f < n/3 （つまり n ≥ 3f + 1）です。モデルは「同期メッセージ配信」を仮定します。部分同期モデルへの拡張は未解決の問題として残されています（§8）。
* * *
3. 安全性: クロスドメイン状態保存
ここから、投稿は適切な形式モデルに入ります。モデル内では「状態保存」という用語を使用します。これは、「状態同期の順方向マップが満たすべき数学的条件」を指します。つまり、同期の1つの単方向ステップが、2つのドメイン間の「順方向準同型」であり、状態機械間の「構造保存準同型」（標準的な代数的な意味で）であることを意味します。双方向合成は、このセクションの後半でsymmetric_state_preservationによって扱われます。
安全性部分はState_Preservation.thy（370行、4つの汎用ロケール）にあります。4つのロケールは次のように階層化されています。
locale state_machine =
fixes states :: "'s set"
and actions :: "'a set"
and transition :: "'s ⇒ 'a ⇒ 's option"
and terminal :: "'s set"
assumes finite_states: "finite states"
and finite_actions: "finite actions"
and terminal_subset: "terminal ⊆ states"
and terminal_absorbing: "⟦ s ∈ terminal; a ∈ actions ⟧ ⟹ transition s a = None"
and transition_closed: "⟦ s ∈ states; a ∈ actions; transition s a = Some s' ⟧ ⟹ s' ∈ states"
and transition_domain: "s ∉ states ⟹ transition s a = None"
locale state_preservation =
source: state_machine states⇩s actions⇩s transition⇩s terminal⇩s +
target: state_machine states⇩t actions⇩t transition⇩t terminal⇩t
for states⇩s ... and states⇩t ... +
fixes state_map :: "'s ⇒ 't"
and action_map :: "'a ⇒ 'b"
assumes state_map_well_defined: "s ∈ states⇩s ⟹ state_map s ∈ states⇩t"
and action_map_well_defined: "a ∈ actions⇩s ⟹ action_map a ∈ actions⇩t"
and terminal_preservation: "s ∈ terminal⇩s ⟹ state_map s ∈ terminal⇩t"
-- the naturality / homomorphism condition:
and naturality:
"⟦ s ∈ states⇩s; a ∈ actions⇩s; transition⇩s s a = Some s' ⟧
⟹ transition⇩t (state_map s) (action_map a) = Some (state_map s')"
and naturality_none:
"⟦ s ∈ states⇩s; a ∈ actions⇩s; transition⇩s s a = None ⟧
⟹ transition⇩t (state_map s) (action_map a) = None"
state_preservationロケールの核心は、2つの「異なる」状態機械間の保存関係です。あるドメインのステップが別のドメインのステップに「どのように」対応するかです。この対応は、以下の可換関係によって正確に捉えられます。
ここで φₛ は状態マップ、φₐ はアクションマップです。左側は「ソースでステップし、ターゲットにマップする」であり、右側は「ターゲットにマップし、それからステップする」です。2つの結果が一致することが保存条件です。 これは単一ステップの保存を定義します。
重要な定理が続きます。
定理
sequential_preservation。 単一のステップが保存される場合、任意の長さのアクションシーケンスも保存される。
これは、「単一ステップの保存」が「パスの保存」にリフトされることを示しています。証明はアクションリストに対する帰納法によって行われ、ステップケースはロケールのnaturality仮定によって解除されます。
state_preservationの上にさらに2つのロケールが積み重なります。
symmetric_state_preservationは、2つのドメイン間の「双方向保存」を定義します。順方向マップ φ と逆方向マップ ψ の合成がラウンドトリップ恒等性となる構造です（これは以下の状態マップに適用され、同様にアクションマップにも適用され、ソースとターゲットの両方のラウンドトリップが対象となります）。
このラウンドトリップ恒等性が成立する場所を明確にしておく価値があります。双方向恒等性は、2つのドメインの状態およびアクションの語彙が対応する領域で成立します。2つのドメインが異なるアクション「タイプ」を使用する場合（以下のescalation_preservationインスタンスのように、ソースが規制アクションのエスカレーションサブセットであり、ターゲットが別の独立したアクションタイプである場合）、それは「全単射ラウンドトリップ」ではなく「単方向保存」として扱われ、symmetric_state_preservationレベルではなくstate_preservationレベルに属します。つまり、双方向ラウンドトリップは、2つの表現が情報損失なしに相互に変換される場合の保証であり、2つの語彙が完全に一致しない場合は、その部分についてのみ順方向保存が述べられます。onchain_daml_bridgeインスタンスは前者（対応する語彙領域）に属します。
これは、LochbihlerとMarićのMerkle Functorパターンがインスピレーションとなった点です。Merkle Functorは「単方向」の認証データ構造でしたが、この研究は「双方向保存」を汎用ロケール階層内の独立したフレームワークとして形式化します。2つのフレームワークの直接合成（Merkle FunctorをIsabelleにインポートし、このモデルと合成すること）は、この投稿の範囲外であり、将来の課題として残されています。
multi_domain_preservationは、任意の有限ドメイン集合 D 上で2つのことを同時に扱います。「接続されたドメイン間の整合性」と「未接続ドメインの分離（資産ごとの分離）」です。2つの主要な定理：
定理
cross_domain_consistency。 資産idに対してsync_allが正常に完了した場合、connected(id)内のすべてのドメイン d は同じコンセンサス状態を反映する。
定理
sync_isolation。 ある資産の同期は、すべてのドメイン上の他のすべての資産を変更しない。
sync_isolationは、Merkle Functorパターンには「なかった」保証です。単一ドメインの整合性では、「別の資産の保存」という概念自体が未定義です。マルチドメイン設定では、ある資産に対する同期が別の資産に影響を与えないという保証が定義に含まれなければなりません。
8つの解釈が汎用ロケールの範囲を示す
4つのロケールはすべて汎用です。それらが「実際に意味のあるドメインで動作する」ことは、8つの具体的な解釈によって示されます。
| 解釈 | ロケール | 意味 |
|---|---|---|
| reg_sm | state_machine | 規制状態遷移（単一チェーン） |
| reg_state_machine | state_machine | マルチチェーンインスタンス |
| escalation_preservation | state_preservation | 異なるアクションタイプを持つ2つのチェーン間の保存。ソース = 規制アクションのエスカレーションサブセット、ターゲット = 別の独立したアクションタイプ |
| forward_layer_preservation | state_preservation | オンチェーン列挙型 → オフチェーンパーミッションモデル |
| backward_layer_preservation | state_preservation | オフチェーンパーミッションモデル → オンチェーン列挙型 |
| onchain_daml_bridge | symmetric_state_preservation | 順方向 + 逆方向合成 = ラウンドトリップ |
| multi-domain instance | multi_domain_preservation | 規制状態のNドメイン整合性 |
| dq_priority | priority_system (§4) | コンセンサスメッセージ優先順位 |
これらのうち、escalation_preservationは「異種型クロスチェーン保存」のケースを形式化します。2つのドメインのアクションタイプがまったく同じであるケース（同種アクション）は既存のモデルで処理できますが、「2つのドメインが異なるアクションタイプを使用する」ケース（ここでは、ソースが規制アクションのエスカレーションサブセットを使用し、ターゲットが別途定義されたアクションタイプを使用する）には、別のロケールインスタンスが必要でした。
onchain_daml_bridgeは、この研究が「EVM ↔ 非EVM」境界を扱うケースです。順方向マップはオンチェーン規制状態列挙型をオフチェーンパーミッションモデルに送信し、逆方向マップはその逆であり、その合成がラウンドトリップ恒等性を満たすことを形式的に証明しました。これは、DAML/Cantonのようなエンタープライズ台帳を「オフチェーン側のインスタンス」として扱う研究です。
* * *
4. ビザンチン障害下での活性
活性部分はPriority_Resolution.thy（407行、3つの汎用ロケール）とDQuencer_Instance.thy（解釈）にあります。このセクションでは、§3の安全性で「仮定された正直なノード」が、ビザンチン環境 f < n/3 の下で「どのように解除されるか」を扱います。
3つの汎用ロケールの骨格：
locale priority_system =
fixes priority :: "'m ⇒ 'k::linorder"
assumes priority_injective:
"⟦ priority m1 = priority m2 ⟧ ⟹ m1 = m2"
locale deadlock_free_locking =
fixes timeout :: nat
assumes timeout_positive: "timeout > 0"
locale fair_leader_system =
fixes leader_at :: "nat ⇒ 'n"
and is_honest :: "'n ⇒ bool"
and pending :: "nat ⇒ nat"
and fairness_bound :: nat
assumes fairness_bound_positive: "fairness_bound > 0"
and fair_leader:
"∀epoch. ∃e. epoch ≤ e ∧ e < epoch + fairness_bound ∧ is_honest (leader_at e)"
and honest_progress:
"⟦ is_honest (leader_at e); pending e > 0 ⟧ ⟹ pending (Suc e) < pending e"
and non_honest_bounded:
"pending (Suc e) ≤ pending e"
これら3つのロケールから以下の定理が導出されます。
定理
select_highest_deterministic。 単射優先順位を持つメッセージの集合において、最高優先順位の選択は決定論的である。同じ候補セットを見る2つの正直なノードは同じ決定に達する。
定理
deadlock_freedom。 タイムアウトが正の場合、ロックは永遠に保持されない（lock_eventually_expires）。
定理
eventual_completion。 リーダーローテーションが公平な環境（任意のエポックウィンドウ内で正直なノードが少なくとも一度はリーダーになる）では、正直なノードによってキューに入れられたすべてのリクエストは「有限時間内」に処理される。
3つの定理はすべて汎用です。それらはドメインが何であるかとは独立しています。
安全性仮定の解除
この研究の核となる構成は、「安全性証明が仮定する正直なノード」が「活性証明によって解除される」ことです。仮定-保証推論として表現すると：
安全性は、正直なノードによって同期が実行された場合にvalid_state_preservationを証明します。この「正直なノードの仮定」は、単一のドメイン内では解除できません。ビザンチン環境仮定は、本質的に「コンセンサス層」の特性です。
活性証明は、「f < n/3」の下でのコンセンサス結果の決定性と進捗を直接証明します。つまり、「同期がコミットされた場合、それはコンセンサス多数によって選択された同期であり、その決定は決定論的である」ということです。これは、安全性証明の正直なノードの仮定をBFT仮定で置き換えることに相当します。
したがって、2つの証明の合成は、条件付き安全性を無条件の保証に昇格させます。 DQuencer_Instance.thyの結合された定理は、これを定理形式で述べています。
定理
combined_safety_liveness。 資産が存在し（asset_exists）、有効な状態遷移が定義され（reg_transition s action = Some s'）、資産がロックされておらず（¬ is_locked）、接続されたドメインセットが有限であると仮定すると、グローバル状態が有効であれば（valid_state gs）、同期は成功し（sync source action aid gs = Some gs'）、結果の状態もグローバルな有効性不変条件を保存する（valid_state gs'）。決定性（dq_select_highest_deterministic）、デッドロックフリー（dq_deadlock_freedom）、およびスターベーションフリー（dq_starvation_bound）は、同じエントリ内で個別の定理として確立されており、これらが結合されて、上記の安全性不変条件が正直なノードの仮定なしにビザンチン環境下で成立する基盤となる。
* * *
5. 本研究の数学的基盤
本研究が依拠する数学的原則は3つの系統に分類されます。
第一に、「代数準同型」です。§3のstate_preservationロケールの可換条件、δₜ(φₛ(s), φₐ(a)) = φₛ(δₛ(s, a)) は、まさに2つの状態機械間の「演算保存マップ」の定義です。この形式の目的は、2つのドメインの遷移の「対応」だけでなく、その「構造」を保存することです。
第二に、「圏論のファンクター」です。準同型の一般化である「ファンクターマップ」は、このエントリの「学術的地位」を決定します。このエントリは現在、4つの汎用ロケールと8つの解釈の形で「準同型とその姉妹構造」を形式化しています。ファンクター法則（恒等性の保存、合成の保存）が形式的証明を伴う場合、エントリは「証明可能に」ファンクターの地位を獲得します。この投稿は、その正当化の前の段階の結果を扱っています。
第三に、「仮定-保証推論」（Misra-Chandy 1981）です。これは、§4で活性が安全性証明の正直なノードの仮定を解除する構成の論理的基盤です。「条件付き保証の合成から無条件の保証を得る」ことは、分散システム検証の標準的な論理です。
これら3つの原則が、このエントリの構成を支えています。圏論、代数、分散システム検証論理がすべて1つのモデル内で動作するというのが、本研究の「方法論的性格」です。
* * *
6. ツール選択と7つの汎用ロケールの再利用性
本研究におけるIsabelle/HOLの選択は、擁護する必要があるものではありません。検証対象が(i)状態遷移の抽象構造、(ii)分散システムの進捗特性、(iii)多層合成であることを考えると、ロケールモジュール性と分散システム検証における豊富な前例を持つツールは自然な選択です。本研究の4つのロケールからなる安全性階層は、LochbihlerとMarićのMerkle Functorパターンと「同じツールと同じ方法論（ロケールモジュール性）」に従いながら、「異なる抽象化軸」（データ構造の整合性 vs. 状態遷移の保存）を選択しており、姉妹結果と言えます。
隣接する先行研究との距離には、もう1つの側面があります。「アトミックコミット」自体は新しいものではありません。2PC、3PC、アトミックスワップ、HTLCは数十年にわたってこの問題に取り組んでおり、ここでの貢献は「コミットプロトコルの発明」ではありません。既存のアトミックコミット文献がコミットプロトコルの正しさを扱っているとすれば、本研究の区別は、それを基盤として3つのことを単一のモデルで機械的証明として結合する点にあります。すなわち、「双方向状態保存」（順方向マップと逆方向マップの合成が恒等性であること）、「資産ごとの分離」、および「ビザンチン活性」です。単方向アトミックコミットは最初の2つを必要としません。つまり、その区別は「何をするか」（アトミック同期）ではなく、「それが成立する保証を形式的証明によってどこまで結合するか」にあり、この組み合わせを形式化するケースは、私たちの知る限り、存在しません。
7つのロケールは、このモデル外でも再利用可能です。
| ロケール | 適用可能なドメイン |
|---|---|
| priority_system | MEV（最大抽出可能価値）バンドル優先順位、マルチチェーンブリッジリレーメッセージ順序付け、分散タスクスケジューラ |
| deadlock_free_locking | 分散DB行レベルロックタイムアウト（CockroachDB、TiDB）、DeFi HTLCタイムアウト |
| fair_leader_system | Tendermint、HotStuffにおけるスターベーションフリー |
| state_preservation + multi_domain_preservation | 双方向DBレプリケーション、分散キャッシュ整合性、ステートチャネルのオンチェーン/オフチェーン同期 |
上記の適用可能性は「主張」であり、「証明された事実」ではありません。各アプリケーションには個別の解釈の努力が必要です。この投稿では、「その解釈の努力がどのようなものか」の小さなサンプルとして、escalation_preservation（異種型クロスチェーン）とdq_priority（typedefワークアラウンドパターン）を提示しました。後者は、サブロケールパターンを介してロケールパラメータに対するtypedef制約を回避するケースであり、パターン自体が汎用ロケールフレームワークの再利用性の小さなサンプルです。
* * *
7. L2 / クロスドメイン設計への影響
この形式的証明は、ツールレベルでいくつかの設計原則を「示唆」します。私たちは「示唆する」と書きます。なぜなら、形式的証明はモデル内で定理を確立しますが、「モデルが現実のどの部分に対応し、どの程度の忠実度を持つか」は別の探求領域だからです。このセクションは、後者の探求を議論に供する意図で書かれています。
(a) 双方向クロスドメイン同期は、単方向の2倍ではない。 単方向同期のみを扱うモデルは、「ラウンドトリップ恒等性」という追加の保証を必要としません。双方向の場合、順方向と逆方向の合成は恒等性でなければならず、これには「構成可能な抽象化」が必要です。symmetric_state_preservationロケールはその構成可能性をカプセル化します。
(b) 資産ごとの分離は、モデルの第一級の存在であるべき。 Merkle Functorパターンには「資産ごとの分離」という概念がありません。なぜなら、単一ドメインの整合性では、他の資産の存在自体がモデルの範囲外だからです。マルチドメイン設定では、「ある資産に対する同期が別の資産に影響を与えない」という保証が定義に含まれなければなりません。sync_isolation定理がこれに対応します。
(c) 安全性と活性の組み合わせは、階層化アーキテクチャによって解決される。 このモデルでは、状態同期層とコンセンサス進捗層が「異なるロケール階層」に存在します。2つの層の定理は、仮定-保証によって合成されます。これは、コンセンサスを仮定解除ツールとして扱う方が、形式的証明にとって、コンセンサスアルゴリズムを統一モデルに引き込むよりもクリーンであるという観察です。
(d) 副次的な効果としての構造的OEV（オーダーフロー抽出可能価値）封じ込め。 このモデルの同期パターンは、アトミックな「バインド → 検証 → コミット」サイクルで構成されます。このサイクル内では、「抽出可能な情報非対称性の時間窓」は、定義上、
サイクルの内部はアトミックであるため、「ティック間の間隔」という概念は存在しません。これは「発生封じ込めアプローチ」であり、既存の価格オラクルに限定されたOEV軽減メカニズム（発生したOEVを「再分配する」もの）とは構造的に異なります。この投稿では、このセクションでのみ言及しています。OEV分類、離散的 vs. 連続的更新モデルの抽出ウィンドウ関数、およびコンセンサス優先順位シーケンシングからの分離については、別のトピックで完全に扱います。
* * *
8. 仮定と限界
この証明はモデル内で成立するものであり、実装によって自動的に保証されるものではないことを強調します。 以下の仮定は、検証を回避するために隠されているわけではなく、「明示的な抽象化の選択」です。特に、同期メッセージ配信と公平なリーダーローテーションの仮定は、リーダーベース、ラウンドベースの分散コンセンサス検証（Heard-Ofモデルファミリー、Charron-Bost & Schiper 2009; Wanner et al. SRDS 2020）の確立された方法論的伝統の中にあり、その伝統では同期/公平性の仮定は「活性を記述可能にするモデリングデバイス」であり、結果を無意味にする抜け穴ではありません。また、部分同期への一般化は「より困難な、別の問題」であること（§9 Q1）も認識しており、本研究はその一般化を主張するものではありません。
安全性に関する仮定:
- 同期メッセージ配信。部分同期モデル（メッセージ遅延、再配信、再順序付け）への拡張は未解決の問題です。
- 正直なノード（安全性のみ）。この仮定は、本研究では活性証明によって解除されます。
- 有限ドメインセット。動的ドメイントポロジー（ランタイムでの参加/離脱）はこのモデルの範囲外です。
活性に関する仮定:
- ビザンチン f < n/3。クォーラムベースBFTの標準仮定です。
- 公平なリーダーローテーション。どのノードも無限にリーダーになるという仮定です。VRFベースの実装におけるランダム性仮定と同等です。
- 閉鎖システム（リクエスト到着が有限/有界）。オープンシステム（連続的な到着）におけるスターベーションフリーは将来の課題です。
共通:
- モデルから実装への洗練は、本研究の範囲外です。モデルレベルの定理が実際のコードレベルでどのように成立するかを検証することは、別のトラックとして計画されています。本研究では、その洗練トラックが最も自然に位置するツールと構成パターンに関する決定を保留します。
この領域の境界をどこに引くかについて、Vitalikの形式検証に関する投稿（2026-05-18）が強調しているように、仮定を隠さないことが形式的証明の基礎です。
* * *
9. 未解決の疑問
この投稿が「答えを持っていない、または部分的な答えしか持っていない」問題です。このセクションは質問であり、主張ではありません。
Q1. 部分同期ネットワークモデルへの一般化。 このモデルは同期メッセージ配信を仮定しています。部分同期モデルに一般化する場合、7つのロケールのうちどれを変更する必要がありますか？fair_leader_systemはかなり自然に一般化できるように見えますが、multi_domain_preservationのsync_allはより微妙です。
Q2. 異種コンセンサス体制の合成。 このモデルは、すべてのドメインが同じコンセンサス体制に従うことを仮定していません（ドメイン識別子のみが固定されています）。それでも、ドメイン間で「異種コンセンサス体制」の「合成」に関する保証（例：あるドメインはPoS、別のドメインはPoA、さらに別のドメインは非ブロックチェーン台帳）は、このモデルから直接導出することはできません。この合成には他に何が必要ですか？
Q3. 同期強度の異質性。 この研究は「単一強度」のクロスドメイン状態同期を証明しています。実際には、各資産が必要とする同期強度は異なります。一部の資産は単方向観測のみを必要とし、一部は双方向結合を必要とし、一部（例：規制措置の対象）は必要性として「アトミックな結合」を要求します。同じシステム上で「異種強度」の資産を「分岐」させながら、各資産が必要とする強度が「保証される」という記述をどのように最もよく形式化するかは、現在探求している方向です。§3の保存マップの上に、強度間の還元関係（より高い強度がより低い強度を安全に含む）がどのような構造をとるべきかについて、分散システムと型理論の両方からの視点を歓迎します。
Q4. モデルから実装への洗練のための最も自然な構成パターン。 モデルレベルの定理をコードレベルの洗練に引き下げる際に、「構成コスト」が最も低いツールは何ですか？候補ツール（Coq + MathComp、Lean 4、Creusot/Kani、F*）間の相互運用可能な構成パターンの事例は蓄積されていません。
Q5. 何を検証すべきか（仕様の問題）。 この研究は状態保存を「可換準同型」として定義しました。しかし、クロスドメイン設定では、「正しい同期」の仕様自体が自明ではありません。2つのドメインの時間モデルが異なる場合（ブロック高 vs. 壁時計時間 vs. 論理時計）、誰の時計の下でhappened-before関係を定義すべきでしょうか？どの特性が検証する「価値がある」のか、そして検証可能だが「無意味な」（自明に真であり、何も排除しない）特性はどれか？これはツールに関する問題ではなく、「モデリングの問題」です。汎用ロケールが実際に意味のあるドメインで動作することを確認する過程で、この区別の実践的な重要性を経験しました。しかし、「クロスドメイン同期の正しい仕様とは何か」という一般理論は、この分野でより多くの形式化事例が蓄積されるにつれて初めて明らかになるでしょう。このトピックがその蓄積の出発点の一つとなることを願っています。
上記の質問は、このトピックのフォローアップ作業と学術出版で段階的に扱われる予定です。しかし、私たち自身の答えよりも、「コミュニティからの追加的な視点」がこのトピックの最大の資産になると信じています。
* * *
10. 結び
このトピックが共有したのは、形式的証明の完了報告書ではなく、共有可能な検証資産です。 7つの汎用ロケールはドメイン独立であり、解釈を通じてこのモデル外でも使用できます。8つの解釈は、その再利用性が抽象的なものにとどまらないことを示しています。この研究の次のステップは合成です。ファンクター法則と合成定理を単一のエントリ内に追加し、フレームワーク資産に昇格させることです。
この研究は、RCP（規制コンプライアンスプロトコル）フレームワーク（arXiv:2603.29278）のクロスドメイン拡張性のための形式的基盤を提供します。このフレームワークはInformational EIP（Ethereum 改善提案） (EIP-RCP)として提出される予定であり、この形式的証明の結果は、そのEIP（Ethereum 改善提案）の内部整合性基盤として引用されます。とはいえ、このトピック自体の重要性はEIP（Ethereum 改善提案）提出とは独立しています（7つの汎用ロケールは、Ethereum L2 / クロスドメイン設計のための再利用可能な資産として、それ自体で公開されています）。
このトピックに関するすべての議論、反論、提案を歓迎します。
* * *
成果物
- arXivプレプリント: arXiv:2604.03844、“Safety and Liveness of Cross-Domain State Preservation under Byzantine Faults: A Mechanized Proof in Isabelle/HOL”
- GitHub: Oraclizer/formal-verification
- AFP: エントリ
Cross_Domain_State_Preservation（2026-03-25提出、2026-05-09改訂版アップロード、レビュー中） - RCP論文: arXiv:2603.29278
- ビルド環境: Isabelle/HOL 2025-2。
sorry/oopsはゼロ。4つの理論ファイル、3,215行。
1投稿 - 1参加者