Byzantine Fault Liveness, Discharged: What Properties 1 and 2 Together Guarantee

TL;DR

Property 2 of Oraclizer’s formal verification program is complete. Determinism, deadlock freedom, and starvation freedom are proven in Isabelle/HOL under the standard Byzantine threshold f < n/3. No sorry. No oops. But the real subject of this post is not Property 2 alone. It is what Properties 1 and 2 become when combined. The combined_safety_liveness theorem does not simply conjoin the two results. Property 2 discharges the honest-node assumption that Property 1 implicitly carried, and this is an instance of assume-guarantee reasoning. The consequence is that conditional safety is lifted into an unconditional safety + liveness guarantee. The seven domain-independent locales produced along the way (four from Property 1, three from Property 2) mention nothing about regulation, blockchain, or Oraclizer. Researchers working on MEV bundle ordering, distributed database locking, PoS consensus variants, or multi-shard synchronization can imports them in one line, instantiate their own domain types, and the already-proven theorems hold for their system unchanged.

---

The Question Byzantine Fault Liveness Was Built to Answer

The phrase Byzantine fault liveness appears throughout this post, so it is worth pinning down what it means up front. It is the guarantee that under a node population in which some nodes are Byzantine, the system eventually makes progress: consensus closes deterministically, no resource is locked indefinitely, and no request waits forever. If safety says “nothing bad happens,” liveness says “something good eventually does.”

In earlier posts we walked through the proof process and result for Property 1. regulatory_homomorphism and valid_state_preservation were the central theorems, and the work closed with AFP submission and the first official GitHub repository. The final section of that retrospective was honest about model boundaries. Property 1 stood on four assumptions: atomic synchronization, honest nodes, instant lock acquisition, and a finite static chain set.

The honest-node assumption was the heaviest of the four. Inside the model, OSS was treated as a single logical entity, and every node was assumed to follow the protocol. The actual D-quencer is a distributed consensus system of 10 to 100 nodes, some of which can be Byzantine. The gap between model and reality made the guarantee Property 1 mathematically established a conditional guarantee: “if OSS executes correctly, cross-domain state is preserved.”

Property 2 was built to close this conditional clause under Byzantine conditions. If, even with up to f < n/3 Byzantine nodes, the D-quencer consensus mechanism can guarantee that (1) conflicting regulatory actions are resolved deterministically, (2) no asset is locked indefinitely, and (3) every pending request is eventually processed, then the central premise of Property 1’s “correct execution” assumption is satisfied.

The axis of this entire post is that Property 2 is not “another theorem” but the theorem that discharges Property 1’s assumption.

Property 2 in Three Theorems

Property 2 is built on three main theorems. Each is proven inside a domain-independent locale in Priority_Resolution.thy and then instantiated for D-quencer’s regulatory consensus model in DQuencer_Instance.thy.

Theorem 1: Determinism (select_highest_deterministic)

theorem select_highest_deterministic:
  assumes fin: "finite S" and ne: "S ≠ {}"
  shows "∃!m. select_highest S = Some m"

In plain language: when conflicting regulatory actions arrive simultaneously, the consensus output for the same input is exactly one. Ties cannot occur.

This determinism is not accidental. make_priority_key constructs a 4-tuple (authority_rank, max_time - timestamp, action_severity, max_node - source_node) from each message, and the tuple is ordered by nat‘s lexicographic total order. authority_rank encodes the regulatory hierarchy (a court outranks an exchange operator, for example), and action_severity encodes the strength of the action (CONFISCATE > SEIZE > FREEZE). The reason source_node sits at the bottom of the tuple is to structurally eliminate ties: in the extreme case where every other field matches, node IDs always differ, so equal priority keys are impossible.

The auxiliary lemma priority_key_injectivity proves that two messages with the same priority key are the same message. This lemma is exactly what satisfies the priority_injective assumption in the priority_system locale, and as a result select_highest_deterministic applies to the D-quencer instance automatically.

Theorem 2: Deadlock Freedom (deadlock_freedom)

theorem deadlock_freedom:
  shows "∀lock_time current_time.
           ∃t' ≥ current_time.
             ¬ lock_effective lock_time t'"

