Bridging Safety and Liveness: A Prelude to Compositional Verification

TL;DR

With the mechanized proofs of Cross-Domain State Preservation and D-quencer Liveness under Byzantine Faults now complete, one question remains: how should the two be composed? A connecting theorem already exists between them, named combined_safety_liveness, but it guarantees only conditional safety. This next step is not a mechanical stitching of two results. It is an assume-guarantee operation in which one property’s assumption is discharged by the other property’s guarantee, and we stand at a design crossroads regarding both the level of abstraction and the strength of the final conclusion. This post records the thinking before the design is finalized. The finalized structure belongs to the next post.

Two Independent Proofs, and the Gap Between

The two Isabelle/HOL proofs we released are each independent statements. The first formalizes cross-domain state preservation as a functor pattern. The second addresses determinism and progress in a Byzantine environment. They coexist in the same repository, but strictly speaking they are two separate sentences.

The problem is that describing the Oraclizer system requires a single sentence. To answer the question “under what conditions does cross-domain state preservation hold in a Byzantine environment?”, we need a structure in which each proof fills the gaps of the other. This is what compositional verification originally means.

This post is a record of exploration about how to construct that composition. The design is not yet finalized. Several directions are being examined in parallel, and what follows is the reasoning behind the direction we are leaning toward along with the open concerns that still remain. Because this is pre-design reflection rather than post-proof retrospection, this post belongs to the earliest stage of our research journal.

The Limits of the Existing Bridge Theorem

Interestingly, the two proofs have already been bridged once. At the bottom of DQuencer_Instance.thy sits the following theorem:

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'"

This theorem emerged naturally after the second property was complete. It confirms in a single statement that the preservation invariant coexists with deterministic progress. As documented in our previous post, this theorem already represents unconditional safety and liveness along one axis: the honest-node axis, since Property 2 discharged the single-entity OSS abstraction that Property 1 had relied on.

But another axis remains. This theorem is still a conditional safety result in a second sense. It takes valid_state gs as a precondition, and only claims its result under that precondition. What this post examines is what remains conditional along that second axis: the requirement that the system already start in a valid state.

Why is this insufficient? The question a regulatory-compliant oracle state machine actually faces is broader than “does an already-valid state stay valid?” The system may start from an arbitrary configuration, a partially inconsistent state, or a state where only some domains have synchronized. What we ultimately want to assert is that from any such starting point, the system converges to a valid state.

The second limitation appears on the progress side. The liveness result was proved inside the fair_leader_system locale, which assumes honest_progress. That is, the property “when an honest leader is scheduled and pending > 0, the pending count strictly decreases” is injected externally.

An important distinction here. This honest_progress is a finer-grained assumption sitting inside the fair_leader_system locale, and it is not the same as the honest-node abstraction that Property 2 already discharged at the system level. The previous discharge replaced Property 1’s “OSS as a single honest entity” with a Byzantine node population bounded by f < n/3. What remains external here is a different kind of property entirely: an internal scheduling assumption that honest leaders, once scheduled, produce strict progress. This assumption itself must be derived from the BFT consensus structure for our claim to close.

To summarize: we need to elevate conditional safety into unconditional convergence, and we need to discharge an external assumption into an internal system property. These are the two jobs this composition undertakes.

Figure 1: The Gap Between Conditional Safety and Unconditional Convergence

Compositional Verification via Assume-Guarantee

There are several ways to bridge two proofs. The most mechanical approach is to conjoin the conclusions of both theorems. This is precisely what combined_safety_liveness already did. But this approach performs no assumption discharge. The assumptions of both proofs accumulate unchanged, producing a weaker conclusion under stronger preconditions.

The direction we intend to take is assume-guarantee reasoning. It has been the standard pattern in distributed-systems verification since Abadi and Lamport [1]. The core idea: if one property’s assumption can be supplied as another property’s guarantee, then in the composed result that condition is no longer an assumption but an internal property.

