Safety and Liveness of Cross-Domain State Preservation under Byzantine Faults: A Mechanized Proof in Isabelle/HOL

arXiv:2604.03844v2 Announce Type: replace Abstract: 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.