pith. sign in

arxiv: 2604.03844 · v1 · submitted 2026-04-04 · 💻 cs.CR · cs.LO

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

Jinwook Kim (for the Oraclizer Core Team) This is my paper

Pith reviewed 2026-05-13 17:02 UTC · model grok-4.3

classification 💻 cs.CR cs.LO
keywords formal verificationIsabelle/HOLByzantine faultscross-domain synchronizationsafety and livenessblockchain interoperabilityregulatory compliance
0
0 comments X

The pith

Isabelle/HOL proof establishes safety and liveness for cross-domain regulatory states under Byzantine faults.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents a mechanized proof that regulatory state transitions performed in one blockchain domain are faithfully preserved across all connected domains, including bidirectional roundtrips and per-asset isolation. It also shows that the system resolves conflicting actions, avoids deadlocks, and prevents starvation even when up to one-third of nodes are Byzantine. The liveness result removes the honest-node assumption required by the safety proof, turning the guarantee unconditional. This matters for tokenized assets that must maintain regulatory compliance while moving across heterogeneous ledgers and networks.

Core claim

We prove cross-domain state preservation (structural reflection of any regulatory transition across an arbitrary finite set of domains) together with liveness under f < n/3 Byzantine faults (deterministic conflict resolution, deadlock freedom, and starvation freedom). Because the liveness proof discharges the honest-node assumption of the safety proof, the combined result yields unconditional safety for the regulatory state transition model.

What carries the argument

Seven generic locales in Isabelle/HOL that encode the safety and liveness properties and allow them to be instantiated for arbitrary domains via the interpretation mechanism.

Load-bearing premise

The formal model accurately captures the RCP framework requirements and that the Byzantine fault threshold f < n/3 is the only fault model needed.

What would settle it

A concrete execution in which a regulatory state transition performed on one domain fails to appear on another domain while the number of Byzantine nodes remains below one-third would falsify the safety claim.

Figures

Figures reproduced from arXiv: 2604.03844 by Jinwook Kim (for the Oraclizer Core Team).

