Defining D-quencer Liveness under Byzantine Faults: Determinism, Deadlock Freedom, and Starvation Freedom

TL;DR

Property 1 modeled OSS as a single logical entity, proving that “if executed correctly, cross-domain state is preserved,” a safety guarantee. But real-world OSS runs on one of several nodes elected through D-quencer consensus. What if some nodes act maliciously? What if conflicting regulatory orders arrive simultaneously? Property 1 alone cannot answer these questions. Property 2 targets Byzantine fault verification: formally proving three liveness properties under Byzantine conditions (f < n/3), namely determinism, deadlock freedom, and starvation freedom. These three properties are designed as domain-independent, reusable locales applicable not only to regulatory systems but to distributed systems broadly. If Property 1 defined the “if condition,” Property 2 verifies that this “if condition” holds even in Byzantine environments.

---

The Hidden Assumptions of Property 1

In the previous post, we reported that cross-domain state preservation had been mathematically proven. Three core theorems, regulatory_homomorphism, valid_state_preservation, and reg_multi_domain_instantiation, were verified by the Isabelle/HOL kernel, submitted to AFP, and published on GitHub.

But every formal proof has assumptions. If the assumptions do not hold, neither does what the proof guarantees. Let us revisit the assumption list of Property 1.

1. All nodes honestly follow the protocol
2. The sync function executes atomically
3. Lock acquisition occurs instantaneously
4. No priority conflicts exist between simultaneously arriving regulatory actions
5. A single leader exists implicitly

Assumptions 2 and 3 are implementation-level concerns. Preemptive locking mechanisms, timeouts, and automatic releases bridge the gap between these assumptions and reality. Assumptions 1, 4, and 5, however, are fundamentally different. What these assumptions imply is that Property 1’s guarantees are effectively confined to the safety of a centralized service.

Modeling OSS as a single logical entity means that the proof never examines what consensus occurs internally, who the leader is, or whether the leader is honest. The internals of the sync function remained a black box. Property 1 provided a conditional guarantee: “if sync is called correctly, the result is correct.” It did not prove that “sync is actually called correctly.”

In a decentralized system, this conditional is critical. D-quencer consists of 10 to 100 nodes, some of which may be Byzantine (malicious). A Byzantine node could refuse to release locks, drop or reorder messages, or inject invalid transitions. Property 1 is silent about all of these scenarios.

Property 2 exists to break this silence.

Safety and Liveness: Two Different Questions

In formal verification, safety and liveness are the two pillars of system correctness. Safety says “bad states are never reached.” Liveness says “good things eventually happen.” Both are necessary. Neither alone suffices to claim system correctness.

A system with only safety guarantees could satisfy safety by freezing all assets and doing nothing. No bad state is reached. But if a regulator’s freeze order sits unprocessed in a queue, the system is “safe but useless.”

Property 1 (safety) proved that “cross-domain state is preserved.” Property 2 (liveness) must prove that “even when conflicting regulatory actions arrive simultaneously, the system does not halt, no asset is trapped forever, and outcomes are deterministic.”

The relationship between these two properties can be stated more precisely: Property 1 defines the “if condition” and Property 2 verifies that this “if condition” is met even under Byzantine environments. Property 1 stated: “if sync executes correctly, state is preserved.” Property 2 proves: “even with Byzantine nodes, sync executes correctly.” Combined, they yield an unconditional guarantee: “in a Byzantine environment, cross-domain regulatory state is synchronized deterministically, without halting, without neglect.”

Figure 1: Safety × Liveness Composition

Three Liveness Properties

Property 2 is not a single proposition but the conjunction of three independent liveness properties. Each carries distinct formal meaning, and each excludes a different class of system failure.

Determinism: A Unique Outcome

Suppose the U.S. SEC and the U.K. FCA simultaneously issue different regulatory orders against the same tokenized bond. The SEC orders a FREEZE; the FCA orders a SEIZE. D-quencer must process exactly one of these orders first, and that choice must be deterministic. If different nodes select different orderings given the same input, consensus breaks.

The formal meaning of determinism is the existence proof of a total order. Over a finite message set, a priority function induces a total order, and the message with the highest priority exists uniquely.

Priority is defined as a lexicographic order over a 4-tuple: (authority_rank, negated_timestamp, action_severity, node_id). International bodies (FATF) outrank national bodies (SEC); at the same authority level, earlier-issued orders take precedence; at the same timestamp, the more severe sanction prevails; and when everything else is equal, node ID serves as a tiebreaker.