The first property guarantees cross-domain preservation under the honest-node assumption (equivalently, under successful lock acquisition). The second property guarantees deterministic progress in a Byzantine environment under the fair_leader assumption. When we bridge them, we build a structure in which the progress guarantee of liveness repeatedly discharges the honest-node precondition of safety. The composed result then holds without the honest-node assumption. This is where conditional safety is transformed into unconditional convergence.

The structure looks clean, but in practice three difficulties appear. First, the state space of the safety side and the schedule space of the liveness side live in different types. A glue layer is required to connect them. Second, deriving fair_leader from the BFT structure involves an abstraction from a probabilistic statement to a deterministic one, so complete discharge is impossible. We need to set a boundary for how far weakening can go. Third, what form should the composed theorem’s conclusion take? That is the subject of the next section.

The Crossroads of Abstraction Level

Early-stage whiteboards carry more erasure marks than final notation. What you erase matters as much as what you write.

The first substantive decision in this compositional verification design is the abstraction level of the composition locale. Three candidates exist.

The most concrete approach is to stitch the existing locales together directly. Define a single composition locale that has state_preservation and fair_leader_system as sublocales, and prove the composition theorem within it. The advantage is maximum reuse of existing proofs. The disadvantage is that the range of reusability is confined to the narrow domain of “state transitions plus priority-based consensus”.

At the opposite end sits the most abstract approach. Remove concrete concepts like priority, leader, and epoch entirely, and abstract into two pure locales. The first, guarded_invariant, describes a system where an invariant is preserved under a guard predicate. The second, eventual_discharger, describes a schedule in which guard-releasing events occur within a bounded window. Their composition is declared as safety_liveness_composition. In this approach, words like priority, Byzantine, or blockchain do not appear in the definitions. The locales become instantiable in entirely different domains such as replica convergence in distributed databases, path stabilization in routing protocols, or scheduling in container orchestration.

There is also a middle position. Keep the composition locale abstract, but add a concrete intermediate instance layer to reduce the cost of sublocaling the existing locales.

The direction we are currently leaning toward is maximum abstraction. The basis is the breadth of academic contribution. There is a meaningful difference in citation potential and extensibility between proving a specific system’s composition method and proving a general distributed-systems composition framework of which Oraclizer is one instance. The trade-off is increased proof complexity, but the locale-construction patterns we developed across the previous two proofs are settled enough to absorb this cost.

That said, the core risk of maximum abstraction lies in the design of the realize predicate. This is a type-polymorphic function describing “when an event occurs, which guarded operation does it manifest as?”, and it must correspond naturally to priority_system’s select_highest in the concrete instance. If type lifting does not go through smoothly, the design can stall at the instantiation step. The verdict on this depends on actually building a skeleton in Isabelle.

An honest self-check is warranted here. Is this abstraction simply over-design aimed at widening academic contribution? Once priority, leader, and other concrete notions are removed, does what remains become a hollow shell? The criterion for this judgment is clear. For an abstraction to be worthwhile, it should instantiate naturally into at least two genuinely different concrete domains. For now, alongside Oraclizer we are considering adjacent domains such as distributed database replication and the reconciliation loop of a Kubernetes controller. If actual instantiation succeeds only in one domain, this is over-engineering, and reverting to the concrete approach is the correct call. That judgment is one step beyond design finalization, at the actual instantiation attempt.

Another Axis: Canton’s ADS_Functor

Another unavoidable question in composition design is the relationship with Canton. This is partly a matter of the project’s narrative identity and partly a technical dependency. Narratively, Oraclizer is positioned as the on-chain extension of DAML’s built-in regulatory philosophy. It carries the authority structure and privacy guarantees assured inside Canton out to public chains. Technically, Lochbihler and Marić’s Merkle Functor formalization is publicly available as the ADS_Functor entry on the Archive of Formal Proofs, and it has already proven the authenticated-data model of Canton’s transaction tree in Isabelle/HOL [2].

What we want to prove and what Lochbihler proved live on different axes. They handle the authenticity of data structures, that is, the consistency of hashes and inclusion proofs. We handle the preservation of state transitions, that is, whether the same asset’s regulatory state evolves coherently across domains. The two axes can intersect. If the data authenticity carried by an authenticated transaction tree inside Canton is preserved along the cross-domain sync path, this means that when a Canton user interacts with external chains through Oraclizer, the guarantees Canton provided are not broken.