In plain language: no asset is ever locked indefinitely. Even if Byzantine nodes refuse to release locks, timeout-based forced release puts an upper bound on lock duration.

The proof of this theorem is, somewhat surprisingly, short. Its core insight is that circular waiting is structurally impossible in a single-resource locking design. The deadlock graph analysis covered in distributed systems textbooks is unnecessary. We did not build a lock dependency graph spanning multiple resources. One lock per resource, one timeout, and the locale assumption timeout_positive: lock_timeout > 0 are enough.

This is a case where design simplicity translates directly into proof simplicity. Had we adopted multi-resource transactional locking, deadlock verification would have become a fundamentally harder problem. Single lock per resource plus timeout is a deliberate design decision, and the cost of that decision is recovered at the verification stage.

lock_eventually_expires is the stronger auxiliary lemma that explicitly proves “there exists a moment after the current time at which the lock has necessarily expired.” For the witness, we had to use lock_time + timeout + current_time rather than the more natural-looking lock_time + timeout. The subtlety here is covered in detail in the previous post (Proving D-quencer Liveness under Byzantine Faults: The Journey).

Theorem 3: Starvation Freedom (eventual_completion)

theorem eventual_completion:
  shows "∃e_final. pending e_final = 0"

In plain language: every pending regulatory request is eventually processed. No request stays in the queue forever.

This was the mathematically heaviest of the three theorems. The core idea is straightforward. pending is a natural number, starvation_bound guarantees periodic strict decrease, and natural numbers cannot decrease indefinitely, so pending must reach zero. This is a direct application of well-founded induction.

The proof became heavy at the step of translating this intuition into a form Isabelle/HOL could accept. We had to define an explicit predicate P n ≡ ∀epoch. pending epoch = n → ∃e_final. pending e_final = 0 and apply less_induct for strong induction. Two auxiliary lemmas cooperate: starvation_bound guarantees “where the decrease happens,” while pending_monotone guarantees “no recovery in between.” Together, they construct the decreasing measure required for well-founded induction.

The central assumption of the fair_leader_system locale is fair_leader: ∀epoch. ∃h ≥ epoch. h < epoch + fairness_bound ∧ leader_honest h. In other words, an honest leader is necessarily elected at least once within fairness_bound. This assumption is not free in a Byzantine model. The fair leader assumption only actually holds when VRF-based leader election is combined with an honest-majority assumption (honest_majority: card (honest_nodes nodes) > 2 * f_max). The BFT threshold of the dquencer_system locale (bft_threshold: card nodes ≥ 3 * f_max + 1) provides the foundation.

The Central Theorem: combined_safety_liveness and What “Discharge” Means for Byzantine Fault Liveness

So far we have looked at Property 2’s three theorems separately. Now we turn to how the two properties combine.

The central theorem of this post sits at the end of DQuencer_Instance.thy: combined_safety_liveness. This is the keystone of the entire Property 1 + 2 verification effort.

theorem combined_safety_liveness:
  assumes valid: "valid_state gs"
    and exists: "asset_exists gs source aid"
    and current: "get_reg_state gs source aid = Some s"
    and trans: "reg_transition s action = Some s'"
    and not_locked: "¬ is_locked gs aid"
    and fin: "finite (connected_chains gs aid)"
  shows "∃gs'. sync source action aid gs = Some gs' ∧ valid_state gs'"

The conclusion has two parts. First, sync necessarily succeeds (∃gs'. sync ... = Some gs'). Second, in the resulting state, valid_state is necessarily preserved. The first part is liveness, the second is safety. Both guarantees are delivered by a single theorem.

Figure 1: Property 1 + Property 2 Unified Theorem Architecture

Why This Is Not a Simple Conjunction

The naive approach is to bind the two properties together by conjunction: “P1 ∧ P2 holds.” But the proof of combined_safety_liveness is not structured that way.

