原子跨域状态同步的机械化证明——Layer 2

引言

当一个资产同时存在于多个域时，其状态必须以某种形式在这些域之间耦合。本文讨论的情况是这种耦合必须是因果性的，而不仅仅是观察性的。如果在一个域中生效的状态转换未能到达另一个域，那么中间时段对于市场和监管者来说都会成为一个未定义区域，两个域会将同一资产视为两个不同的事实。现有的跨域消息传递基础设施（跨链桥、数据预言机、链上/链下连接器）通过两个独立的单向信道运作，这使得中间状态在结构上是可达到的。本文形式化定义了一种同步模型，在该模型中，这种中间状态在定义上就是不可达到的： 一种将两个域的状态转换绑定为一个单一因果单元的模型，即原子性同步。

这一轴心与价格预言机轴心是正交的。价格预言机处理的是观测值；任何使该值更信任最小化、或使其更慢且更具有可争议性的改进，都会提高对"数值是多少"这一观测的安全性。本文的主题不是观测值，而是效果：一个域中已生效的状态转换，是否以相同的效力并同时地在另一个域上生效。无论你把价格预言机做得多么安全，它回答的是"值是多少"；而效果是否在两个域中同时生效，则是一个独立的保证。与价格信息的不一致不同，效果的不一致会分裂市场本身。如果一个域接受了某个事实的效果，而另一个域继续交易，仿佛它尚未发生，那么它们之间的间隔恰好就是一个套利窗口。一个生效的事实必须同时被反映，否则就不应被反映。

这不是我们的主张，而是国际监管标准明确提出的要求。FATF 建议 16（Travel Rule）要求交易信息与资产转移"同行"，且截至 2025 年，117 个司法管辖区中，85 个已通过该立法，另有 14 个正在推进中。FATF 已采取官方立场，认为虚拟资产本质上无国界，因此一个司法管辖区的监管失败会产生全球性后果。BIS-IOSCO PFMI 原则 8（结算最终性）将最终结算定义为"不可撤销且无条件的转移"。根据这一定义，分布式账本的概率性结算（因分叉而可能被逆转）与该标准存在张力。PFMI 并非针对分布式账本的文件，但其最终结算标准可以理解为要求跨域效果的转移必须是不可撤销的、无条件的。两个领域（反洗钱和市场基础设施）从不同起点出发，最终都要求相同的属性：原子性的同时执行。 状态的因果耦合才是本文真正要讨论的问题。

问题沿着两个维度展开。安全性：如果同步正确执行，结果状态在每个域是否一致？活性：在包含拜占庭节点的去中心化环境中，同步是否真正进行？系统是否避免停机？资产是否不会陷入永久锁定？请求是否不会无限期延迟？

本文给出一个将两个维度绑定在单一模型中的结果，并在 Isabelle/HOL 中通过机械化证明予以验证。主题是原子性跨域状态同步，而共识层仅作为该同步所需的活性保证的操作引擎出现。更精确地说，它展示的是如何将安全性证明所假设的诚实节点在拜占庭环境下无条件地释放。作为一个附带结果，基于领导者的 BFT 共识的活性很少得到机械化证明的处理（尽管 HotStuff、Tendermint 家族以及许多构建于其上的 L2 定序器设计十分普遍）；本文为这一小群体增添了一个案例。但本文的主要主题是原子性状态同步本身。

完整的工件构建在 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 设计者隐含依赖的属性，但几乎没有人正式地表述过它。当两个 Rollup 交换消息时，何时以及在何种保证下，一侧生效的状态转换会在另一侧被反映？在共享排序下，当两个域同时改变一个单一状态时，中间状态是什么，观察到它的第三个域应该相信什么？这些问题构成了跨链桥设计、共享排序和跨 Rollup 原子组合的基础，但它们大多作为实现实践来处理，而没有以定理的形式表述。本文的起点是将该属性提升为显式陈述。

这个问题在每一个资产同时存在于多个域的场景中都出现。除了上述纯基础设施的例子外，对于金融资产，潜在的错配点遍布资产的因果性状态转换发生的每一处：清算、冻结、到期时权利的行使、衍生品结算、KYC 状态更新、监管行动的执行、资产类别重新分类、代币销毁与释放。本节通过两个代表性场景展示问题的结构。两者都使用金融资产，但其结构与上述 Rollup 间的状态转换相同。