This 4-tuple uses nat × nat × nat × nat in Isabelle/HOL, directly leveraging the standard library’s built-in lexicographic linorder instance. The fact that no separate linear order instance registration is required significantly reduces modeling complexity.

type_synonym priority_key = "nat × nat × nat × nat"

definition make_priority ::
  "authority_level ⇒ nat ⇒ reg_action ⇒ nat ⇒ nat ⇒ priority_key"
where
  "make_priority auth ts act nid max_ts =
    (authority_rank auth, max_ts - ts, action_severity act, nid)"

The max_ts - ts sign inversion is a key technical point. The regulatory principle “earlier timestamp = higher priority” (earlier-issued orders take precedence) must be mapped onto nat’s default ordering (larger values rank higher), requiring sign inversion. The precondition max_ts ≥ ts is added as a locale assumption.

Deadlock Freedom: The System Does Not Halt

If determinism addresses the question “in what order should things be processed,” deadlock freedom addresses “can processing happen at all.” A deadlock is a state where two or more processes wait for resources held by each other, making no progress indefinitely.

In Property 1, the preemptive locking mechanism was introduced to prevent concurrent regulatory actions. If a sync is in progress for an asset, another sync attempt for the same asset fails. But what if a Byzantine node acquires a lock and intentionally never releases it? That asset would remain locked forever.

Timeout-based forced release solves this problem. Every lock records its acquisition time, and if the current time exceeds lock_time + timeout, the lock is considered expired. Expired locks are excluded from the active_locks set.

definition lock_expired :: "'r ⇒ bool" where
  "lock_expired r = (case lock_time r of None ⇒ False
                     | Some t ⇒ current_time ≥ t + timeout)"

definition active_locks :: "'r set" where
  "active_locks = {r ∈ resources. is_locked r ∧ ¬ lock_expired r}"

In this model, the proof of deadlock freedom is relatively straightforward. Oraclizer’s locking structure uses single-resource locks (one lock per asset ID), which structurally eliminates the classical deadlock condition of “circular wait.” Adding timeouts ensures that even a Byzantine node’s intentional lock retention is resolved within finite time.

Starvation Freedom: No Asset Is Neglected

Deadlock freedom and starvation freedom may appear similar but are fundamentally different properties. Deadlock freedom guarantees “the system as a whole does not halt.” Starvation freedom guarantees “no specific request is ignored indefinitely.” A system may be making overall progress (deadlock-free) while a particular asset’s regulatory request keeps getting deprioritized and never processed (starvation). That is starvation.

Consider a scenario in D-quencer where starvation could occur. If Byzantine nodes are consecutively elected as leaders and keep ignoring regulatory requests for a specific asset, the probability of this happening is $(f/n)^k$, which decreases exponentially with the number of epochs. But the probability is not zero.

A critical design decision was needed here. Directly proving VRF’s probabilistic fairness in Isabelle/HOL would require the HOL-Probability library, which would cause proof complexity to explode. Probabilistic reasoning substantially exceeds the scope of Property 2.

Instead, we adopt assume-guarantee reasoning, a standard academic pattern.

Assume: “Within any epoch, at least one honest node is elected as leader within k consecutive epochs” (fair_leader_assumption)

Guarantee: Under this assumption, all pending requests are processed within finite time, proven deterministically.

locale fair_leader_system =
  fixes leader_at :: "nat ⇒ 'n"
    and is_honest :: "'n ⇒ bool"
    and pending :: "nat ⇒ nat"
    and fairness_bound :: nat
  assumes 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"

The timeout-based deadlock freedom insight, captured on a park bench before it became a formal assumption.

The honest_progress assumption is the crux. When an honest leader is elected and the pending queue is non-empty, the pending queue size strictly decreases in the next epoch. This decreasing measure on nat forms the basis of the termination proof. Since natural numbers cannot decrease indefinitely, the pending queue eventually reaches zero.

There is also the non_honest_bounded assumption: the pending queue does not grow during epochs when a Byzantine leader is elected. This implies a closed-system assumption, meaning no new requests arrive during the analysis interval. Without this assumption, the queue could grow unboundedly while a Byzantine leader refuses to process, and starvation freedom would not hold. The closed-system assumption limits Property 2’s scope to “completion of processing for a given finite queue.” Modeling the arrival of new requests remains a topic for future work.

