TL;DR
Cross-domain state preservation — “a state transition on one domain is reflected identically across all linked domains” — is an intuitively clear claim. But turning intuition into something provable demands ruthless precision about what we mean, what we assume, and what we abstract away. This article documents the completion of Phase 1: semi-formal specification for Property 1 of our formal verification project, with regulatory states as the first verification instance. We define five regulatory states and seven actions as a finite state machine, fix a partially synchronous network with honest nodes, and introduce the preemptive locking mechanism that serializes concurrent regulatory actions. The most consequential design decision was renaming the Regulatory State Functor to the Cross-Domain State Preservation Functor — not cosmetic rebranding, but a structural recognition that the functor we need is a generic locale for state preservation across domains, of which regulation is one instance. This article traces the path from natural language to mathematical precision, including every design decision, rejected alternative, and open question encountered along the way.
From Intuition to Precision
In the previous article, we established why Isabelle/HOL is an essential expression language for our problem. The need to quantify over state transition functions themselves placed us beyond the expressiveness of first-order logic, and Higher-Order Logic was the minimal extension that crossed that boundary. We also presented a design hypothesis we called the Regulatory State Functor.
Now comes the next step. Having chosen the tool, we must define precisely what we intend to prove.
“FREEZE → all chains FROZEN” — this sentence is intuitively clear. But for it to become a proof target, the intuition must be converted into a mathematical proposition. In that conversion process, we discovered a surprising number of decisions that needed to be made.
How many states are there? Which transitions are permitted and which are forbidden? Is the network synchronous or asynchronous? Are nodes honest or Byzantine? What exactly does “within bounded time” mean? How are two regulatory actions arriving simultaneously for the same asset handled?
This article shares our answers to all of these questions — the semi-formal specification completed in Phase 1. Semi-formal here means an intermediate point between natural language and mathematical notation. The full translation into Isabelle/HOL code (Phase 2) is the next stage, but this specification must be fixed before code writing becomes meaningful.
The State Space: What Can an Asset Be?
The first decision in a regulatory state model is defining the state space.
We define the set of possible regulatory states for a single tokenized asset as five:
$$\text{RegState} = \{ \text{ACTIVE}, \text{FROZEN}, \text{SEIZED}, \text{CONFISCATED}, \text{RESTRICTED} \}$$
The legal meaning of each state is precise. ACTIVE is the normal state where all transactions are permitted. FROZEN is a temporary trading halt, reversible by a regulatory authority’s release order. SEIZED represents court-ordered custodial hold — ownership is retained but control is lost. CONFISCATED is permanent forfeiture of ownership, and this leads to a critically important design property: CONFISCATED is a terminal state. No regulatory action can exit this state. RESTRICTED is a partial control state where transactions are permitted only under specific conditions.
Here the first abstraction decision arises. Oraclizer’s full regulatory action taxonomy includes six actions, but two of them — RECOVER and LIQUIDATE — are not state transitions. RECOVER is a force transfer operation that moves balances rather than changing states. LIQUIDATE is a compound operation requiring external DEX calls. Neither changes regulatory “state,” so both fall outside this model’s scope.
This decision is a classic abstraction tradeoff: narrowing the model’s scope in exchange for proof clarity. We chose the narrower scope because this model addresses only cross-chain consistency of regulatory states — balance movements and market operations belong to separate verification domains.
The Transition Table: Which Moves Are Legal?
Once the state space is defined, the next task is fixing the permitted transitions. This appears simple, but it is where the most meaningful design decisions emerged.
The transition function is defined as:
$$\text{transition} : \text{RegState} \times \text{RegAction} \to \text{RegState option}$$
The option type is used because not every (state, action) combination is valid. Invalid combinations return None.
Regulatory actions consist of five forward actions and three reverse actions:
$$\text{RegAction} = \{ \text{FREEZE}, \text{SEIZE}, \text{CONFISCATE}, \text{RESTRICT}, \text{UNFREEZE}, \text{UNRESTRICT}, \text{RELEASE} \}$$
Modeling reverse actions (UNFREEZE, UNRESTRICT, RELEASE) as separate actions was an intentional decision. Lifting a restriction is itself an explicit regulatory act, not simply “undoing” the original action. This distinction carries legal significance — freezing and unfreezing require different legal bases and procedures.
The complete transition table:
| Current State | Action | Next State |
|---|---|---|
| ACTIVE | FREEZE | FROZEN |
| ACTIVE | SEIZE | SEIZED |
| ACTIVE | CONFISCATE | CONFISCATED |
| ACTIVE | RESTRICT | RESTRICTED |
| FROZEN | UNFREEZE | ACTIVE |
| FROZEN | SEIZE | SEIZED |
| FROZEN | CONFISCATE | CONFISCATED |
| SEIZED | RELEASE | ACTIVE |
| SEIZED | CONFISCATE | CONFISCATED |
| RESTRICTED | UNRESTRICT | ACTIVE |
| RESTRICTED | FREEZE | FROZEN |
| RESTRICTED | CONFISCATE | CONFISCATED |
| CONFISCATED | (any) | (invalid) |
Three key invariants emerge from this table:
I1 (Terminal State): No action can exit CONFISCATED. Once assets are permanently forfeited, no system path exists to restore them.
I2 (Universal Reachability of CONFISCATE): CONFISCATE is applicable from every non-terminal state. Legally, forfeiture must be enforceable regardless of the asset’s current regulatory status.
I3 (Determinism): The same (state, action) pair always yields the same result. Nondeterminism is not permitted in regulatory state transitions.
Figure 1: Regulatory State Transition Diagram
The SEIZED→FROZEN Question
The most interesting question during transition table design was whether to permit a direct transition from SEIZED to FROZEN. Intuitively, a scenario where a court “relaxes” seizure to a simple freeze seems plausible.
We decided to exclude this transition. The reasoning is both legal and technical.
Legal basis: SEIZED is a stronger constraint than FROZEN. “Relaxing” from court-ordered custodial hold to a simple trading halt does not align with established legal practice. If seizure needs to be lifted, the path is RELEASE → ACTIVE, followed by a separate FREEZE if needed (a two-step path: RELEASE → ACTIVE → FREEZE).
Design benefit: Minimizing transition paths directly reduces proof complexity. By limiting exits from SEIZED to just two — RELEASE (→ACTIVE) and CONFISCATE (→CONFISCATED) — case analysis for this state becomes concise.
By similar logic, a direct FROZEN → RESTRICTED transition is also excluded. Only the path FROZEN → UNFREEZE → ACTIVE → RESTRICT is permitted. In practice, lifting a freeze before imposing restrictions is the natural regulatory procedure.
The common principle behind these decisions is minimization of transition paths. Fewer permitted paths means fewer proof cases and higher system predictability. This does mean some regulatory actions require two-step sequences in practice, but executing both steps atomically within a single transaction makes the practical constraint negligible.
The Global State: Modeling a Multi-Chain World
Beyond a single asset’s state, we need to model global state across multiple chains. This is where abstraction decisions characteristic of formal verification emerge.
A single asset’s state:
$$\text{AssetState} = \{ \text{asset\_id}, \text{reg\_state}, \text{owner}, \text{locked} \}$$
Fields like balance, metadata, and kycStatus are all excluded as irrelevant to regulatory state transitions. The owner field is included to express ownership transfer during CONFISCATE but its concrete address format is abstracted. The locked field is included to model preemptive locking.
Assets managed by a single chain:
$$\text{ChainState} = \text{AssetId} \to \text{AssetState option}$$
The option type is used because a given asset may not exist on a given chain. RWAs can span multiple chains, so which assets are registered on which chains is dynamic.
And the full system’s global state:
$$\text{GlobalState} = \{ \text{chains} : \text{ChainId} \to \text{ChainState}, \; \text{oss\_queue} : \text{Message list}, \; \text{locks} : \text{AssetId} \to \text{LockInfo option} \}$$
Including oss_queue in the global state is a deliberate simplification. In reality, OSS operates as a network of decentralized sequencer nodes, but in this first model it is abstracted as a single logical entity. The distributed processing and consensus mechanisms internal to OSS belong to Property 2 (D-quencer determinism and deadlock freedom). Separating concerns here keeps each property’s proof manageable.
Network Model: Choosing Partial Synchrony
The most fundamental assumption — the one that determines the meaning and scope of the proof — is the network model.
Three options exist. Synchronous: all messages are delivered within a known upper bound Δ. Proofs are simple but the assumption is unrealistic — no real blockchain network guarantees this. Asynchronous: no upper bound on message delivery. Closest to reality, but the Fischer-Lynch-Paterson (FLP) impossibility result [4] rules out deterministic consensus. Proving meaningful safety properties becomes extremely difficult. Partially synchronous: an upper bound Δ on message delivery exists but its value is unknown. Messages are eventually delivered.
We chose the partially synchronous model [1].
Understanding the implications of this choice precisely is important. Under partial synchrony, what we prove is not “all chains reach the same state simultaneously” but “all chains reach the same state within bounded time, eventually.” This is eventual state consistency — close to the strongest guarantee realistically achievable in distributed systems.
The specific assumptions under our partially synchronous network:
Messages have an upper bound Δ on delivery delay, but Δ is not known a priori. Messages are eventually delivered (eventual delivery). Message ordering is not guaranteed (out-of-order delivery is possible). Messages may be duplicated but cannot be forged (authenticated channels).
For the node model, we also made a deliberate choice. In this first model, all nodes honestly follow the protocol. Node crashes are permitted but malicious behavior is not. This is a restrictive assumption, but establishing the core property (homomorphism) under honest nodes before deciding on Byzantine extensions is strategically sound. Canton’s Merkle Functor also began with an “honest participants” assumption [2].
Preemptive Locking: Serializing Concurrent Regulatory Actions
The subtlest problem in cross-chain state synchronization is concurrency.
Consider this scenario. Asset X exists on Chain A and Chain B. Nearly simultaneously, regulatory authority α issues FREEZE on Chain A, and regulatory authority β issues SEIZE on Chain B. Without a locking mechanism, OSS might process both actions concurrently — Chain A transitions to FROZEN then to SEIZED, while Chain B transitions to SEIZED then attempts to transition to FROZEN. But SEIZED → FROZEN is a forbidden transition in our model.
This is what preemptive locking resolves.
The locking model’s assumptions: locks operate at the asset_id level (actions on different assets are independent), lock acquisition and release are atomic, and while a lock is held, other actions on the same asset_id enter a wait queue.
The synchronization workflow proceeds as follows. A regulatory action occurs on a source chain and emits an event. OSS receives the event and acquires a global lock on the target asset_id. OSS validates the transition via transition(current_state, action). If valid, state change messages are sent to all target chains. Each target chain applies the state change and returns an acknowledgment. When all acknowledgments are received, the lock is released and synchronization completes. If some acknowledgments are missing, the system retries after timeout or initiates rollback.
An important scope clarification is needed here. What this model’s locking mechanism prevents is state inconsistency from concurrent regulatory actions. Traditional double-spend prevention (balance/transfer models) is not within this model’s scope — balances and token transfers are excluded from the abstraction. Where Canton’s Merkle Functor proves properties of the transaction model itself (UTXO-style) [2], our model operates on top of that, addressing cross-chain consistency of regulatory state transitions.
What We Do NOT Assume
What a model does not guarantee matters as much as what it does. In formal verification, transparency of assumptions is directly tied to the credibility of proofs.
What this model does not cover:
Chain-specific characteristics such as gas costs, block production times, and finality delays are fully abstracted. A chain is simply a logical entity that stores states and receives messages.
Regulatory authority verification — whether a given authority has the right to perform a given action — is not checked. This falls within Property 2 (D-quencer priority determinism).
Financial operations including balances and token transfers are outside model scope.
Implementation correctness — the correspondence (refinement) between this model and Go/Solidity code — is not proved. The model verifies logical consistency of the design, not whether code faithfully implements the model. Those are separate verification domains.
We record this list explicitly to prevent overstatement of formal verification results. The claim “regulatory homomorphism is proved” is valid only within the context of these assumptions and non-assumptions.
The Threat Model
The threat model makes the negative of assumptions explicit — which attacks are considered and which are not.
| Threat | Included | Handling |
|---|---|---|
| Network delays | ✓ | Partially synchronous model |
| Message loss | ✓ | Retransmission mechanism |
| Message duplication | ✓ | Idempotency |
| Out-of-order messages | ✓ | Locking mechanism enforces ordering |
| Node crashes | ✓ | Retry/timeout |
| Byzantine nodes | ✗ | Outside first model scope |
| Chain reorganization | ✗ | Chain finality assumed |
| Bugs in OSS itself | ✗ | Model correctness is what we prove |
Excluding Byzantine nodes is a deliberate scoping decision. Byzantine environments sharply increase model complexity, and confirming that the core property (homomorphism) holds under honest conditions must logically precede any Byzantine extension. Whether to add Byzantine assumptions will be decided after Property 1 is complete.
The Property: Stated Precisely
We can now state the property to be proved with precision.
Informal: “When a state transition occurs on domain A, the same transition is reflected on all domains where the asset exists, within bounded time.”
Semi-formal:
$$\forall S : \text{GlobalState}, \; \forall a : \text{RegAction}, \; \forall \text{aid} : \text{AssetId}, \; \forall \text{src} : \text{ChainId},$$
$$\text{valid\_state}(S) \;\wedge\; \text{asset\_exists}(S, \text{src}, \text{aid}) \;\wedge\; \text{transition}(\text{get\_reg\_state}(S, \text{src}, \text{aid}), a) = \text{Some}(\text{new\_state})$$
$$\Longrightarrow$$
$$\exists S’, \; \exists t’ > t. \;\; \text{sync}(\text{src}, a, \text{aid}, S) = \text{Some}(S’) \;\wedge\; \left(\forall c \in \text{connected\_chains}(\text{aid}). \; \text{get\_reg\_state}(S’, c, \text{aid}) = \text{new\_state}\right)$$
In words: given a valid global state \(S\), if asset \(\text{aid}\) exists on chain \(\text{src}\) and regulatory action \(a\) produces a valid transition, then after synchronization, the regulatory state of that asset on every connected chain equals \(\text{new\_state}\). This is cross-domain state preservation instantiated for the regulatory domain.
Subsidiary properties expected to be needed for the proof:
A1: Determinism of the transition function — guaranteed by Isabelle’s fun definition itself.
A2: Terminal property of CONFISCATED — \(\forall a. \; \text{transition}(\text{CONFISCATED}, a) = \text{None}\)
A3: Mutual exclusion of locks — a locked asset_id blocks other sync operations.
A4: Idempotency of synchronization — applying the same action to an already-transitioned state returns None or produces no change.
Renaming the Functor: From “Regulatory State” to “Cross-Domain State Preservation”
In the previous articles, we called the core design idea of this verification project the Regulatory State Functor, and the property to be proved Cross-Chain Regulatory Homomorphism. During the process of designing the semi-formal specification, we came to recognize that these names unfairly narrow the scope.
Mid-stroke: crossing out “Regulatory State Functor” and writing “Cross-Domain State Preservation” — the most consequential naming decision in the specification phase.
What we are actually designing is not a functor limited to regulatory states. Its core structure — finite state sets, deterministic transition functions, permitted terminal states, structure preservation across cross-domain synchronization — is applicable to any state synchronization scenario with well-defined transition rules.
This is the lesson we take from Lochbihler‘s naming of the Merkle Functor [2]. Lochbihler created the functor to verify Canton’s authenticated data structures, but did not call it “Canton Transaction Functor.” By choosing the generic name Merkle Functor and defining Canton’s transactions as an instance, the naming decision enabled the functor to be registered as a general-purpose theory on the Archive of Formal Proofs (AFP) — an independent academic contribution not tied to any specific project.
We follow the same structure. The functor is renamed to the Cross-Domain State Preservation Functor, the property to Cross-Domain State Preservation Homomorphism, and the regulatory domain is defined as the first verification instance.
This change is directly reflected in the .thy file structure:
State_Preservation.thy: the generic locale — defining finite state sets, deterministic transition functions, terminal states, and natural transformation conditions as a chain/domain-independent theory.
Regulatory_Instance.thy: the regulatory domain instantiation — RegState, RegAction, the transition table, OSS message propagation model, preemptive locking, synchronization function, and the eventual state consistency proof.
Regulatory_Instance.thy
+ Composition.thy
Figure 2: Cross-Domain State Preservation Functor Architecture
The Generic Locale
The core constraints of the generic locale:
The state set is finite (\(|S| < \infty\)). The transition function is deterministic (same input, same output). Terminal states are permitted (states from which no transition is possible). The natural transformation condition holds: \(F_{\text{target}} \circ \text{transition} = \text{sync} \circ F_{\text{source}}\).
Any domain satisfying these constraints can be an instance of this locale. Regulatory states — with five finite states, deterministic transition rules, and CONFISCATED as a terminal state — form a natural instance.
But other scenarios with the same structure could also be defined as instances. Cross-chain synchronization of KYC certification states (PENDING → VERIFIED → EXPIRED → REVOKED), or game asset state synchronization (AVAILABLE → EQUIPPED → LOCKED → DESTROYED), would fit the same locale pattern.
This generality increases the academic contribution. Positioned not as “a functor only for regulatory states” but as “a generic pattern for cross-domain state preservation,” the work opens the possibility of broader recognition at venues like AFP or FMBC.
The Direct Proof Strategy
One thing to make clear: the generic locale structure is a design for extensibility, not a prerequisite for proving Property 1. The proof strategy follows a two-stage approach — complete the direct proof first, then layer the functor structure on top.
Stage 1: prove cross-domain state preservation homomorphism directly against the global state in Regulatory_Instance.thy, using regulatory states as the concrete instance. Stage 2: define the generic locale in State_Preservation.thy, prove that the regulatory instance satisfies locale constraints, and prove the functor laws.
The rationale for this ordering is practical. If the direct proof fails, the problem lies in the model itself — not in the functor abstraction. Confirming whether the functor structure successfully generalizes the proof into a more universal form is logically safer after the direct proof succeeds.
From Here to Isabelle/HOL
With the semi-formal specification fixed, the next step is translating it into Isabelle/HOL code — Phase 2, formal model construction.
The mapping plan is already concrete:
| Semi-formal concept | Isabelle/HOL encoding | .thy file |
|---|---|---|
| RegState | datatype reg_state = ACTIVE | FROZEN | ... | Regulatory_Instance.thy |
| RegAction | datatype reg_action = FREEZE | SEIZE | ... | Regulatory_Instance.thy |
| transition | fun reg_transition :: reg_state ⇒ reg_action ⇒ reg_state option | Regulatory_Instance.thy |
| State (generic) | locale state_preservation = fixes states :: "'s set" ... | State_Preservation.thy |
| GlobalState | record global_state = ... | Regulatory_Instance.thy |
| sync | definition sync :: ... | Regulatory_Instance.thy |
But tensions are already visible in this mapping. Should the partially synchronous network’s nondeterministic message delivery be expressed via fun (deterministic total function) or inductive (relational definition)? We discussed this tension theoretically in the previous article — now, at the point where it must be implemented as actual code, this decision will shape the entire proof strategy.
This becomes the central question of the next article — the design decisions encountered while translating semi-formal specification into actual .thy code, the gaps between expectation and reality, and the discoveries made along the way.
Conclusion
What this specification work confirmed is that the value of formal verification lies not only in the final theorem but in the process of writing the specification itself.
Starting from a single sentence — “FREEZE → all chains FROZEN” — we derived five states and seven actions, twelve valid transitions, partially synchronous network assumptions, honest node assumptions, a preemptive locking mechanism, and four subsidiary properties. Most importantly, the design decision that SEIZED→FROZEN direct transition is unnecessary was discovered at the intersection of legal analysis and proof complexity analysis — before writing a single line of code.
The transition from Regulatory State Functor to Cross-Domain State Preservation Functor — and correspondingly from Cross-Chain Regulatory Homomorphism to Cross-Domain State Preservation Homomorphism — was the most significant conceptual evolution in this process. We began with the specific motivation of regulatory state verification, but through the specification process discovered a more general abstraction — a pattern encompassing any cross-domain synchronization scenario with finite states and deterministic transitions. This is a structural decision that widens the scope of academic contribution without narrowing the scope of the proof.
Open questions remain. How best to express the partially synchronous network’s nondeterministic message delivery in Isabelle/HOL? How large is the practical gap between direct proofs and functor structure? And most fundamentally — will all these abstractions survive contact with actual proof attempts?
The next step confronts these questions directly.
References
[1] Dwork, C., Lynch, N. & Stockmeyer, L. (1988). “Consensus in the Presence of Partial Synchrony.” Journal of the ACM, 35(2), 288–323. https://doi.org/10.1145/42282.42283
[2] Lochbihler, A. & Marić, O. (2020). “Authenticated Data Structures As Functors in Isabelle/HOL.” In: FMBC 2020. OASIcs vol. 84, 6:1–6:15. https://doi.org/10.4230/OASIcs.FMBC.2020.6
[3] Nipkow, T. & Klein, G. (2014). Concrete Semantics: With Isabelle/HOL. Springer. http://concrete-semantics.org/
[4] Fischer, M.J., Lynch, N.A. & Paterson, M.S. (1985). “Impossibility of Distributed Consensus with One Faulty Process.” Journal of the ACM, 32(2), 374–382. https://doi.org/10.1145/3149.214121
[5] Lamport, L. (1998). “The Part-Time Parliament.” ACM Transactions on Computer Systems, 16(2), 133–169. https://doi.org/10.1145/279227.279229
Learn More
Read more on Oraclizer Research:
Higher-Order Logic as a Design Language: Why Our Verification Requires HOL — Why HOL is the essential expression language for our problem and core Isabelle/HOL constructs
Why We’re Starting Formal Verification: Applying Our Own Standard — Verification target properties, tool selection rationale, and the initial functor concept
From Isabelle/HOL to Compliance-Aware Infrastructure: Why RWA Needs Provable Compliance — Pattern 3 necessity and Digital Asset’s verification case study
