Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Jinwook Kim

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.

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

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.

Paper Structure

This paper contains 71 sections, 9 theorems, 1 equation, 6 figures, 5 tables.

Table of Contents

  1. Introduction
  2. System Model and Threat Model
  3. System Model
  4. Domains.
  5. State transitions.
  6. Per-asset locking.
  7. Synchronization.
  8. Communication.
  9. Global state.
  10. Global validity.
  11. Threat Model
  12. Property 1 (Safety).
  13. Property 2 (Liveness).
  14. Combined.
  15. Non-Goals
  16. ...and 56 more sections

Key Result

Theorem 4.1

If an action sequence is valid at the source, the mapped sequence is valid at the target with the mapped final state. $\blacktriangleleft$$\blacktriangleleft$

Figures (6)

  • Figure 1: Regulatory state transition diagram. Five states with 12 valid transitions. CONFISCATED (solid dark) is the terminal state: all transitions from it return None. CONFISCATE is universally reachable from every non-terminal state.
  • Figure 2: Locale hierarchy for cross-domain state preservation (Property 1). Each level adds assumptions and proves additional properties. Theorems proven at each level are shown on the right.
  • Figure 3: Synchronization protocol workflow. Solid arrows: normal execution. Dashed red arrows: failure paths returning None. The lock is acquired before updates and released after, ensuring atomicity.
  • Figure 4: Locale architecture for liveness properties (Property 2). Three generic locales (blue) are defined independently of the regulatory domain. DQuencer_Instance (orange) instantiates all three and imports Regulatory_Instance (green) from Property 1.
  • Figure 5: Assumption discharge structure. Property 1 provides a conditional safety guarantee (assuming honest execution). Property 2 discharges this assumption under Byzantine faults, yielding an unconditional combined guarantee.
  • ...and 1 more figures

Theorems & Definitions (9)

  • Theorem 4.1: Sequential Preservation
  • Theorem 4.2: Cross-Domain Consistency
  • Theorem 4.3: Sync Isolation
  • Theorem 4.4: Regulatory Homomorphism
  • Theorem 4.5: Valid State Preservation
  • Theorem 5.1: Deterministic Selection
  • Theorem 5.2: Deadlock Freedom
  • Theorem 5.3: Starvation Bound
  • Theorem 5.4: Eventual Completion