Stating this limitation transparently is the honest posture of formal verification.

Figure 2: Starvation Freedom Proof Structure under Assume-Guarantee Reasoning

Why Byzantine Inclusion Matters

The decision to include Byzantine nodes in Property 2 is not mere academic completeness. There are four concrete reasons for performing Byzantine fault verification.

First, product value. Property 1 assumed OSS as a single logical entity. In reality, OSS runs through one of several nodes elected via D-quencer consensus. Property 1 alone only guarantees “safety of a centralized service”; safety in a decentralized environment remains unproven. Property 2 with Byzantine inclusion verifies this precondition.

Second, implementation design guidance. The proof assumptions in a Byzantine environment (timeout inequalities, minimum honest node ratios, epoch length constraints) translate directly into parameter design rationale for D-quencer implementation. At Phase 4 (D-quencer implementation), these become “design constraints derived from proofs.” For instance, if the proof yields the simple constraint timeout > 0, the implementation translates this to T > 2δ + ε (at least twice the network round-trip time plus a safety margin).

Third, academic value. Canton’s CPP 2021 paper (Lochbihler, Schneider) mentioned Byzantine environment verification as a “Next step.” Performing this Byzantine verification with the same tool (Isabelle/HOL) on a consensus algorithm in the regulatory domain constitutes a meaningful academic contribution.

Fourth, strengthening Property 3. In Property 3 (composition of heterogeneous verification systems), the guarantee from the Oraclizer side becomes stronger. With Property 1 alone, the guarantee is conditional: “if OSS executes correctly, state is preserved.” With Properties 1+2, the guarantee becomes unconditional: “correct execution is guaranteed even in a Byzantine environment.” In assume-guarantee composition, a stronger guarantee reduces the burden on the glue layer.

Byzantine Model: Abstracting BFT Consensus

Byzantine inclusion does not mean formalizing BLS signature cryptographic security or elliptic curve arithmetic. Property 2’s Byzantine fault verification adopts the strategy of assuming properties of consensus outcomes and proving liveness on top of them.

datatype node_behavior = Honest | Byzantine
definition bft_valid :: "node_info set ⇒ bool" where
  "bft_valid ns = (card (honest_nodes ns) > 2 * card (byzantine_nodes ns))"

bft_valid is the BFT safety condition requiring that honest nodes exceed twice the number of Byzantine nodes. This is equivalent to n ≥ 3f + 1. Under this condition, the bft_select function sorts valid messages by priority and selects the highest-priority one. The bft_determinism theorem proves this selection is unique.

Attacks a Byzantine node can attempt are enumerated into four types.

datatype byzantine_action =
    ByzDropMessage dq_message
  | ByzReorderMessages
  | ByzHoldLock asset_id
  | ByzInjectInvalid dq_message

Message dropping, message reordering, lock withholding, invalid transition injection. Each requires an individual blocking proof. byzantine_cannot_forge_transition proves that invalid transitions are blocked by reg_transition, and byzantine_lock_bounded proves that even Byzantine-held locks are released by timeout.

Two-File Structure: Separating the Universal from the Instance

The design pattern from Property 1 repeats in Property 2. The structure of State_Preservation.thy (universal) and Regulatory_Instance.thy (instance) extends into Priority_Resolution.thy (universal) and DQuencer_Instance.thy (instance).

The core principle of this two-file structure is import independence. Priority_Resolution.thy imports only Main and never imports Regulatory_Instance.thy. It defines universal locales and proves universal theorems while knowing nothing about the regulatory domain.

DQuencer_Instance.thy is the junction that merges both worlds. It imports both Priority_Resolution and Regulatory_Instance, instantiating the universal locales into the regulatory domain and combining them with Property 1’s model.

theory DQuencer_Instance
  imports Priority_Resolution Regulatory_Instance
begin

This structure is academically significant because the three universal locales of Priority_Resolution.thy can be independently reused outside the regulatory domain.

priority_system: Deterministic selection based on total order over a finite message set. Applicable to DeFi transaction ordering, MEV auctions, and distributed scheduler task prioritization.

deadlock_free_locking: Deadlock freedom under finite resources, locks, and timeouts. Applicable to distributed database locks, file system locks, and distributed cache locks.