让我们更具体地看这个问题。假设同一资产 $a$ 以耦合形式存在于两个域 $D_1$ 和 $D_2$ 上。耦合意味着每一侧上 $a$ 的状态必须在另一侧上反映。反映到什么程度？是只有值需要一致（如同价格信息），还是行动的效果也必须一致？

代表性场景 1：同步清算。 资产 $a$ 作为抵押品锁定在两个域上。价格下跌，清算触发条件在两个域上都达到。如果清算不是原子性地执行，$D_1$ 的清算恰好在 $D_2$ 之前完成，产生滑点，或者受保护的清算人争抢在两边同时清算。这不是价格信息的不一致（两边的价格相同），不一致产生于效果的时机。

代表性场景 2：监管冻结。 资产 $a$ 在两个域上被代币化。一个司法管辖区的监管机构对 $a$ 发出冻结令。在 $D_1$ 上，冻结被反映且交易暂停，但在 $D_2$ 上尚未被反映。在此期间，$D_2$ 上的每一笔交易都存在其法律效力与系统状态之间的差距。从 FATF Travel Rule 和国家 AML 法规的角度看，这是一种合规风险。

两个场景的共同结构可以压缩为一句话。

两个域的状态转换必须被绑定为一个单一的因果单元。

保证这一条件从不被打破，就是原子性同步的定义。现有的数据预言机无法满足这一要求。 数据预言机的主要场景是单向观测（价格馈送）；即使可以实现双向交付，那也是两个独立的单向信道，而不是因果耦合的双向同步。由于每个方向被作为独立事件处理，一侧成功而另一侧失败的中间状态在结构上是可达到的。

本文形式化定义的是一种同步模型，其中这种中间状态在定义上就是不可达到的。 我们称其为原子性跨域状态同步（双向的、因果耦合的、原子性的）。

问题通过将其分离为两个维度进行分析。

安全性：如果同步正确执行，结果状态在每个域是否一致？这是一个条件性陈述。它仅在同步被正确执行的假设下成立。

活性：在包含拜占庭节点的去中心化环境中，同步是否真正进行？也就是说，系统是否避免停机，资产是否不会陷入永久锁定，任何诚实请求（市场行动或监管行动）是否不会无限期延迟？

先前的工作分别处理了其中之一。Lochbihler 和 Marić 的 Merkle Functor 模式（FMBC 2020）在 Isabelle/HOL 中形式化了 Canton 分布式账本中的单域单向数据完整性。Velisarios（ESOP 2018）在 Coq 中验证了 PBFT 的安全性，活性不在范围内。Carr 等人（NFM 2022）在 Agda 中验证了 HotStuff 的安全性，并明确表示**"将活性留给关于特定实现的证明"**。Wanner 等人（SRDS 2020）在 Isabelle/HOL 中基于 Heard-Of 模型（无领导者）验证了日志复制协议的安全性和活性。

本文与上述先前工作的不同之处在于两点。(i) 它在一个单一的区域层次结构中处理跨域、双向、多域、每资产隔离的原子性状态同步。(ii) 它将活性作为基于领导者的 BFT 的机械化证明来处理，并释放安全性证明中的诚实节点假设（假设-保证推理）。这第二个贡献的份量不在于同步与非同步的难度。同步性假设是该模型的一个有意抽象选择（§8）。份量在于已验证属性的性质。通用 BFT 活性验证不处理的是行动优先级的确定性（两个冲突请求中哪一个先被处理，在所有诚实节点上是相同的），以及该优先级与每资产隔离的互锁方式，这些在机械化证明中被绑定在一起。通用共识所处理的问题——"谁构建下一个区块"——与本模型所要求的问题——"冲突行动中哪一个先生效，是否被确定性固定"——是不同的属性，后者必须被形式化为一个独立的区域。这也是通用 BFT 共识不能直接使用的原因。

2. 系统模型

