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

TL;DR

This paper provides a formal, mechanized proof in Isabelle/HOL demonstrating safety and liveness properties for cross-domain state synchronization systems under Byzantine faults, ensuring reliable regulatory state transitions across heterogeneous blockchain networks.

Contribution

It introduces a comprehensive formal proof of safety and liveness in cross-domain state synchronization, including reusable domain-independent components, under Byzantine fault conditions.

Findings

Proves bidirectional state preservation across multiple domains.

Establishes deterministic conflict resolution under Byzantine faults.

Ensures deadlock and starvation freedom in the system.

Abstract

Formally guaranteeing the safety and liveness of regulatory state transitions in cross-domain state synchronization systems is a problem of growing importance as tokenized assets are increasingly operated across heterogeneous blockchain networks and off-chain ledgers. This paper presents a mechanized proof of 2,348 lines in Isabelle/HOL establishing two complementary properties. First, cross-domain state preservation (safety): a regulatory state transition performed on one domain is faithfully reflected across all connected domains with structural preservation. This guarantee encompasses bidirectional roundtrip preservation, consistency across an arbitrary finite set of domains, and per-asset isolation. Second, liveness under Byzantine faults: in the presence of up to f < n/3 Byzantine nodes, we prove deterministic resolution of conflicting regulatory actions, deadlock freedom, and starvation freedom. In the combination of these two properties, the liveness proof discharges the honest-node assumption of the safety proof under Byzantine faults, promoting conditional safety to an unconditional guarantee. The seven generic locales derived in this process are domain-independent and reusable for arbitrary domains via Isabelle/HOL's interpretation mechanism. 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 regulatory authorities. All proof artifacts build in Isabelle/HOL without sorry or oops, have been submitted to the Archive of Formal Proofs (under review), and are publicly available on GitHub.