fair_leader_system: Starvation freedom under fair leader election assumptions. Applicable to leader-based consensus systems (Raft, PBFT variants), round-robin schedulers, and fair queuing systems.

Just as State_Preservation.thy‘s four universal locales from Property 1 became a reusable standard for cross-domain state preservation, Priority_Resolution.thy‘s three universal locales can serve as a reusable standard for distributed system liveness properties.

Figure 3: Two-File Structure and Import Independence

Academic Significance of Universal Proofs

The decision to include Byzantine environments is not simply about “attempting a harder proof.” The key point is that the structure itself, separated into universal locales, constitutes an independent academic contribution.

Existing blockchain formal verification research, such as Tendermint’s TLA+ specification or Ethereum 2.0’s Beacon Chain modeling, was written tightly coupled to each specific protocol. As a result, reusing proof results for other protocols required substantial remodeling.

Priority_Resolution.thy takes a different approach. None of the three locales presuppose a specific consensus algorithm or domain. priority_system requires only the mathematical structure of “deterministic selection based on total order over a finite set.” deadlock_free_locking requires only the general abstraction of “finite resources, locks, and timeouts.” fair_leader_system requires only the minimal assumption of “periodic honest leader election.”

If this separation is realized, the theorems of Priority_Resolution.thy apply not only to D-quencer but to any distributed system satisfying the same structural properties, without additional proofs and through locale instantiation alone. DeFi protocol transaction ordering, distributed database lock management, and fairness guarantees in leader-based consensus systems could all obtain the same assurances.

Just as State_Preservation.thy‘s four universal locales became a “certification standard” for cross-domain state preservation in Property 1, the three universal locales of Priority_Resolution.thy aim to become a “certification standard” for distributed system liveness properties. For this goal to be realized, proofs must be completed, registered in AFP, and peer-reviewed. A long road remains.

Byzantine Fault Verification for Consensus Algorithms: No Precedent

One more contextual point deserves attention. To our knowledge, formally verifying a consensus algorithm in the regulatory domain with Isabelle/HOL has no precedent.

Formal verification of consensus algorithms is an active research area. Tendermint was specified in TLA+, Gasper (Ethereum 2.0) was partially verified in Dafny, and PBFT’s safety was proven in Coq. However, these efforts verified universal properties of general-purpose consensus algorithms. No case has been identified where a system with regulatory action priority as domain logic intrinsic to the consensus process was formally verified.

And this domain logic is precisely what elevates the difficulty. In general-purpose consensus, “which value to agree on” lies outside the consensus algorithm’s concern. Value semantics are handled above the consensus layer. In D-quencer, however, the priority of the regulatory actions being agreed upon affects the consensus process itself. When an international body’s CONFISCATE and a regional body’s FREEZE arrive simultaneously, “which value to select” must be determined within the consensus algorithm. Value semantics penetrate the consensus layer.

Formalizing this structure in Isabelle/HOL requires the consensus model and the domain model (regulatory state transitions) to be combined within a single proof context. The design where DQuencer_Instance.thy imports both Priority_Resolution.thy (consensus side) and Regulatory_Instance.thy (domain side) reflects precisely this requirement.

Whether this attempt succeeds can only be known once the proof is complete. The absence of precedent means there are no reference patterns, and unanticipated obstacles may emerge. But just as the solution for multi_domain_preservation locale instantiation was discovered during Property 1, we expect that the process of trial and failure in Property 2 will similarly lead to design improvements.

What Changes from the Property 1 Model

Property 2 does not break Property 1’s model but extends it. The existing reg_state, reg_action, reg_transition, global_state, sync, and valid_state are used as-is. Changes are confined to four areas.

First, the regulatory authority identifier, previously abstracted as msg_authority :: nat, is formalized into a concrete hierarchical structure.

datatype authority_level = International | National | Regional

fun authority_rank :: "authority_level ⇒ nat" where
  "authority_rank International = 3"
| "authority_rank National = 2"
| "authority_rank Regional = 1"

International bodies outrank national, and national outrank regional. This is a core principle of the RCP framework. It reflects the legal reality where FATF blacklists take precedence over individual national regulations.

Second, regulatory actions are assigned severity rankings. CONFISCATE (7) is most severe; UNRESTRICT (1) is least. This formalizes the legal principle that “the more conservative, i.e. more asset-protective, action takes priority.”

Third, the oss_message record is extended.

