原子跨域状态同步的机械化证明——Layer 2 本文形式化了一种跨域原子状态同步模型，其中两个域的状态转换被绑定为一个因果单位，使得中间状态不可达。 跨域状态同步 形式化验证 Isabelle/HOL 安全性 活性 拜占庭容错 以太坊中文 发布于 2026-06-03 94 0 0
