Formally guaranteeing the safety and liveness of regulatory state transitions in cross-domain state synchronization systems is increasingly important as tokenized assets are operated across heterogeneous blockchain networks and off-chain ledgers. This paper presents a mechanized proof of 3,215 lines in Isabelle/HOL establishing two complementary properties. First, cross-domain state preservation (safety): a regulatory state transition on one domain is faithfully reflected across all connected domains with structural preservation, encompassing bidirectional roundtrip preservation, consistency across an arbitrary finite set of domains, and per-asset isolation. Second, liveness under Byzantine faults: with up to $f < n/3$ Byzantine nodes, we prove deterministic resolution of conflicting regulatory actions, deadlock freedom, and starvation freedom. Combining the two, the liveness proof discharges the honest-node assumption of the safety proof, promoting conditional safety to an unconditional guarantee. The seven generic locales derived here are domain-independent and reusable via Isabelle/HOL's interpretation mechanism. To show they are not vacuously satisfied, every locale is concretely instantiated against the regulatory model, including a heterogeneous-action instance and an on-chain/DAML layer-crossing instance; the development contains eight concrete locale interpretations plus a parametric multi-domain instantiation. The application context is a regulatory state transition model based on the RCP framework (arXiv:2603.29278), which systematizes 31 requirements from 15 global financial regulators. All artifacts build without sorry or oops, have been submitted to the Archive of Formal Proofs (under review), and are available on GitHub.

翻译：在异构区块链网络和链下账本上运行代币化资产时，跨域状态同步系统中监管状态转换的安全性与活性形式化保证日益重要。本文提出一个在Isabelle/HOL中编写、包含3215行代码的机械化证明，确立两个互补性质。第一，跨域状态保持（安全性）：一个域上的监管状态转换在所有连接域上被忠实地反映，并保持结构完整性，涵盖双向往返保持、任意有限域集合的一致性以及每项资产的隔离性。第二，拜占庭故障下的活性：在最多$f < n/3$个拜占庭节点的情况下，我们证明了冲突监管动作的确定性解决、无死锁和无饥饿性。结合两者，活性证明解除了安全性证明中的诚实节点假设，将有条件安全性提升为无条件保证。本文推导出的七个通用语境与领域无关，可通过Isabelle/HOL的解释机制重用。为证明它们非空满足，每个语境都针对监管模型进行了具体实例化，包括一个异构动作实例和一个链上/DAML跨层实例；开发包含八个具体语境解释加上一个参数化多域实例化。应用背景是基于RCP框架（arXiv:2603.29278）的监管状态转换模型，该模型系统化了来自15个全球金融监管机构的31项要求。所有构件均在无sorry或oops的情况下构建，已提交至形式化证明档案库（审稿中），并在GitHub上公开。