Mechanized Proofs for Atomic Cross-Domain State Synchronization

Layer 2
, ,
1

Introduction

When an asset exists on several domains at once, its state has to be coupled across those domains in some form. The case this post is about is the one where that coupling must be causal, not merely observational. If a state transition that takes effect in one domain fails to reach another, the interval in between becomes an undefined region for both markets and regulators, and the two domains start treating the same asset as two different facts. Existing cross-domain message-passing infrastructure (cross-chain bridges, data oracles, on-chain/off-chain connectors) operates over two independent unidirectional channels, so that intermediate state is structurally reachable. What this post formalizes is a synchronization model in which that intermediate state is unreachable by definition: a model where the state transitions of two domains are bound into a single causal unit, i.e. atomic synchronization.

This axis is orthogonal to the price-oracle axis. A price oracle deals with an observed value; any improvement that makes that value more trust-minimized, or slower and more contestable, raises the safety of the observation of what the number is. The subject here is not the observed value but the effect: whether a state transition that has taken effect on one domain takes effect, with the same force and at the same time, on another. However safe you make a price oracle, it answers what the value is; whether the effect takes hold simultaneously across two domains is a separate guarantee. Unlike a mismatch in price information, a mismatch in effect splits the market itself. If one domain accepts the effect of some fact while another keeps trading as though it had not yet happened, the interval between them is exactly an arbitrage window. A fact that takes effect must be reflected simultaneously, or not at all.

This is not our claim but a requirement that international regulatory standards make explicit. FATF Recommendation 16 (the Travel Rule) requires that transaction information “travel” together with the movement of the asset, and as of 2025, of 117 jurisdictions, 85 have passed that legislation and 14 more are in progress. FATF has taken the official position that virtual assets are inherently borderless, so that a regulatory failure in one jurisdiction produces global consequences. BIS-IOSCO PFMI Principle 8 (Settlement Finality) defines final settlement as an “irrevocable and unconditional transfer.” Read against that definition, the probabilistic settlement of a distributed ledger (the possibility of reversal by a fork) stands in tension with the standard. PFMI is not a document aimed at distributed ledgers, but its final-settlement criterion reads as a requirement that the transfer of effect across domains be reflected irrevocably, and unconditionally. Two areas (AML and market infrastructure), starting from different places, end up requiring the same property: atomic simultaneous enforcement. The causal coupling of state is the real problem this post is about.

The problem splits along two dimensions. Safety: if synchronization was performed correctly, is the resulting state consistent across every domain? Liveness: in a decentralized environment that includes Byzantine nodes, does synchronization actually proceed; does the system avoid halting, does no asset fall into a permanent lock, and is no request delayed indefinitely?

This post shares a result that ties the two dimensions together in a single model and proves them, mechanized, in Isabelle/HOL. The subject is atomic cross-domain state synchronization, and the consensus layer appears only as the operational engine for the liveness guarantee that this synchronization requires. More precisely, it is the work of showing that the honest nodes assumed by the safety proof can be discharged unconditionally under a Byzantine environment. As a side result, liveness of leader-based BFT consensus has rarely been treated in a mechanized proof (despite the ubiquity of HotStuff, the Tendermint family, and the many L2 sequencer designs built on them); this work adds one case to that small body. But the main subject of this post is atomic state synchronization itself.

The full artifact builds in Isabelle/HOL 2025-2 at 3,215 lines, with zero sorry/oops. The result is public as the arXiv:2604.03844 preprint and can be inspected directly in the GitHub repository (Oraclizer/formal-verification). The integrated AFP entry Cross_Domain_State_Preservation is under review, with the 2026-05-09 revision passing the build.

1. The Problem

Cross-domain state consistency is a property that any multi-chain, L2, or L3 designer implicitly depends on, yet almost nobody states formally. When two rollups exchange messages, when and under what guarantee is a state transition that took effect on one side reflected on the other? Under shared sequencing, when two domains change a single state simultaneously, what is the intermediate state, and what should a third domain that observes it believe? These questions underlie cross-chain bridge design, shared sequencing, and atomic composition across rollups, but they are mostly handled as implementation practice and not stated in the form of a theorem. The starting point of this post is to raise that property to an explicit statement.