我们将系统抽象如下。一个域由一个 4 元组定义：一个有限状态集 $S$，一个有限动作集 $A$，一个确定性转移函数 $\delta: S \times A \rightharpoonup S$，以及一个终止状态谓词 $terminal: S \to bool$。一个多域系统，对于一组域标识符 $D$，每个域 $d \in D$ 携带自己的 4 元组，并且对于每个资产标识符 $id$ 定义一个连接的域子集 $connected(id) \subseteq D$。

这种抽象是故意最小化的。无论一个域是 EVM 链、L2 Rollup，还是非区块链账本（例如像 DAML/Canton 这样的企业账本），只要它满足这个 4 元组，就进入模型。这正是后续七个通用区域可复用性的基础。

拜占庭环境假设是标准的 BFT 假设 $f < n/3$（即 $n \geq 3f + 1$）。该模型假设同步消息传递；扩展到部分同步模型留作开放问题（§8）。

3. 安全性：跨域状态保持

从这里开始，本文进入形式化模型本身。在模型中我们使用术语状态保持，它指的是状态同步的前向映射必须满足的数学条件。它意味着同步的一个定向步骤是两个域之间的前向同态，即状态机之间的一种结构保持同态（在标准代数意义上）。双向组合在本节稍后的 symmetric_state_preservation 中处理。

安全性部分位于 State_Preservation.thy 中（370 行，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"
    -- 自然性/同态条件：
    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 区域的核心是两个不同状态机之间的保持关系：一个域的一步动作如何对应另一个域的一步动作。这种对应关系由以下交换关系精确捕获。

$$\delta_t(\phi_s(s), \phi_a(a)) = \phi_s(\delta_s(s, a))$$

这里 $\phi_s$ 是状态映射，$\phi_a$ 是动作映射。左边是"在源处执行一步，然后映射到目标"，右边是"映射到目标，然后执行一步"。两个结果相等就是保持条件。 这定义了对单一步骤的保持。

关键定理如下。

定理 sequential_preservation。 如果单一步骤被保持，那么任意长度的动作序列也被保持。

这表明对单一步骤的保持提升为对一条路径的保持。证明通过对动作列表进行归纳，步骤情况由区域的 naturality 假设释放。

在 state_preservation 之上再叠加两个区域。

symmetric_state_preservation 定义了两个域之间的双向保持：前向映射 $\phi$ 与后向映射 $\psi$ 的组合是往返恒等映射的结构（这对于状态映射成立，如下所示，对于动作映射同样成立，源和目标的往返都是恒等）：

$$\psi \circ \phi = \mathrm{id}_S, \quad \phi \circ \psi = \mathrm{id}_T$$

明确说明此往返恒等成立的范围是必要的。当两个域的状态和动作词汇相互对应时，双向恒等成立。当两个域使用不同的动作类型时（如下面的 escalation_preservation 实例，其中源是监管动作的子集，目标是另一个单独的动作类型），它不被视为双射往返，而是单向保持，并停留在 state_preservation 层级而非 symmetric_state_preservation。也就是说，双向恒等是对两个表示可以无损地相互转换的情况的保证；当词汇不完全对应时，只对该部分陈述前向保持。onchain_daml_bridge 实例属于前者（对应词汇区域）。

这正是 Lochbihler 和 Marić 的 Merkle Functor 模式提供灵感的地方。Merkle Functor 是一种单向认证数据结构；本文将双向保持形式化为一个独立于通用区域层次结构的框架。两个框架的直接组合（将 Merkle Functor 导入 Isabelle 并与本模型组合）超出了本文的范围，留作未来工作。

multi_domain_preservation 同时处理关于任意有限域集 $D$ 的两件事：连接域之间的一致性，以及非连接域的隔离性（每资产隔离）。两个关键定理：

定理 cross_domain_consistency。 如果 sync_all 对于资产 $id$ 成功完成，那么 $connected(id)$ 中的每个域 $d$ 都反映相同的共识状态。

定理 sync_isolation。 同步一个资产会保持每个域上每个其他资产不变。