Verifying the actual structure of the Merkle_Interface locale surfaced an interesting observation. The locale fixes three components: a hash function h, a blinding relation bo, and a partial merge operation m. The blinding relation corresponds directly to Canton’s need-to-know privacy model. It expresses the relation between a system that knows the full data and one that knows only a part of it. How exactly this plays into our composition is not yet settled. The baseline plan is to establish a glue predicate stating that when two authenticated values are merged, the cross-domain state view extracted from them must stand in a consistent join relation. The precise definition will be finalized after Lochbihler provides a sanity check.

The Strength of the Conclusion

The shape of the composed theorem’s conclusion is itself a crossroads. The weakest claim sits at the level of combined_safety_liveness: preservation under a valid_state precondition. The middle is eventuality: starting from a valid state, the system reaches the next valid state within finite time even under Byzantine scheduling. The strongest claim is guarded bounded convergence: starting from an arbitrary global state, in an environment where regulatory intervention is admitted, the system converges to a valid state along a finite measure.

The third claim is the direction we intend to take. It is close to Dijkstra’s self-stabilization literature [3], or more precisely an assisted-self-stabilization variant in which external conflict-resolving actions are permitted. Academically this belongs to a well-studied family in the self-stabilization line since Dolev [4], but mechanized proofs of this convergence strength in the specific domain of blockchain regulatory consensus remain rare.

The central difficulty in the actual proof lies in defining the inconsistency measure. We need a well-founded measure that captures how far the system is from valid_state. The form currently under examination is the count of inconsistent chain pairs, that is, the number of ordered pairs of chains holding the same asset with different regulatory states. The definition itself is simple, but proving a lemma that each regulatory action strictly decreases this measure is the critical path of the design.

Should Isabelle demand a counterexample at that step, structuring the conclusion around the middle-strength claim (eventuality) remains a viable alternative formulation. Because the entire design does not collapse but only the strength of the conclusion drops by one step, sufficient design flexibility is preserved.

To be candid, the most uncertain point in this design is whether the inconsistency measure strictly decreases for every regulatory action. For instance, between chains where some have FREEZE applied and others remain in ACTIVE, could a conditional release action (UNFREEZE, UNRESTRICT, RELEASE) temporarily increase the measure? Intuitively, a release action propagated to only some chains first could momentarily raise the count of inconsistent pairs in the intermediate state. The measure change must be decomposed per action type and verified case by case. If Isabelle demands a counterexample here, the design will be adjusted to narrow the conclusion to a weaker claim. The reason for writing this vulnerability into the post in advance is twofold. If the proof succeeds, we can trace precisely which lemma resolved the concern in the next post. If it fails, we can document honestly that the failure point was exactly where we anticipated it, which becomes material for design reflection.

The Composition.thy Draft

At this point, the shape of Composition.thy looks roughly as follows. This is a sketch, and it will be adjusted once actual proving begins.

locale guarded_invariant =
  fixes carrier :: "'s set"
    and step :: "'s ⇒ 'op ⇒ 's option"
    and ops :: "'op set"
    and inv :: "'s ⇒ bool"
    and guard :: "'s ⇒ 'op ⇒ bool"
  assumes ...

locale eventual_discharger =
  fixes schedule :: "nat ⇒ 'event"
    and discharges :: "'event ⇒ bool"
    and window :: nat
  assumes ...

locale safety_liveness_composition =
  safe: guarded_invariant ... +
  live: eventual_discharger ...
  for ... +
  fixes realize :: "'event ⇒ 's ⇒ 'op option"
  assumes ...

In the third locale, realize is the design’s glue point. It is a function that maps events on the schedule to operations actually performed at the current state, with an additional assumption ensuring that this function only produces operations that satisfy the guard. In this structure, the final theorems take roughly the following form.