This problem arises in every scenario where an asset exists on multiple domains at once. Beyond the pure-infrastructure examples above, in financial assets the potential mismatch points are everywhere an asset’s causal state transition occurs: liquidation, freezing, exercise of rights at maturity, derivative settlement, KYC-status updates, enforcement of regulatory actions, asset-class reclassification, token burn-and-release. This section shows the structure of the problem through two representative scenarios. Both use financial assets, but their structure is identical to the inter-rollup state transitions above.

Let us look at the problem more concretely. Suppose the same asset a exists in a coupled form on two domains D₁ and D₂. Coupled means the state of a on each side must be reflected on the other. Reflected in what sense? Does only the value need to agree, as with price information, or must the effect of an action agree as well?

Representative scenario 1, simultaneous liquidation. Asset a is locked as collateral on two domains. The price falls and the liquidation trigger is reached on both. If liquidation is not performed atomically, D₁’s liquidation settles just before D₂’s, producing slippage, or a protected liquidator races to liquidate on both sides. This is not a mismatch in price information (the price was the same on both domains). The mismatch arises in the timing of effect.

Representative scenario 2, regulatory freeze. Asset a is tokenized on two domains. A regulator in one jurisdiction issues a FREEZE order against a. On D₁ the FREEZE is reflected and trading halts, but on D₂ it has not yet been reflected. During that interval, every trade on D₂ has a gap between its legal effect and the system state. From the standpoint of the FATF Travel Rule and national AML regulations, this is a compliance exposure.

The shared structure of the two scenarios compresses to one line.

The state transitions of the two domains must be bound into a single causal unit.

Guaranteeing that this condition is never broken is the definition of atomic synchronization. Existing data oracles cannot meet this requirement. A data oracle’s main scenario is unidirectional observation (a price feed); even where bidirectional delivery is possible, it is two independent unidirectional channels, not a causally coupled bidirectional synchronization. Since each direction is handled as an independent event, an intermediate state where one side succeeds and the other fails is structurally reachable.

What this work formalizes is a synchronization model in which that intermediate state is unreachable by definition. We call it atomic cross-domain state synchronization (bidirectional, causally coupled, atomic).

The problem is analyzed by separating it into two dimensions.

Safety: if synchronization was performed correctly, is the resulting state consistent across every domain? This is a conditional statement. It holds only under the assumption that synchronization is performed correctly.

Liveness: in a decentralized environment that includes Byzantine nodes, does synchronization actually proceed? That is, does the system avoid halting, does no asset fall into a permanent lock, and is no honest request (market action or regulatory action alike) delayed indefinitely?

Prior work addresses one or the other. Lochbihler and Marić’s Merkle Functor pattern (FMBC 2020) formalized single-domain, unidirectional data integrity within the Canton distributed ledger in Isabelle/HOL. Velisarios (ESOP 2018) verified the safety of PBFT in Coq, with liveness out of scope. Carr et al. (NFM 2022) verified HotStuff safety in Agda and explicitly “leave liveness to proofs about specific implementations.” Wanner et al. (SRDS 2020) verified the safety and liveness of a log-replication protocol in Isabelle/HOL on a Heard-Of model basis (leaderless).

This work is distinguished from the prior work above in two ways. (i) It treats atomic state synchronization that is cross-domain, bidirectional, multi-domain, and per-asset isolated, within a single locale hierarchy. (ii) It handles liveness as a mechanized proof of leader-based BFT, and discharges the safety proof’s honest-node assumption (assume-guarantee reasoning). The weight of this second contribution does not lie in synchronous vs. asynchronous difficulty. The synchrony assumption is an intended abstraction choice of this model (§8). The weight lies in the character of the verified properties. What general BFT-liveness verification does not address is the determinism of action priority (which of two conflicting requests is processed first is identical across all honest nodes), and the way that priority interlocks with per-asset isolation, bound together in a mechanized proof. The question general consensus addresses, “who builds the next block,” and the question this model requires, “is it deterministically fixed which of the conflicting actions takes effect first,” are different properties, and the latter had to be formalized as a separate locale. This is also the formal reason general BFT consensus is not used as-is.

2. System Model

We abstract the system as follows. A domain is defined by a 4-tuple: a finite state set S, a finite action set A, a deterministic transition function ή: S × A ⇀ S, and a terminal-state predicate terminal: S → bool. A multi-domain system, over a set of domain identifiers D, has each domain d ∈ D carry its own 4-tuple, and for each asset identifier id a connected subset of domains connected(id) ⊆ D is defined.