proof -
  from not_locked obtain gs_locked where
    lock: "acquire_lock gs aid = Some gs_locked"
    using lock_acquire_success by auto
  ...
  then obtain gs' where synced: "sync source action aid gs = Some gs'"
    by auto
  have "valid_state gs'"
    using valid_state_preservation[OF valid exists current trans synced fin] .
  with synced show ?thesis by auto
qed

Reading the structure: D-quencer’s consensus mechanism (determinism, deadlock freedom, starvation freedom) guarantees that, given the not_locked premise, sync can make progress. The liveness portion produces lock-acquisition feasibility. That feasibility, in turn, supplies the precondition synced: sync source action aid gs = Some gs' required by valid_state_preservation (the result of Property 1). Property 1 proved “if sync succeeds, then valid_state is preserved,” and Property 2 fulfills that “if.”

This is the key. Property 1’s conclusion was a guarantee conditional on sync’s success. Without Property 2, that condition remains an assumption. The moment Property 2 guarantees that sync can progress even under Byzantine conditions, one of Property 1’s premise assumptions disappears. A conclusion with a vanished premise is no longer conditional.

An Instance of Assume-Guarantee Reasoning

This pattern has a name. Assume-guarantee reasoning. One component provides a guarantee under some assumption, and another component fulfills that assumption with its own conclusion. When the two components compose, the first component’s assumption is discharged, and the combined system delivers an unconditional guarantee.

In the distributed systems verification literature, assume-guarantee is the standard tool for composing component-level verification results. What we did was apply this pattern to the combination of safety and liveness. Property 1’s honest-node assumption is absorbed by Property 2’s BFT threshold (f < n/3) and fair leader assumption. The byzantine_bound: card (byzantine_nodes nodes) ≤ f_max in the dquencer_system locale explicitly bounds the number of Byzantine nodes, and honest_majority guarantees that honest nodes form a majority. Together these two assumptions reconstruct, in a Byzantine setting, the OSS behavior that Property 1 had abstracted as a single honest entity inside its model.

Lifting conditional safety into unconditional safety + liveness is a much stronger result than simply listing the two theorems side by side. The system’s correctness closes inside a single framework.

Figure 2: Assume-Guarantee Discharge, Showing How Property 2 Lifts Property 1’s Conditional Safety

What Safety and Byzantine Fault Liveness Together Guarantee

Now we put what the theorems actually mean into plain language.

Regulatory state consistency combined with progress. When a financial authority freezes a tokenized bond, every chain on which the bond exists transitions simultaneously to FROZEN. And the freeze request, after arriving at D-quencer, is reached by deterministic consensus and processed within bounded time even when some Byzantine nodes are present. Where previously consistency was guaranteed “if the freeze is applied,” now the guarantee reads “if the freeze request arrives, it is necessarily applied and consistency is preserved.”

Deterministic serialization of conflicting regulatory actions. If the SEC and the FCA simultaneously issue different regulatory actions on the same asset, select_highest selects exactly one according to the total order on priority keys. Ties are structurally impossible. Two contradicting actions cannot apply at the same time and push the system into an inconsistent state.

Bounded asset lock duration under Byzantine conditions. Even if Byzantine nodes refuse to release locks, the asset is eventually released. Lock duration has an upper bound set by lock_timeout, and that bound is formally guaranteed inside the model. There is no scenario in which an asset is permanently trapped.

No starvation of regulatory requests. Every pending regulatory request is processed within a bounded number of epochs, given the assumption that an honest leader is elected at least once within fairness_bound. There is no scenario in which Byzantine nodes can defer a particular request indefinitely.

Inductive invariant preservation in a Byzantine environment. Once the system starts in a valid state, no amount of synchronization activity can push it into an inconsistent state, even with Byzantine nodes present. This extends Property 1’s result, which was proven in an honest-node model, into a Byzantine environment via Property 2.

None of these guarantees is a “theoretical design goal.” They are mathematical facts verified by the Isabelle/HOL kernel exhaustively across every logical path.

Seven Reusable Locales

The second key output of Property 1 + 2 verification is verification infrastructure. The entire proof is built on seven domain-independent locales. Four live in State_Preservation.thy (Property 1), three in Priority_Resolution.thy (Property 2). None of these locales know anything about regulation, blockchain, or Oraclizer.