theorem unconditional_invariant_eventuality:
  assumes start: "s ∈ carrier" and inv_start: "inv s"
  shows "∃t s'. evolves_to s t s' ∧ inv s'"

theorem bounded_convergence_from_arbitrary:
  assumes start: "s ∈ carrier"
    and measure_wf: "wf (measure_order inv)"
  shows "∃t ≤ bound s. ∃s'. evolves_to s t s' ∧ inv s'"

The latter is what we aim for. The former is the more conservative claim we can secure alongside.

Figure 2: Composition.thy Locale Hierarchy (Draft)

Remaining Open Points

Our compositional verification design has three still-unresolved points.

First, the precise shape of the glue predicate. How should the correspondence between Merkle_Interface’s merge operation and cross-domain state join be specified? Intuitively, the extract function should map the result of merging two authenticated values to a consistent join of the state views extracted from each. But under what conditions this correspondence holds in Canton’s semantics requires review by the original author of ADS_Functor.

Second, how far can the fair_leader assumption be derived from the BFT structure? Full derivation is impossible because it involves abstracting a probabilistic property into a deterministic one. Where is the frontier below which we derive, and above which we defend as a methodological assumption in the Heard-Of model tradition [5, 6]? Setting this boundary is the most delicate part of what will go into the academic paper’s scope statement.

Third, the well-founded decrease of the inconsistency measure. Do all regulatory actions strictly decrease the measure in every case, or only for specific action types, and if there are non-decreasing actions, what effect do they have on liveness? This part will only become clear once concrete instance proofs begin.

Next Steps

This post recorded the thinking before the compositional verification design finalizes, continuing from where our previous retrospective on D-quencer liveness left off. The finalized structure, the final form of the locales, and the statements of the main theorems belong to the next post. The counterexamples and adjustments Isabelle will hand back to us during proving belong to the one after that.

When the composition is complete, four artifacts are released together. An assumption discharge specification tracing how the honest-node precondition gets discharged. A residual assumption list mapping assumptions that still remain after composition to the release paths of subsequent properties. A roadmap breaking down open questions like partially synchronous network models and open systems. And a draft scope statement for the academic paper. These artifacts matter as much as the composition proof itself, because no composition is complete, and clarifying the boundary between what we removed and what we kept is a condition of academic honesty.

A question for the reader. Could this compositional verification approach become an abstraction applicable outside blockchain systems? We have two scenarios in mind. First, in replicated databases, when a primary node behaves Byzantinely, under what guards do secondary nodes reach eventual consistency? Structurally this is identical to ours (safety: primary consensus, liveness: periodic failover). Second, in the Kubernetes controller reconciliation loop, does the drift between desired and actual state converge within bounded time? This also takes the form of guards (permission checks, admission control) plus eventual discharge (controller tick), mapping directly onto our guarded_invariant and eventual_discharger pair. If our safety_liveness_composition locale instantiates naturally in both domains, this work becomes a general verification methodology for distributed systems rather than a blockchain-specific one. If not, it is right to lower the abstraction level by one step. Either way, the answer will come only after actual instantiation is attempted.

References

[1] Abadi, M., & Lamport, L. (1995). Conjoining Specifications. ACM Transactions on Programming Languages and Systems, 17(3), 507-534.

[2] Lochbihler, A., & Marić, O. (2020). Authenticated Data Structures as Functors in Isabelle/HOL. FMBC 2020, OASIcs vol. 84, pp. 6:1-6:16. Archive of Formal Proofs entry: ADS_Functor.

[3] Dijkstra, E. W. (1974). Self-stabilizing Systems in Spite of Distributed Control. Communications of the ACM, 17(11), 643-644.

[4] Dolev, S. (2000). Self-Stabilization. MIT Press.

[5] Charron-Bost, B., & Schiper, A. (2009). The Heard-Of Model: Computing in Distributed Systems with Benign Faults. Distributed Computing, 22(1), 49-71.

[6] Wanner, A., Goncalves, M., & Yin, K. (2020). A Formally Verified Protocol for Log Replication with Byzantine Fault Tolerance. IEEE SRDS 2020.

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

Learn More

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