$$\forall \mathrm{id}' \neq \mathrm{id},\ \forall d \in D, \quad \mathrm{state}_d(\mathrm{id}') = \mathrm{state}_d^{\mathrm{prev}}(\mathrm{id}')$$

sync_isolation 是 Merkle Functor 模式没有的一种保证。在单域完整性中，保持其他资产这一概念本身是未定义的。在多域设置中，必须将"同步一个资产不会触及另一个资产"的保证纳入定义。

八个解释展示通用区域的范围

所有四个区域都是通用的。它们确实在有意义的域上运作，这一点通过八个具体解释得到证明。

其中，escalation_preservation 形式化了异构类型跨链保持的一个案例。两个域的动作类型完全相同（同质动作）的情况可以由现有模型处理，但两个域使用不同动作类型的情况（此处，源使用监管动作的升级子集，而目标使用单独定义的动作类型）需要一个单独的区域实例。

onchain_daml_bridge 是本文处理 EVM ↔ 非 EVM 边界的实例。前向映射将链上监管状态枚举发送到链下权限模型，后向映射是其逆，我们正式证明了它们的组合满足往返恒等。这是将像 DAML/Canton 这样的企业账本作为链下侧实例的工作。

4. 拜占庭故障下的活性

活性部分位于 Priority_Resolution.thy 中（407 行，3 个通用区域）和 DQuencer_Instance.thy（解释）。本节讨论如何将 §3 安全性所假设的诚实节点在拜占庭环境 $f < n/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"

从这三个区域推导出以下定理。

定理 select_highest_deterministic。 在具有单射优先级的消息集合中，选择最高优先级是确定性的。两个看到相同候选集的诚实节点会达成相同的决策。

定理 deadlock_freedom。 如果超时为正，则没有锁会被永远持有（lock_eventually_expires）。

定理 eventual_completion。 在领导者轮换公平的环境（任何 epoch 窗口中，诚实节点至少成为领导者一次）中，由诚实节点入队的每个请求在有限时间内被处理。

所有三个定理都是通用的。它们独立于域是什么。

释放安全性假设

本文的核心组合在于，安全性证明所假设的诚实节点被活性证明所释放。用假设-保证推理表述：

$$\underbrace{\text{安全性} \mid \text{诚实节点}}{\text{安全性}} + \underbrace{\text{诚实进展} \mid f < n/3}{\text{活性}} \implies \underbrace{\text{安全性} \mid f < n/3}_{\text{组合}}$$

安全性证明表明当同步由诚实节点执行时 valid_state_preservation 成立。这个诚实节点假设不能在单个域内释放。拜占庭环境假设本质上是共识层的一个属性。

活性证明直接证明了在 $f < n/3$ 下共识结果的确定性和进展性。也就是说，如果一个同步被提交，它是由共识多数选择的同步，并且该决策是确定性的。 这相当于用 BFT 假设替换了安全性证明中的诚实节点假设。

因此，两个证明的组合将条件性安全性提升为无条件保证。 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 中 state_preservation 区域的交换条件 $\delta_t(\phi_s(s), \phi_a(a)) = \phi_s(\delta_s(s, a))$ 正是两个状态机之间操作保持映射的定义。这种形式的要点在于，保持的不仅仅是两个域转移的对应关系，更是它们的结构。

第二，范畴论的函子。函子映射作为同态的推广，决定了本条目的学术地位。本条目目前以 4 个通用区域加 8 个解释的形式形式化了同态及其兄弟结构。当函子定律（保持恒等、保持组合）伴随形式化证明时，该条目就可证明地获得函子地位。本文的处理阶段是在这一证明之前。

第三，假设-保证推理（Misra-Chandy 1981）。这是 §4 中活性释放安全性证明中诚实节点假设的逻辑支柱。从条件性保证的组合中获得无条件保证，是分布式系统验证的标准逻辑。

这三个原理支撑了本条目的组合。范畴论、代数和分布式系统验证逻辑都在一个模型内运作，这是本文的方法论特征。

6. 工具选择与七个通用区域的可复用性

选择 Isabelle/HOL 进行这项工作无需辩护。考虑到验证目标是 (i) 状态转移的抽象结构，(ii) 分布式系统的进展属性，以及 (iii) 多层组合，一个具有区域模块性和丰富分布式系统验证先例的工具是自然的选择。本工作的四区域安全性层次结构与 Lochbihler 和 Marić 的 Merkle Functor 模式遵循相同的工具和相同的方法论（区域模块性），同时选择了不同的抽象轴（数据结构完整性 vs 状态转移保持）；它是一个同级结果。

与邻近先前工作的距离还有另一个维度。原子提交本身并不新鲜。2PC、3PC、原子交换和 HTLC 已经处理这个问题数十年，本文的贡献不是发明一个提交协议。如果现有的原子提交文献处理了提交协议的正确性，那么本工作的区分线在于，在其之上将三件事绑定到一个单一模型中，作为机械化证明：双向状态保持（前向和后向映射的组合是恒等）、每资产隔离，以及拜占庭活性。单向原子提交不需要前两者。也就是说，区别不在于它做什么（原子同步），而在于它通过形式化证明将保证绑定到多么深入的程度，并且据我们所知，形式化这种组合的案例是缺失的。

七个区域可在本模型之外复用。

上述适用性是一种主张，而非已证明的事实。每个应用都需要单独的解释工作。在本文中，我们展示了 escalation_preservation（异构类型跨链）和 dq_priority（一种 typedef 变通模式）作为该解释工作样貌的小样。后者是通过 sublocale 模式处理基于区域参数的 typedef 约束的案例，该模式本身是通用区域框架可复用性的一个小样本。

7. 对 L2 / 跨域设计的影响

这个形式化证明暗示了一些工具层面的设计原则。我们写暗示是因为形式化证明在模型内部确立了定理，但模型的哪个部分对应于现实，以及保真度如何，是一个独立的探究领域。本节旨在将该探究领域提出来讨论。

(a) 双向跨域同步不是两倍的单向同步。 仅处理单向同步的模型不需要往返恒等这一额外保证。在双向情况下，前向和后向的组合必须是恒等，这需要一个可组合的抽象。symmetric_state_preservation 区域封装了这种可组合性。

(b) 每资产隔离应成为模型的一等公民。 Merkle Functor 模式没有每资产隔离的概念，因为在单域完整性中，其他资产的存在在模型之外。在多域设置中，"一个资产上的同步不会触及另一个资产" 的保证必须纳入定义。sync_isolation 定理与这一点对应。

(c) 安全性与活性的组合通过分层架构解决。 在此模型中，状态同步层和共识进展层位于不同的区域层次结构中。两个层的定理通过假设-保证进行组合。这是一个观察：对于形式化证明而言，将共识视为一个假设释放工具，比将共识算法拉入一个统一模型更清晰。

(d) 结构性 OEV 遏制作为附带效应。 本模型的同步模式由原子的绑定 → 验证 → 提交循环组成。在此循环内，可提取信息不对称的时间窗口根据定义是：

$$\text{提取窗口}(t) = 0 \quad \text{对于 } t \in [\text{绑定}, \text{提交}]$$

循环内部是原子的，因此tick 之间的间隔概念不存在。这是一种发生遏制方法，与现有仅限于价格预言机的 OEV 缓解机制（这些机制重新分配已经发生的 OEV）在结构上不同。本文仅在这一节中提到这一点。一个单独的主题将全面处理 OEV 分类学、离散与连续更新模型的提取窗口函数，以及与共识优先级排序的分离。

8. 假设与局限

我们强调，此证明在模型内部成立；它不会自动由实现保证。 下面的假设并非隐藏以逃避验证；它们是明确的抽象选择。特别是，同步消息传递和公平领导者轮换的假设属于基于领导者、基于轮次的分布式共识验证的既定方法论传统（Heard-Of 模型家族，Charron-Bost & Schiper 2009；Wanner 等人 SRDS 2020），在该传统中，同步性/公平性假设是使活性可陈述的建模工具，而不是使结果空洞的漏洞。我们也承认，推广到部分同步是一个更难、更独立的问题（§9 Q1），并且本文不主张这种推广。

安全性假设：

• 同步消息传递。扩展到部分同步模型（消息延迟、重传、乱序）是一个开放问题。

• 诚实节点（仅安全性）。该假设在本文中由活性证明释放。

• 有限域集。动态域拓扑（运行时加入/离开）不在本模型范围内。

活性假设：

• 拜占庭 $f < n/3$。基于 Quorum 的 BFT 的标准假设。

• 公平领导者轮换。任何节点无限频繁成为领导者的假设。相当于基于 VRF 的实现中的随机性假设。

• 封闭系统（请求到达是有限/有界的）。开放系统（连续到达）中的饥饿自由是未来工作。

共同：

• 模型到实现的细化不在本文范围内。验证模型级定理如何在实际代码级成立，计划作为独立轨道进行。对于本文，我们推迟决定该细化轨道最适合哪种工具和组合模式。

关于在何处划定这个领域的边界，正如 Vitalik 的形式化验证文章（2026-05-18）所强调的，不隐藏假设是形式化证明的基础。

9. 开放问题

本文没有答案，或只有部分答案的问题。本节是问题，而非主张。

Q1. 推广到部分同步网络模型。 本模型假设同步消息传递。当推广到部分同步模型时，七个区域中哪些必须修改？fair_leader_system 看起来可能相当自然地推广，但 multi_domain_preservation 的 sync_all 更微妙。

Q2. 异质共识体制的组合。 本模型不假设所有域遵循相同的共识体制（仅域标识符是固定的）。尽管如此，关于跨域的异质共识体制（例如一个域 PoS，另一个域 PoA，再一个域非区块链账本）的组合的保证，不能直接从本模型推导出来。这种组合还需要什么？

Q3. 同步强度的异质性。 本文证明了一种单一强度的跨域状态同步。实际上，每个资产所需的同步强度不同。有些资产只需要单向观测，有些需要双向耦合，有些（例如受监管行动约束的资产）需要原子绑定作为必要。如何最好地形式化这样一种陈述：当在同一个系统上分支处理异质强度的资产时，每个资产所需的强度被保证，这是我们目前正在探索的方向。我们欢迎分布式系统和类型理论两方面对于强度之间归约关系（较高强度安全地包含较低强度）在 §3 的保持映射之上应采用何种结构的观点。

Q4. 模型到实现细化的最自然组合模式。 在将模型级定理下放到代码级细化时，哪个工具的组合成本最低？候选工具（Coq + MathComp、Lean 4、Creusot/Kani、F*）之间可互操作组合模式的案例尚未积累。

Q5. 应该验证什么（规范问题）。 本文将状态保持定义为交换同态。但在跨域设置中，"正确同步"的规范本身并不显然。当两个域的时间模型不同（区块高度 vs 挂钟时间 vs 逻辑时钟）时，应在谁的时钟下定义"发生在先"关系？哪些属性值得验证，哪些是可验证但空洞的（平凡为真，排除了什么）？这不是一个工具问题，而是一个建模问题。我们在通过实例确认通用区域确实在有意义的域上运作的过程中，切身体会到了这个区别的实际重要性；但关于跨域同步的正确规范是什么的一般理论，只有随着该领域更多形式化案例的积累才会显现。我们希望本文的话题是这种积累的一个起点。

上述问题计划在本话题的后续工作和学术出版物中增量处理。但我们相信，社区的额外视角将是这个话题最大的资产，超过我们自己的答案。

10. 结语

本文分享的不是一个形式化证明的完成报告，而是一个可共享的验证资产。 七个通用区域是与域无关的，可以通过解释在本模型之外使用。八个解释表明它们的可复用性并不仅仅停留在抽象层面。这项工作的下一步是组合：在一个条目内添加函子定律和组合定理，将其提升为一个框架资产。

本工作为 RCP (Regulatory Compliance Protocol) 框架（arXiv:2603.29278）的跨域扩展提供了形式化基础。该框架将作为信息性 EIP (EIP-RCP) 提交，而本形式化证明结果被引用为该 EIP 的内部一致性基础。尽管如此，本话题本身的重要性独立于 EIP 提交（七个通用区域本身作为以太坊 L2 / 跨域设计的可复用资产而公开）。

欢迎所有关于本话题的讨论、反驳和建议。

工件

• arXiv 预印本：arXiv:2604.03844，《拜占庭故障下跨域状态保持的安全性与活性：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 行。

• 原文链接： ethresear.ch/t/mechanize...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～