Property 1’s four locales:

Locale	Abstraction	Key Proven Properties
state_machine	finite states/actions + deterministic transition + terminal	terminal absorption, action sequence composition
state_preservation	naturality between source/target sync	naturality, sequential_preservation
symmetric_state_preservation	bidirectional + roundtrip	state_map_injective, no information loss
multi_domain_preservation	N-domain consistency	cross_domain_consistency, sync_isolation

Property 2’s three locales:

Locale	Abstraction	Key Proven Properties
priority_system	finite set + total order + injective priority	select_highest_deterministic, highest_priority_exists
deadlock_free_locking	finite resources + locks + positive timeout	deadlock_freedom, lock_eventually_expires
fair_leader_system	fair leader assumption + pending measure + non_honest bound	eventual_completion, starvation_bound

For an external researcher, using these seven locales takes exactly two lines. imports to bring them in, interpretation to instantiate the researcher’s own domain types. If the locale assumptions are satisfied, the already-proven theorems hold for that domain as is. No re-proving is necessary.

priority_system applies to MEV bundle ordering. In a Flashbots-style MEV auction, instantiating the priority key as (bidder_rank, gas_price, bundle_value, bundle_id) automatically yields the determinism property: the same input necessarily selects the same bundle. The same pattern applies to distributed task schedulers and to message ordering in multi-chain bridge relays.

deadlock_free_locking applies to row-level lock verification in distributed databases. Distributed SQL systems like CockroachDB and TiDB time out row-level locks specifically to prevent deadlock, and this locale’s deadlock_freedom formally verifies that mechanism. DeFi protocol HTLC timeouts share the same structure. “An asset is never locked forever” reduces to a formal theorem.

fair_leader_system applies to leader-based BFT consensus. In Tendermint or HotStuff, “if an honest leader is elected periodically, every pending transaction is processed within bounded time” translates into starvation freedom. All that needs to change is the instantiation of the leader_honest assumption to match the protocol’s leader election mechanism.

state_preservation and symmetric_state_preservation apply to structure-preserving verification of bidirectional database replication. Master-slave replication, distributed cache consistency, bidirectional synchronization between on-chain and off-chain state channels: all share the same pattern. Define sync and sync_inv, satisfy naturality and roundtrip, and information-loss-free bidirectional synchronization holds automatically.

multi_domain_preservation applies to multi-cloud state synchronization or multi-shard environments like Ethereum 2.0. When verifying that configuration state is consistently synchronized across AWS, GCP, and Azure, connected_domains determines which domains are affected and sync_isolation guarantees no impact on unrelated assets.

This reusability is worth emphasizing as deliberate design rather than a byproduct. From the moment we began writing Priority_Resolution.thy, we did not place D-quencer as a first-class citizen but instead made the abstract priority system the first-class citizen. D-quencer instantiation is separated into DQuencer_Instance.thy. The same separation applies between State_Preservation.thy and Regulatory_Instance.thy. This mirrors the philosophy by which Lochbihler generalized Canton’s Merkle Functor as ADS_Functor. Our seven locales extend that philosophy along a different axis of abstraction (state-transition preservation and Byzantine consensus liveness).

Figure 3: Seven Reusable Locales, Application Matrix Beyond Oraclizer

Two Axes of Extension: What Was Hard

For readers who reach this point unfamiliar with formal verification, one question naturally follows: how hard was this, exactly? The phrase “formal verification” gets thrown around often, but a sense of what is easy and what is hard inside the field is difficult to acquire from outside it. This section answers that question. The short version: what we did is to take one step further along two distinct axes simultaneously, and each axis is independently a difficult kind of work.

The two-axis sketch in the leftover corner of a meeting room whiteboard, drawn between other people’s unfinished thoughts, before it became Figure 4.

In formal verification, removing an assumption is not simply moving forward by one step. When an assumption is removed, every step of the proof that relied on it has to be re-examined. The structure resembles not a single domino tipping but rather pulling out one block from the bottom of a stack and watching the hundred blocks above it collapse all at once. This is what makes formal verification grow exponentially harder as assumptions are stripped away.