Figure 1
Figure 1. Figure 1: Regulatory state transition diagram. Five states with 12 valid transitions. CONFISCATED (solid dark) is the terminal [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Locale hierarchy for cross-domain state preservation (Property 1). Each level adds assumptions and proves additional [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Synchronization protocol workflow. Solid arrows: normal execution. Dashed red arrows: failure paths returning [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Locale architecture for liveness properties (Property 2). Three generic locales (blue) are defined independently of [PITH_FULL_IMAGE:figures/full_fig_p009_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Assumption discharge structure. Property 1 provides a conditional safety guarantee (assuming honest execution). [PITH_FULL_IMAGE:figures/full_fig_p012_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Import dependency graph. Priority_Resolution.thy does not import Regulatory_Instance.thy (dashed line), preserving domain independence. DQuencer_Instance.thy imports both, serving as the join point. Build information. All files build in Isabelle/HOL 2025-2 without sorry or oops [PITH_FULL_IMAGE:figures/full_fig_p016_6.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper presents a 2348-line mechanized proof in Isabelle/HOL of two complementary properties for cross-domain regulatory state transitions based on the RCP framework: (1) safety (cross-domain state preservation with bidirectional roundtrip consistency, multi-domain agreement, and per-asset isolation) under an honest-node assumption, and (2) liveness (deterministic conflict resolution, deadlock freedom, and starvation freedom) under the standard Byzantine threshold f < n/3. The liveness result is then used to discharge the honest-node assumption, yielding unconditional safety. Seven generic, domain-independent locales are derived and submitted to the Archive of Formal Proofs with no 'sorry' or 'oops' commands.

Significance. If the result holds, the work supplies a reusable, machine-checked foundation for safety and liveness guarantees in cross-domain tokenized-asset systems subject to regulatory constraints. The fully verified Isabelle/HOL development, explicit locale interpretations, and public artifacts constitute a clear strength; the combination of conditional safety with Byzantine liveness to obtain an unconditional guarantee is a non-trivial formal contribution that directly addresses the RCP requirements.

minor comments (2)
  1. §3 (model definition): the transition relation for regulatory actions could explicitly state the finiteness assumption on the set of domains, even though it is implicit in the locale quantification.
  2. Table 1 (locale summary): the column describing 'honest-node assumption' would benefit from a cross-reference to the exact locale predicate that is later discharged by the liveness theorem.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive review, accurate summary of the 2348-line mechanized proof, and recommendation to accept. The assessment correctly highlights the combination of conditional safety with Byzantine liveness to obtain an unconditional guarantee, the domain-independent locales, and the public artifacts.

Circularity Check

0 steps flagged

No significant circularity; self-contained mechanized proof

full rationale

The paper presents a fully machine-checked Isabelle/HOL proof (2348 lines, no sorry/oops) of safety under an honest-node assumption and liveness under f < n/3 Byzantine faults. The liveness result is then used to discharge the honest-node assumption, yielding unconditional safety. This is a standard, non-circular logical composition in formal verification: the two properties are proved separately against the stated model and locales, then combined. No step reduces by definition or self-citation to its own inputs; the seven generic locales are domain-independent and reusable via interpretation. The derivation is self-contained against the RCP framework model and standard Byzantine assumptions, with all artifacts submitted to the Archive of Formal Proofs.

Axiom & Free-Parameter Ledger

0 free parameters · 3 axioms · 0 invented entities

The proof relies on standard Isabelle/HOL logic, the RCP framework model from the cited prior arXiv paper, and the classic f < n/3 Byzantine fault threshold; no free parameters or new invented entities are introduced.

axioms (3)
  • standard math Standard Isabelle/HOL higher-order logic and locale interpretation mechanism
    Invoked throughout the 2348-line development to structure the seven generic locales.
  • domain assumption RCP framework model of regulatory state transitions (arXiv:2603.29278)
    The safety and liveness statements are proved relative to this model.
  • domain assumption Byzantine fault model with f < n/3
    Used to discharge the honest-node assumption in the combined safety-liveness theorem.

pith-pipeline@v0.9.0 · 5566 in / 1428 out tokens · 35638 ms · 2026-05-13T17:02:55.205910+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

10 extracted references · 10 canonical work pages

  1. [1]

    AuthenticatedDataStructuresasFunctorsinIsabelle/HOL,

    A.LochbihlerandO.Marić,“AuthenticatedDataStructuresasFunctorsinIsabelle/HOL,”inFormalMethodsforBlockchains (FMBC2020), OASIcs, vol.84, pp.6:1–6:15, 2020.AFPentry:https://isa-afp.org/entries/ADS_Functor.html

    work page 2020

  2. [2]

    Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq,

    V. Rahli, I. Vukotic, M. Völp, and P. Esteves-Verissimo, “Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq,” inProgramming Languages and Systems (ESOP 2018), LNCS, vol. 10801, pp. 619–650, 2018

    work page 2018

  3. [3]

    ByMC: Byzantine Model Checker,

    I. Konnov and J. Widder, “ByMC: Byzantine Model Checker,” inISoLA 2018, LNCS, vol. 11246, pp. 327–342, 2018

    work page 2018

  4. [4]

    A Formally Verified Protocol for Log Replication with Byzantine Fault Tolerance,

    J. Wanner, L. Chuat, and A. Perrig, “A Formally Verified Protocol for Log Replication with Byzantine Fault Tolerance,” in Proc. IEEE International Symposium on Reliable Distributed Systems (SRDS), pp. 101–112, 2020

    work page 2020

  5. [5]

    A Regulatory Compliance Protocol for Asset Interoperability between Traditional and Decentralized Finance in Tokenized Capital Markets,

    J. Kim and J. Hong (for the Oraclizer Research Group), “A Regulatory Compliance Protocol for Asset Interoperability between Traditional and Decentralized Finance in Tokenized Capital Markets,” arXiv:2603.29278 [cs.CY], 2026

    work page arXiv 2026

  6. [6]

    Cross Domain State Preservation,

    J. Kim, “Cross Domain State Preservation,” submitted to the Archive of Formal Proofs, 2026. Primary artifact reference: https://github.com/Oraclizer/formal-verification

    work page 2026

  7. [7]

    Formal Verification,

    Oraclizer, “Formal Verification,” GitHub repository, 2026.https://github.com/Oraclizer/formal-verification

    work page 2026

  8. [8]

    Research Publications,

    Digital Asset, “Research Publications,” Daml SDK documentation.https://docs.daml.com/canton/architecture/ research.html

    work page

  9. [9]

    TowardsFormalVerificationofHotStuff-Based ByzantineFault Tolerant Consensus in Agda,

    H.Carr, C. Jenkins, M. Moir, V. C.Miraldo, andL.Silva, “TowardsFormalVerificationofHotStuff-Based ByzantineFault Tolerant Consensus in Agda,” inNASA Formal Methods (NFM 2022), LNCS, vol. 13260, pp. 616–635, 2022

    work page 2022

  10. [10]

    TheHeard-OfModel: ComputinginDistributedSystemswithBenignFaults,

    B.Charron-BostandA.Schiper,“TheHeard-OfModel: ComputinginDistributedSystemswithBenignFaults,”Distributed Computing, vol. 22, no. 1, pp. 49–71, 2009. 16 A Proof Artifact Summary Table 5: Proof artifact summary. File Lines Role Key Theorems State_Preservation.thy 383 Prop. 1 generic (4 locales)sequential_preservation, cross_domain_consistency, sync_isolatio...

    work page 2009