This abstraction is deliberately minimal. Whether a domain is an EVM chain, an L2 rollup, or a non-blockchain ledger (for example, an enterprise ledger like DAML/Canton), it enters the model as long as it satisfies the 4-tuple. This is what underpins the reusability of the seven generic locales that follow.

The Byzantine-environment assumption is the standard BFT assumption f < n/3 (i.e. n ≄ 3f + 1). The model assumes synchronous message delivery; extension to a partially synchronous model is left as an open problem (§8).

3. Safety: Cross-Domain State Preservation

From here the post enters the formal model proper. Inside the model we use the term state preservation, which refers to the mathematical condition that the forward map of state synchronization must satisfy. It means that one directional step of synchronization is a forward homomorphism between the two domains, a structure-preserving homomorphism between state machines (in the standard algebraic sense). The bidirectional composition is handled later in this section by symmetric_state_preservation.

The safety part lives in State_Preservation.thy (370 lines, 4 generic locales). The four locales are layered as follows.

locale state_machine =
  fixes states     :: "'s set"
    and actions    :: "'a set"
    and transition :: "'s ⇒ 'a ⇒ 's option"
    and terminal   :: "'s set"
  assumes finite_states:      "finite states"
    and finite_actions:       "finite actions"
    and terminal_subset:      "terminal ⊆ states"
    and terminal_absorbing:   "⟩ s ∈ terminal; a ∈ actions ⟧ âŸč transition s a = None"
    and transition_closed:    "⟩ s ∈ states; a ∈ actions; transition s a = Some s' ⟧ âŸč s' ∈ states"
    and transition_domain:    "s ∉ states âŸč transition s a = None"