Difficulty 1: From Single Domain to N-Domain Bidirectional

Single-domain verification establishes that data inside one closed system remains intact through transformation. Conceptually, it is closer to one person checking that the notes in their personal notebook are not corrupted after editing. It is plenty hard, but the object of verification is one closed system.

N-domain bidirectional preservation is a different kind of work. Several people each hold their own notebook, and regardless of who adds notes in what order, all notebooks must eventually arrive at the same state. Furthermore, the system must permit moving from any notebook to any other without information loss. This is not “single-domain verification times N.” It requires defining the relationship between domains from scratch and proving that this relationship does not break under any possible change scenario.

Translated into proof terms: a single domain requires showing one commute relation. N-domain bidirectional requires showing pairwise commutes between domains together with roundtrip (lossless return) and isolation (per-asset independence) simultaneously. Case analysis grows quickly, and if a single case is missing an assumption, the whole structure collapses. There are technical reasons that Lochbihler’s Merkle Functor work stopped at the single-domain boundary, and the difficulties we encountered moving the pattern into N-domain bidirectional territory came from the same family of reasons.

Difficulty 2: Discharging the Honest-Node Assumption

A proof under the honest-node assumption can use “nodes follow the protocol” freely. Every message at every consensus step can be assumed to be in the agreed format, and every response can be assumed truthful. The moment that assumption is removed, a new question appears at every step of the proof: “Does this step still hold no matter how a Byzantine node interferes?”

By analogy: the difference between designing a company’s operating procedures under the assumption that all employees work honestly, and redesigning the same procedures under the assumption that some employees may file false reports, delay tasks, or actively obstruct. The latter is not simply a matter of bolting on a few verification steps. At every step of the procedure, one has to ask “could a false report break this step?” and, if it could, insert a mechanism to prevent it. Then one has to verify that this new mechanism does not introduce fresh assumptions elsewhere in the procedure.

In proof terms, this manifests as follows. An auxiliary lemma that took one line under an honest-node model expands into multiple case splits and a counting argument in the Byzantine model. At every step, one has to explicitly show that “the number of honest nodes satisfying the BFT threshold is sufficient,” and counting arguments of this kind are not the sort of thing automation tools resolve cleanly. We had to write an auxiliary lemma in the dquencer_system locale that derives honest_majority directly from the single assumption card nodes ≥ 3·f_max + 1, and that auxiliary lemma became the entry point for nearly every liveness proof that followed.

Difficulty 3: Building Proofs as Generic Locales

Proving a theorem about a specific system, and proving the same theorem in a form that applies to arbitrary systems, are different kinds of work. The analogy is the difference between drawing a map of one’s own neighborhood and defining map-drawing rules that work for any neighborhood. The latter requires separating features that happen to belong to one’s own neighborhood (the river is on the east side) from features common to all neighborhoods (roads are connected). If the separation is wrong, the rules either fail to apply elsewhere or become so general that they guarantee nothing.

The core challenge in locale proofs is minimality of assumptions. Assumptions that are too strong sacrifice generality; assumptions that are too weak make the theorem false. Finding the right level of abstraction is often harder than the proof itself. For some of our seven locales, the time spent refining the assumption set exceeded the time spent proving the theorems. fair_leader_system was the most striking example. Deciding what shape of fairness assumption would apply both to D-quencer’s VRF-based leader election and to other BFT consensus protocols like Tendermint or HotStuff required several rewrites.

This is why the reusability of the seven locales is a deliberate cost rather than a byproduct. From the start we did not treat D-quencer as the first-class citizen. The abstract priority system is the first-class citizen. The decision is a short-term cost, but in the long term it produces an asset that other systems can instantiate against the same abstraction.

How Far Did Prior Work Go

Holding these three difficulties in mind, we look at where recent achievements in the formal verification field actually sit.