record dq_message = oss_message +
  msg_authority_level :: authority_level
  msg_source_node     :: nat

A to_oss_message conversion function enables the extended message to be passed to the existing sync function.

Fourth, the D-quencer node model and the dquencer_system locale are newly introduced. This locale, parameterized by the node set, Byzantine upper bound, timeout, fairness bound, and maximum timestamp, defines the overall proof context for Property 2.

Correspondence with Canton CPP 2021

Andreas Lochbihler and Joshua Schneider of Digital Asset presented their Merkle Functor verification at CPP 2021, proving authenticated data structure preservation within Canton. Their paper mentioned verification in Byzantine environments as a “Next step.”

Property 2 performs this Byzantine environment verification with the same tool (Isabelle/HOL), on a different domain (regulatory state synchronization). If Canton proved state preservation within Canton’s boundaries, Oraclizer is proving state preservation across Canton’s boundaries to EVM chains. Once Property 1 proves safety and Property 2 proves liveness, it becomes technically feasible for Property 3 to import Canton’s AFP-registered theorems for composition.

This is an ambitious goal, and only upon completion of Property 2 can the feasibility of this path be concretely assessed.

Anticipated Challenges

During the modeling design process, four technical challenges were identified.

Record inheritance type compatibility. Whether the subtype relationship in Isabelle’s record dq_message = oss_message + ... connects smoothly with the existing sync function requires verification. Isabelle’s record inheritance is well-supported, but subtype coercion registration may be necessary, and failure would require explicit conversion functions.

Timestamp sign inversion. The max_ts - ts construction implementing “earlier = higher” causes nat underflow if max_ts < ts. The defense is to add max_ts ≥ ts as a locale assumption.

priority_injective proof. One of the core assumptions of the priority_system locale is that distinct messages have distinct priorities. Proving this for D-quencer requires showing that the 4-tuple’s last element, node_id, acts as a tiebreaker. Messages from the same node differ in timestamp or action; messages from different nodes differ in node_id; therefore, priority is globally unique.

Closed-system assumption. The non_honest_bounded assumption of fair_leader_system presupposes that no new requests arrive during the analysis interval. This limitation must be explicitly recorded in the proof and transparently disclosed.

If there is one lesson from the Property 1 experience, it is that such challenges sort themselves into those resolvable during the proving process and those that are not, and the real challenges emerge where they are least expected. The impact of excluding the SEIZED→FROZEN transition on proof complexity was not predicted in advance. Similar discoveries are expected in Property 2.

Design Constraints the Proof Will Yield

One practical value of formal verification is that the proving process yields mathematical constraints on system parameters. In Property 1, the finiteness assumption finite connected_chains was a key constraint. Property 2 is expected to yield more concrete parameter constraints.

Parameter	Expected Constraint	Implementation Mapping
timeout T	T > 0 (minimum); in practice T > 2δ + ε	D-quencer timeout config
minimum node count n	n ≥ 3f + 1	network minimum requirement
fairness_bound k	k > 0; VRF guarantees honest leader within k epochs	VRF + leader rotation

These constraints will be directly utilized as “design guidance derived from proofs” in Phase 4 (D-quencer implementation).

Closing

The natural-language specification of Property 2 can be stated as follows: “Even when conflicting regulatory actions arrive simultaneously, even with Byzantine nodes (at most f < n/3), D-quencer’s priority resolution is deterministic, no deadlock occurs, and no asset is trapped in the system forever.”

Once proven, combined with Property 1, the following is established: in a decentralized environment with Byzantine nodes, cross-domain regulatory state is synchronized deterministically, without halting, without neglect. This is the ultimate goal of Property 2’s Byzantine fault verification.

The next post will enter the actual Isabelle/HOL code for Priority_Resolution.thy and DQuencer_Instance.thy. It will cover the concrete definitions of the three locales, Byzantine node modeling, and the instantiation process for the priority function.

---

References

[1]. Lochbihler, A., Schneider, J. (2021). Mechanizing a Verified Merkle Tree in Isabelle/HOL. CPP 2021. https://dl.acm.org/doi/10.1145/3437992.3439921

[2]. Nipkow, T., Paulson, L., Wenzel, M. (2002). Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer. https://isabelle.in.tum.de/doc/tutorial.pdf

Learn More

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

Proving Cross-Domain State Preservation: The Journey

Oraclizer Formal Verification (GitHub)