locale state_preservation =
  source: state_machine states⇩s actions⇩s transition⇩s terminal⇩s +
  target: state_machine states⇩t actions⇩t transition⇩t terminal⇩t
  for states⇩s ... and states⇩t ... +
  fixes state_map  :: "'s ⇒ 't"
    and action_map :: "'a ⇒ 'b"
  assumes state_map_well_defined:  "s ∈ states⇩s âŸč state_map s ∈ states⇩t"
    and action_map_well_defined:   "a ∈ actions⇩s âŸč action_map a ∈ actions⇩t"
    and terminal_preservation:     "s ∈ terminal⇩s âŸč state_map s ∈ terminal⇩t"
    -- the naturality / homomorphism condition:
    and naturality:
      "⟩ s ∈ states⇩s; a ∈ actions⇩s; transition⇩s s a = Some s' ⟧
       âŸč transition⇩t (state_map s) (action_map a) = Some (state_map s')"
    and naturality_none:
      "⟩ s ∈ states⇩s; a ∈ actions⇩s; transition⇩s s a = None ⟧
       âŸč transition⇩t (state_map s) (action_map a) = None"

The heart of the state_preservation locale is the preservation relation between two distinct state machines: how a step of one domain corresponds to a step of the other. This correspondence is captured exactly by the following commuting relation.

\delta_t(\phi_s(s), \phi_a(a)) = \phi_s(\delta_s(s, a))

Here φₛ is the state map and φₐ the action map. The left side is “step at the source, then map to the target,” the right side is “map to the target, then step.” That the two results coincide is the preservation condition. This defines preservation of a single step.

fig1_commuting_square_no_eq
fig1_commuting_square_no_eq573×277 19.8 KB

The key theorem follows.

Theorem sequential_preservation. If a single step is preserved, then a sequence of actions of arbitrary length is preserved.

This states that preservation of a single step lifts to preservation of a path. The proof is by induction on the action list, and the step case is discharged by the locale’s naturality assumption.

Two more locales stack on top of state_preservation.

symmetric_state_preservation defines bidirectional preservation between two domains: the structure where the composition of the forward map φ and the backward map ψ is the roundtrip identity (this holds for the state map as below, and equally for the action map, with both source and target round-trips):

\psi \circ \phi = \mathrm{id}_S, \quad \phi \circ \psi = \mathrm{id}_T

Where this roundtrip identity holds is worth making explicit. Bidirectional identity holds on the region where the state and action vocabularies of the two domains correspond. When the two domains use different action types (the escalation_preservation instance below, where the source is the escalation subset of the regulatory actions and the target is a separate action type), it is treated not as a bijective roundtrip but as unidirectional preservation, and lives at the state_preservation level rather than symmetric_state_preservation. That is, the bidirectional roundtrip is the guarantee for the case where the two representations convert into each other without information loss, and where the two vocabularies do not correspond identically, only forward preservation is stated for that part. The onchain_daml_bridge instance belongs to the former (corresponding vocabulary region).

This is the point at which Lochbihler and Marić’s Merkle Functor pattern served as inspiration. The Merkle Functor was a unidirectional authenticated data structure; this work formalizes bidirectional preservation as a separate framework within a generic locale hierarchy. The direct composition of the two frameworks (importing the Merkle Functor into Isabelle and composing it with this model) is out of scope for this post and is left to future work.

multi_domain_preservation handles two things at once over an arbitrary finite set of domains D: consistency among connected domains, and isolation of unconnected domains (per-asset isolation). Two key theorems:

Theorem cross_domain_consistency. If sync_all completes successfully for asset id, then every domain d in connected(id) reflects the same consensus state.

Theorem sync_isolation. Syncing one asset leaves every other asset, on every domain, unchanged.

\forall \mathrm{id}' \neq \mathrm{id},\ \forall d \in D, \quad \mathrm{state}_d(\mathrm{id}') = \mathrm{state}_d^{\mathrm{prev}}(\mathrm{id}')

sync_isolation is a guarantee the Merkle Functor pattern did not have. In single-domain integrity, the very notion of preservation of another asset is undefined. In the multi-domain setting, the guarantee that a sync on one asset does not touch another asset must enter the definition.

Eight interpretations demonstrate the scope of the generic locales

All four locales are generic. That they actually operate on meaningful domains is shown by eight concrete interpretations.

Interpretation Locale Meaning
reg_sm state_machine regulatory state transition (single chain)
reg_state_machine state_machine multi-chain instance
escalation_preservation state_preservation preservation between two chains with different action types; source = escalation subset of regulatory actions, target = a separate action type
forward_layer_preservation state_preservation on-chain enum → off-chain permission model
backward_layer_preservation state_preservation off-chain permission model → on-chain enum
onchain_daml_bridge symmetric_state_preservation forward + backward composition = roundtrip
multi-domain instance multi_domain_preservation N-domain consistency of regulatory state
dq_priority priority_system (§4) consensus message priority

Among these, escalation_preservation formalizes a case of heterogeneous-type cross-chain preservation. The case where the two domains’ action types are exactly the same (homogeneous action) can be handled by the existing model, but the case where the two domains use different action types (here, the source uses the escalation subset of the regulatory actions while the target uses a separately defined action type) required a separate locale instance.

onchain_daml_bridge is the case where this work treats the EVM ↔ non-EVM boundary. The forward map sends the on-chain regulatory-state enum to an off-chain permission model, the backward map is its inverse, and we formally proved that their composition satisfies the roundtrip identity. It is work that takes an enterprise ledger like DAML/Canton as the off-chain-side instance.

f3
f31192×794 99.3 KB

4. Liveness under Byzantine Faults

The liveness part lives in Priority_Resolution.thy (407 lines, 3 generic locales) and DQuencer_Instance.thy (interpretation). This section addresses how the honest nodes assumed by §3’s safety are discharged under a Byzantine environment f < n/3.

The skeleton of the three generic locales:

locale priority_system =
  fixes priority :: "'m ⇒ 'k::linorder"
  assumes priority_injective:
    "⟩ priority m1 = priority m2 ⟧ âŸč m1 = m2"

locale deadlock_free_locking =
  fixes timeout :: nat
  assumes timeout_positive: "timeout > 0"

locale fair_leader_system =
  fixes leader_at      :: "nat ⇒ 'n"
    and is_honest      :: "'n ⇒ bool"
    and pending        :: "nat ⇒ nat"
    and fairness_bound :: nat
  assumes fairness_bound_positive: "fairness_bound > 0"
    and fair_leader:
      "∀epoch. ∃e. epoch ≀ e ∧ e < epoch + fairness_bound ∧ is_honest (leader_at e)"
    and honest_progress:
      "⟩ is_honest (leader_at e); pending e > 0 ⟧ âŸč pending (Suc e) < pending e"
    and non_honest_bounded:
      "pending (Suc e) ≀ pending e"

From these three locales the following theorems are derived.

Theorem select_highest_deterministic. In a set of messages with injective priorities, selecting the highest priority is deterministic. Two honest nodes that see the same candidate set reach the same decision.

Theorem deadlock_freedom. If the timeout is positive, no lock is held forever (lock_eventually_expires).

Theorem eventual_completion. In an environment where leader rotation is fair (within any epoch window an honest node becomes leader at least once), every request enqueued by an honest node is processed within finite time.

All three theorems are generic. They are independent of what the domain is.

Discharging the safety assumption

The core composition of this work is that the honest nodes assumed by the safety proof are discharged by the liveness proof. Phrased as assume-guarantee reasoning:

\underbrace{\text{Safety} \mid \text{honest nodes}}_{\text{safety}} + \underbrace{\text{honest progress} \mid f < n/3}_{\text{liveness}} \implies \underbrace{\text{Safety} \mid f < n/3}_{\text{combined}}

Safety proves valid_state_preservation when a sync is performed by honest nodes. This honest-node assumption cannot be discharged within a single domain. The Byzantine-environment assumption is essentially a property of the consensus layer.

The liveness proof directly proves the determinism and progress of the consensus result under f < n/3. That is, if a sync was committed, it is the sync chosen by the consensus majority, and that decision is deterministic. This amounts to substituting the safety proof’s honest-node assumption with the BFT assumption.

The composition of the two proofs therefore promotes conditional safety to an unconditional guarantee. The combined theorem in DQuencer_Instance.thy states this in theorem form.

f2
f2984×616 64.5 KB

Theorem combined_safety_liveness. Given that the asset exists (asset_exists), a valid state transition is defined (reg_transition s action = Some s'), the asset is not locked (ÂŹ is_locked), and the connected domain set is finite, then if the global state is valid (valid_state gs), synchronization succeeds (sync source action aid gs = Some gs') and the resulting state also preserves the global validity invariant (valid_state gs'). Determinism (dq_select_highest_deterministic), deadlock freedom (dq_deadlock_freedom), and starvation freedom (dq_starvation_bound) are established as separate theorems within the same entry, and together they are the ground on which the above safety invariant holds under a Byzantine environment without the honest-node assumption.

5. The Mathematical Backbone of This Work

The mathematical principles this work rests on sort into three strands.

First, algebraic homomorphism. The commuting condition of §3’s state_preservation locale, ήₜ(φₛ(s), φₐ(a)) = φₛ(ήₛ(s, a)), is exactly the definition of an operation-preserving map between two state machines. The point of this form is to preserve not merely the correspondence of the two domains’ transitions but their structure.

Second, the functor of category theory. The functorial map, a generalization of the homomorphism, determines the academic status of this entry. This entry currently formalizes homomorphisms and their sibling structures in the form of 4 generic locales plus 8 interpretations. When the functor laws (preservation of identity, preservation of composition) are accompanied by formal proof, the entry acquires functor status provably. This post treats the result at the stage prior to that justification.

Third, assume-guarantee reasoning (Misra-Chandy 1981). This is the logical backbone of the composition in §4 where liveness discharges the safety proof’s honest-node assumption. Obtaining an unconditional guarantee from the composition of conditional guarantees is a standard logic of distributed-systems verification.

These three principles underpin the composition of this entry. That category theory, algebra, and distributed-systems verification logic all operate within one model is the methodological character of this work.

6. Tool Choice and the Reusability of the Seven Generic Locales

The choice of Isabelle/HOL for this work is not something that needs defending. Given that the verification targets are (i) the abstract structure of state transitions, (ii) progress properties of distributed systems, and (iii) multi-layer composition, a tool with locale modularity and a rich precedent in distributed-systems verification is the natural choice. The four-locale safety hierarchy of this work follows the same tool and same methodology (locale modularity) as Lochbihler and Marić’s Merkle Functor pattern, while choosing a different abstraction axis (data-structure integrity vs. state-transition preservation); it is a sibling result.

There is one more dimension of distance from adjacent prior work. Atomic commit itself is not new. 2PC, 3PC, atomic swaps, and HTLCs have addressed the problem for decades, and the contribution here is not the invention of a commit protocol. If existing atomic-commit literature addresses the correctness of the commit protocol, the distinguishing line of this work lies in binding three things on top of it, in a single model, as a mechanized proof: bidirectional state preservation (the composition of forward and backward maps is the identity), per-asset isolation, and Byzantine liveness. A unidirectional atomic commit does not require the first two. That is, the distinction is not in what it does (atomic synchronization) but in how far it binds, by formal proof, the guarantees under which it holds, and a case that formalizes this combination is, to the best of our knowledge, absent.

The seven locales are reusable outside this model.

Locale Applicable domains
priority_system MEV bundle priority, multi-chain bridge relay message ordering, distributed task scheduler
deadlock_free_locking distributed-DB row-level lock timeout (CockroachDB, TiDB), DeFi HTLC timeout
fair_leader_system starvation freedom in Tendermint, HotStuff
state_preservation + multi_domain_preservation bidirectional DB replication, distributed cache consistency, state-channel on/off-chain synchronization

The applicability above is a claim, not a proven fact. Each application requires a separate interpretation effort. In this post we presented, as small samples of what that interpretation effort looks like, escalation_preservation (heterogeneous-type cross-chain) and dq_priority (a typedef-workaround pattern). The latter is a case of working around a typedef constraint over a locale parameter via a sublocale pattern, and the pattern itself is a small sample of the reusability of the generic-locale framework.

7. Implications for L2 / Cross-Domain Design

This formal proof suggests a few design principles at the tooling level. We write suggest because formal proof settles theorems inside the model, but which part of reality the model corresponds to, and with what fidelity, is a separate area of inquiry. This section is written with the intent of putting that latter inquiry up for discussion.

(a) Bidirectional cross-domain synchronization is not twice the unidirectional. A model that treats only unidirectional synchronization does not require the additional guarantee of roundtrip identity. In the bidirectional case the composition of forward and backward must be the identity, and this requires a composable abstraction. The symmetric_state_preservation locale encapsulates that composability.

(b) Per-asset isolation should be a first-class citizen of the model. The Merkle Functor pattern has no notion of per-asset isolation, because in single-domain integrity the very existence of other assets is outside the model. In the multi-domain setting, the guarantee that a sync on one asset does not touch another must enter the definition. The sync_isolation theorem corresponds to this.

(c) The combination of safety and liveness is resolved by a layered architecture. In this model the state-synchronization layer and the consensus-progress layer live in different locale hierarchies. The theorems of the two layers are composed by assume-guarantee. This is an observation that treating consensus as an assumption-discharging tool is cleaner, for formal proof, than pulling the consensus algorithm into a unified model.

(d) Structural OEV containment as a side effect. The synchronization pattern of this model consists of an atomic bind → verify → commit cycle. Within this cycle the time window of extractable information asymmetry is, by definition,

\text{extraction window}(t) = 0 \quad \text{for } t \in [\text{bind}, \text{commit}]

The cycle interior is atomic, so the notion of an interval between ticks does not exist. This is a containment-of-occurrence approach, structurally different from existing OEV-mitigation mechanisms confined to price oracles (which redistribute OEV that has occurred). This post mentions it in this one section only. A separate topic will treat OEV taxonomy, the extraction-window function of discrete vs. continuous update models, and the separation from consensus priority sequencing in full.

8. Assumptions and Limits

We stress that this proof holds inside the model; it is not automatically guaranteed by an implementation. The assumptions below are not hidden to evade verification; they are explicit abstraction choices. In particular, the assumptions of synchronous message delivery and fair leader rotation are within the established methodological tradition of leader-based, round-based distributed-consensus verification (the Heard-Of model family, Charron-Bost & Schiper 2009; Wanner et al. SRDS 2020), and in that tradition synchrony/fairness assumptions are modeling devices that make liveness statable, not loopholes that make the result vacuous. We also acknowledge that generalization to partial synchrony is a harder, separate problem (§9 Q1), and this work does not claim that generalization.

Safety assumptions:

  • Synchronous message delivery. Extension to a partially synchronous model (message delay, redelivery, reordering) is an open problem.

  • Honest nodes (safety alone). This assumption is discharged in this work by the liveness proof.

  • Finite domain set. Dynamic domain topology (runtime join/leave) is outside this model.

Liveness assumptions:

  • Byzantine f < n/3. The standard assumption of quorum-based BFT.

  • Fair leader rotation. The assumption that any node becomes leader infinitely often. Equivalent to the randomness assumption in a VRF-based implementation.

  • Closed system (request arrival is finite/bounded). Starvation freedom in an open system (continuous arrival) is future work.

Common:

  • Model-to-implementation refinement is out of scope for this work. Verifying how the model-level theorems hold at the actual code level is planned as a separate track. For this work we defer the decision on which tools and which composition pattern that refinement track sits most naturally on.

On where to draw the boundary of this area, as Vitalik’s formal-verification post (2026-05-18) emphasizes, not hiding assumptions is the basis of formal proof.

9. Open Questions

Problems for which this post has no answer, or only a partial one. This section is questions, not claims.

Q1. Generalization to a partially synchronous network model. This model assumes synchronous message delivery. When generalizing to a partially synchronous model, which of the seven locales must be modified? fair_leader_system looks like it would generalize fairly naturally, but the sync_all of multi_domain_preservation is more subtle.

Q2. Composition of heterogeneous consensus regimes. This model does not assume that all domains follow the same consensus regime (only the domain identifier is fixed). Still, a guarantee about the composition of heterogeneous consensus regimes across domains (e.g. one domain PoS, another PoA, another a non-blockchain ledger) is not directly derivable from this model. What more is needed for this composition?

Q3. Heterogeneity of synchronization strength. This work proves a single-strength cross-domain state synchronization. In reality, the synchronization strength each asset requires differs. Some assets need only unidirectional observation, some need bidirectional coupling, and some (e.g. subjects of regulatory action) require atomic binding as a necessity. How best to formalize the statement that, while branching heterogeneous-strength assets on the same system, the strength each asset requires is guaranteed, is a direction we are currently exploring. We welcome perspectives from both distributed systems and type theory on what structure the reduction relation among strengths (a higher strength safely contains a lower one) should take on top of §3’s preservation map.

Q4. The most natural composition pattern for model-to-implementation refinement. With which tool is the composition cost lowest when pulling model-level theorems down to code-level refinement? Cases of interoperable composition patterns among candidate tools (Coq + MathComp, Lean 4, Creusot/Kani, F*) are not accumulating.

Q5. What should be verified (the specification question). This work defined state preservation as a commuting homomorphism. But in a cross-domain setting the specification of “correct synchronization” is itself non-obvious. When the two domains’ time models differ (block height vs. wall-clock time vs. logical clock), under whose clock should the happened-before relation be defined? Which properties are worth verifying, and which are verifiable but vacuous (trivially true, ruling nothing out)? This is not a tooling problem but a modeling problem. We experienced the practical importance of this distinction in the course of confirming, via instances, that the generic locales actually operate on meaningful domains; but a general theory of what the correct specification of cross-domain synchronization is will only come into view as more formalization cases in this area accumulate. We hope this topic is one starting point for that accumulation.

The questions above are planned to be treated incrementally in the follow-up work and academic publication of this topic. But we believe the additional perspectives of the community will be the greatest asset of this topic, more than our own answers.

10. Closing

What this topic shared is not a completion report of a formal proof, but a shareable verification asset. The seven generic locales are domain-independent and can be used outside this model via interpretation. The eight interpretations demonstrate that their reusability does not stay in the abstract. The next step of this work is composition: adding the functor laws and composition theorems within a single entry to elevate it to a framework asset.

This work provides a formal basis for the cross-domain extensibility of the RCP (Regulatory Compliance Protocol) framework (arXiv:2603.29278). That framework is to be submitted as an Informational EIP (EIP-RCP), and this formal-proof result is cited as the internal-consistency basis of that EIP. That said, the significance of this topic itself is independent of the EIP submission (the seven generic locales are public as reusable assets for Ethereum L2 / cross-domain design in their own right).

All discussion, counterarguments, and suggestions on this topic are welcome.

Artifacts

  • arXiv preprint: arXiv:2604.03844, “Safety and Liveness of Cross-Domain State Preservation under Byzantine Faults: A Mechanized Proof in Isabelle/HOL”

  • GitHub: Oraclizer/formal-verification

  • AFP: entry Cross_Domain_State_Preservation (submitted 2026-03-25, revision uploaded 2026-05-09, under review)

  • RCP paper: arXiv:2603.29278

  • Build environment: Isabelle/HOL 2025-2. Zero sorry/oops. 4 theory files, 3,215 lines.

2 Likes