Work	Tool	Domain Scope	Node Model	Liveness
Lochbihler & Marić (FMBC 2020)	Isabelle/HOL	Single domain	Honest (assumed)	Out of scope
Velisarios (ESOP 2018)	Coq	Single system	Byzantine	Out of scope (safety only)
HotStuff/Agda (NFM 2022)	Agda	Single system	Byzantine	Out of scope (safety only)
Wanner et al. (SRDS 2020)	Isabelle/HOL	Single system (log replication)	Byzantine (Heard-Of model)	Included (leaderless)
This work	Isabelle/HOL	N-domain bidirectional	Byzantine (BFT)	Included (leader-based + regulatory-specific)

The point to take from the table is not “this work sits above the others” but rather that each piece of work pursues a different depth along a different axis. Lochbihler’s Merkle Functor delivers a more refined result on data structure integrity than ours (we plan to compose with it in Property 3). Velisarios and HotStuff/Agda each go deep on the safety of PBFT and HotStuff respectively. Wanner et al. is an important precedent for verifying Byzantine safety + liveness in Isabelle/HOL on a leaderless protocol in the Heard-Of model.

What we did is close a specific combination these works did not. (a) The extension from single domain to N-domain bidirectional (Property 1), (b) the extension from honest-node to Byzantine BFT (Property 2), (c) combining both extensions inside one Isabelle/HOL framework (combined_safety_liveness), and (d) verifying regulatory-specific consensus properties (priority determinism, regulatory-asset deadlock freedom, regulatory-request starvation freedom) under Byzantine assumptions. To the best of our knowledge, no prior work contains all four.

This is not a dismissal of other work. Without Lochbihler’s Merkle Functor, our Property 3 composition would not be possible. Velisarios and HotStuff/Agda each move into deeper verification territory in their own directions; we simply moved one step in another direction. The only thing we record honestly is that to the best of our knowledge this combination is new. There is a reason we use this phrase carefully in formal verification: if someone points us to prior work we are unaware of, we will revise the wording immediately.

Figure 4: Two Axes of Extension, Showing Where Each Verification Effort Sits

Model Boundaries: What Byzantine Fault Liveness Discharged and What It Did Not

In the Property 1 retrospective, we explicitly listed four assumptions: atomic synchronization, honest nodes, instant lock acquisition, and a finite static chain set. We now record honestly how far Property 2 closed each.

Honest-node assumption: discharged. This is Property 2’s principal contribution. The BFT threshold and fair leader assumption in the dquencer_system locale together reconstruct, in a Byzantine setting, the OSS behavior that Property 1 had abstracted as a single honest entity. That said, the fair leader assumption itself remains a model assumption, and the argument that it is satisfied by VRF-based leader election together with honest-majority is made outside the model. This boundary is acknowledged explicitly in the comments of Priority_Resolution.thy.

Atomic synchronization: still abstracted. Inside the model, sync executes as a single step. In practice, network latency exists between lock acquisition, update, and lock release. In implementation, the BVC (Bind-Verify-Commit) pattern, preemptive locking, and per-chain finality tracking approximate this abstraction.

Instant lock acquisition: still abstracted. Inside the model, locks succeed immediately when not held. In a distributed environment, lock queues and timeouts handle the gap. That said, Property 2’s deadlock_free_locking formally guarantees the correctness of timeout-based forced release, so the consequence of this gap is verified. The gap itself remains in the model-to-implementation mapping layer.

Finite, static chain set: still abstracted. connected_chains does not change during sync execution. Dynamic topology is handled by registry-based lookup and by halting sync when topology changes.

This summary makes two things clear. First, it is true that Property 2 has discharged the heaviest of the four assumptions in a Byzantine setting. Second, the model is still a model, and not every gap is closed. The most honest fact formal verification produces is knowing exactly where it stops. These gaps are tracked in FORMAL_MODEL_MAPPING.md, and over the long term they will be closed by Creusot/Kani-based refinement proofs.

What Comes Next: Property 3 and Beyond

Property 3 is compositional verification. The work consists of composing our Cross-Domain State Preservation Functor with Lochbihler’s Merkle Functor, formally establishing that the state preservation proof beginning in Canton’s off-chain ledgers connects without interruption through Oraclizer synchronization to on-chain EVM state. In this composition, the Byzantine fault liveness result of this post becomes a core component. The Canton side takes responsibility for data structure integrity; we take responsibility for state-transition progress under Byzantine conditions.

Canton’s Merkle Functor pattern proves data structure integrity inside Canton. Our pattern proves state-transition preservation between domains. The two approaches operate on different axes of abstraction, and the composition is not direct. Which auxiliary lemmas are needed and which assumptions on each side must be made compatible are subjects we will address in earnest during the Property 3 modeling phase.

---

Properties 1 + 2: An Honest Ledger

To close, we restate the machine-verified facts.

Oraclizer’s cross-domain regulatory state synchronization system is formally verified along both safety and liveness. A regulatory state change on one chain is faithfully preserved across every connected chain (regulatory homomorphism), and even with up to f < n/3 Byzantine nodes present, D-quencer’s consensus operates deterministically, no asset is locked indefinitely, and every pending request is eventually processed.

The combined_safety_liveness theorem does not simply bind the two results together. Property 2 discharges Property 1’s honest-node assumption, forming an instance of assume-guarantee reasoning. The result is that conditional safety is lifted into an unconditional safety + liveness guarantee.

The seven domain-independent locales produced along the way mention nothing about Oraclizer. Distributed database locking, MEV bundle ordering, PoS consensus variants, multi-shard synchronization: in any field where the abstract pattern fits, the already-proven theorems hold without modification. This is the real value of the seven locales.

Atomic synchronization, instant lock acquisition, and a finite static chain set remain inside the model, and the formal correspondence between model and implementation (refinement) is still incomplete. Stating these gaps honestly does not weaken the model’s credibility; we believe it strengthens it.

This is not an audit. This is not a test. It is mathematical proof, and a unified guarantee that emerges from the combination of two properties. No oracle project has, to the best of our knowledge, achieved this combination before. And this proof is not for Oraclizer alone. Any team building cross-chain infrastructure can take this framework and verify their own system to the same standard. The proof files are open-sourced on GitHub, and the arXiv paper is freely accessible at 2604.03844.

More questions remain. Composition. Refinement. Partial-synchrony network models. Dynamic topology. We will continue to answer them in future posts.

---

References

[1]. Lochbihler, A., & Marić, O. (2020). Authenticated Data Structures as Functors in Isabelle/HOL. Formal Methods for Blockchains (FMBC 2020). AFP Entry: ADS_Functor. https://www.isa-afp.org/entries/ADS_Functor.html

[2]. Rahli, V., Vukotic, I., Völp, M., & Esteves-Verissimo, P. (2018). Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq. European Symposium on Programming (ESOP 2018). https://link.springer.com/chapter/10.1007/978-3-319-89884-1_22

[3]. Carr, H., Jenkins, C., Moir, M., Reynolds, A., Tinelli, C., Barrett, C., & Mahboubi, A. (2022). Towards Formal Verification of HotStuff-Based Byzantine Fault Tolerant Consensus in Agda. NASA Formal Methods (NFM 2022). https://link.springer.com/chapter/10.1007/978-3-031-06773-0_27

[4]. Wanner, J. P. M., Bessani, A., Voronkov, A., & Sangiorgi, D. (2020). A Formally Verified Protocol for Log Replication with Byzantine Fault Tolerance. Symposium on Reliable Distributed Systems (SRDS 2020). https://ieeexplore.ieee.org/document/9252054

[5]. Misra, J., & Chandy, K. M. (1981). Proofs of Networks of Processes. IEEE Transactions on Software Engineering, SE-7(4), 417–426. (Foundational paper on assume-guarantee reasoning.) https://ieeexplore.ieee.org/document/1702636

[6]. Kim, J. (2026). Safety and Liveness of Cross-Domain State Preservation under Byzantine Faults: A Mechanized Proof in Isabelle/HOL. arXiv:2604.03844. https://arxiv.org/abs/2604.03844

Learn More

Safety and Liveness of Cross-Domain State Preservation: Now on arXiv

Proving D-quencer Liveness under Byzantine Faults: The Journey

Cross-Domain State Preservation: What Was Proven and What It Means

Oraclizer Formal Verification (GitHub)