TL;DR
Oraclizer’s cross-domain state preservation theory has been mathematically proven. The complete proof has been submitted to the Archive of Formal Proofs (AFP), the world’s largest repository of machine-checked proofs operated by the Technical University of Munich and the University of Cambridge, and open-sourced as Oraclizer’s first official GitHub repository. A regulatory state change on one chain is faithfully preserved across every connected chain, verified for all possible cases by a machine-checked proof. This is not an audit. This is not a test. It is a mathematical proof where Isabelle/HOL’s theorem-proving kernel has exhaustively verified every logical path. No oracle project has done this before Oraclizer.
Why This Proof Matters
It is now routine for blockchain projects to publish security audit reports. But there is a fundamental difference between an audit and formal verification. An audit scans code for known vulnerability patterns. The absence of discovered vulnerabilities is not a proof that no vulnerabilities exist. Formal verification is different. It mathematically defines the properties a system must satisfy, then logically proves those properties hold for every possible input and every possible state. Not a single counterexample is tolerated.
In previous posts, we followed the proof journey of cross-domain state preservation: designing the locale hierarchy, formalizing the naturality condition, modeling the locking mechanism, and instantiating the multi-domain locale through a bridge function. That journey is now complete.
On February 28, 2026, every proof obligation in State_Preservation.thy and Regulatory_Instance.thy was verified by the Isabelle/HOL kernel. No sorry or oops remains. On March 25, the entry was submitted to AFP under the name Cross_Domain_State_Preservation, and on the same day we published Oraclizer’s first official GitHub repository.
State synchronization is a first-of-its-kind concept in blockchain history. Existing oracles were pipelines that relayed data in one direction; they were never systems that bidirectionally synchronized state between on-chain and off-chain environments. This proof guarantees that this new theory can work in a mathematically complete sense.
Yet completing a proof does not close every question. In fact, it is only after a proof is finished that the more honest questions become possible. What does this model actually guarantee? What does it not guarantee? How did the proof process itself improve the system’s design? And what does this proof mean for the ERC-TRUST token standard and cross-chain infrastructure as a whole?
This post answers those questions.
Cross-Domain State Preservation: Three Core Theorems
We begin with the final results. The technical structure consists of a two-file architecture: a generic theory (State_Preservation.thy) and a regulatory instantiation (Regulatory_Instance.thy). Three core theorems form the backbone of the entire proof.
Theorem 1: Regulatory Homomorphism
theorem regulatory_homomorphism:
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 synced: "sync source action aid gs = Some gs'"
and connected: "c ∈ connected_chains gs aid"
and fin: "finite (connected_chains gs aid)"
shows "get_reg_state gs' c aid = Some s'"
In plain language: given a valid global state, if a regulatory action (freeze, seize, confiscate, etc.) is applied to an asset on a source chain and synchronization succeeds, every chain holding that asset agrees on the new regulatory state.
This does not hold “most of the time” or “with high probability.” It holds for every possible global state, every possible chain configuration, and every possible regulatory action that satisfies the theorem’s assumptions. Without exception.
The proof proceeds by decomposing the sync function into lock, update_all_chains, and unlock, then showing that each phase correctly handles chain state. acquire_lock does not modify chain data; update_all_chains updates every connected chain to the new state; release_lock does not modify chain data. Combining these facts yields the conclusion.
Theorem 2: Valid State Preservation
theorem valid_state_preservation:
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 synced: "sync source action aid gs = Some gs'"
and fin: "finite (connected_chains gs aid)"
shows "valid_state gs'"
This theorem closes the inductive invariant. If valid_state holds at the initial state and sync preserves valid_state, then valid_state holds at every reachable state.
Why this matters: once the system starts in a valid state, no amount of synchronization operations can push it into an inconsistent state. Here valid_state is the conjunction of two properties. First, consistent_state: all chains holding the same asset agree on its regulatory state. Second, no_locked_without_reason: no outstanding locks remain after synchronization completes; the system returns to a clean state.
Separating these two properties was itself a discovery made during the proof process (detailed later in this post).
Theorem 3: Multi-Domain Parametric Instantiation
theorem reg_multi_domain_instantiation:
assumes fin_doms: "finite (doms :: chain_id set)"
and valid: "valid_state gs"
shows "multi_domain_preservation doms reg_states reg_actions
reg_transition reg_terminal (reg_domain_state gs)"
This theorem bridges the generic theory to the concrete model. Given any finite set of domains and a valid global state, the multi_domain_preservation locale is satisfied for the regulatory model. “Any finite set of domains” is the key phrase. Whether it is 3 chains, 30 chains, or 300 chains, the same guarantee applies as long as the set is finite. This is a parametric result, independent of any specific chain topology.
Through this instantiation, every generic theorem proved in State_Preservation.thy (cross_domain_consistency, sync_isolation, sequential_preservation) automatically applies to the regulatory model. No re-proving required.
A Generic Framework: Not Just for Oraclizer
The proof of Property 1 began as a way to verify Oraclizer’s regulatory compliance system. But there was a deliberate architectural choice in how the proof was structured: we built a domain-independent generic theory first, then defined the regulatory model as one instance of that theory.
The four locales in State_Preservation.thy know nothing about regulatory states. They know nothing about FREEZE or SEIZE. All they require are finite state sets, deterministic transition functions, terminal states, and the naturality condition on synchronization maps.
locale state_machine =
fixes states :: "'s set"
and actions :: "'a set"
and transition :: "'s ⇒ 'a ⇒ 's option"
and terminal :: "'s set"
assumes finite_states / finite_actions / transition_closed
/ terminal_absorbing / terminal_subset / transition_domain
On top of this sits state_preservation, which formalizes the naturality condition between two state machines. When the synchronization map commutes with transitions, synchronizing after a local transition yields the same result as transitioning after synchronization.
When this condition holds, preservation extends from single transitions to arbitrary-length action sequences. This is the sequential_preservation theorem.
theorem sequential_preservation:
assumes "s ∈ states⇩s"
and "∀a ∈ set as. a ∈ actions⇩s"
and "source.apply_actions s as = Some s'"
shows "target.apply_actions (state_map s) (map action_map as)
= Some (state_map s')"
If a valid action sequence exists at the source domain, the mapped sequence is also valid at the target domain and the final state is preserved through the mapping. Failure cases (None) are likewise preserved by sequential_preservation_none.
The third locale, symmetric_state_preservation, models bidirectional synchronization. When inverse maps exist with roundtrip guarantees, the state map is proven injective, guaranteeing no information loss during synchronization.
The fourth locale, multi_domain_preservation, generalizes to N domains. When N domains share the same abstract state machine and one domain transitions, sync_all brings every connected domain into agreement on the resulting state.
The implication of this generic framework is clear. Any team building cross-chain infrastructure can import these locales, define their own state model as an instance, and verify their system’s cross-domain state preservation to the same standard. Beyond regulatory states, any domain with finite states and deterministic transitions (game asset synchronization, supply chain state tracking, DeFi position management) can be verified on top of this framework.
We proved more than Oraclizer’s protocol. We created a certification standard for cross-chain state preservation. This is why the AFP entry is named Cross_Domain_State_Preservation: the regulatory domain is merely one instance of this generic framework.
The Regulatory State Machine: Transition Table and Invariants
Instantiating the generic framework for the regulatory domain is the first half of Regulatory_Instance.thy. The reg_transition function defines 35 (state, action) combinations across 5 states (ACTIVE, FROZEN, SEIZED, CONFISCATED, RESTRICTED) and 7 actions (FREEZE, SEIZE, CONFISCATE, RESTRICT, UNFREEZE, UNRESTRICT, RELEASE). Of these, 12 are valid transitions and 23 return None.
This transition table reflects design decisions grounded in legal precedence and operational logic.
RECOVER and LIQUIDATE are excluded from the state machine because they are force transfers. Recovering stolen assets or forcing liquidation are not transitions of regulatory state but forced transfers of ownership. Mixing state transitions and ownership transfers would break the model’s separation of concerns.
The direct transition from SEIZED to FROZEN is excluded because, legally, seizure is a strictly stronger constraint than freezing. “Relaxing” a court-ordered seizure to a mere freeze is legally nonsensical. The correct legal path is RELEASE to ACTIVE, then FREEZE if needed.
Three invariants are proven over this transition table.
I1: Terminal absorption. No action succeeds from the CONFISCATED state. Confiscation is a final measure and cannot be reversed.
lemma confiscated_terminal: "reg_transition CONFISCATED a = None"
I2: Universal confiscation. CONFISCATE is reachable from every non-terminal state. Regardless of the current regulatory state, the authority can always execute confiscation.
lemma confiscate_universal: "s ≠ CONFISCATED ⟹ reg_transition s CONFISCATE = Some CONFISCATED"
I3: No self-loops. No transition maps a state to itself. Every regulatory action produces a genuine state change.
lemma no_self_loops: "reg_transition s a = Some s ⟹ False"
Additionally, non_terminal_has_action shows that every non-terminal state has at least one valid action. Until the system reaches CONFISCATED, there is always a next step. There are no dead ends in regulatory enforcement.
These invariants matter not simply because they confirm the transition table’s correctness, but because they serve as the reference specification that the ERC-TRUST token standard’s Solidity implementation must match exactly. confiscated_terminal corresponds to the require(state != RegState.CONFISCATED) guard in Solidity, and confiscate_universal informs the precondition design of the CONFISCATE function.
The Synchronization Protocol: Lock, Update, Unlock
The second half of Regulatory_Instance.thy defines the global state model and synchronization protocol.
definition sync ::
"chain_id ⇒ reg_action ⇒ asset_id ⇒ global_state ⇒ global_state option"
where
"sync source action aid gs =
(case get_reg_state gs source aid of
None ⇒ None
| Some current_st ⇒
(case reg_transition current_st action of
None ⇒ None
| Some new_st ⇒
(case acquire_lock gs aid of
None ⇒ None
| Some gs_locked ⇒
let targets = connected_chains gs aid in
let gs_updated = update_all_chains gs_locked aid
new_st targets in
Some (release_lock gs_updated aid))))"
The structure of sync is clear: look up the asset’s current regulatory state on the source chain, verify the transition is valid, acquire a global lock (fail if already locked), update all connected chains to the new state, and release the lock. If any step fails, the entire operation returns None.
A clarification on the role of preemptive locking: it exists for concurrent regulatory action prevention. If two regulators simultaneously attempt FREEZE and SEIZE on the same asset, only one acquires the lock; the other fails. This is distinct from double-spend prevention, which concerns token balances and transfers and lies outside this model’s scope.
The lock_mutual_exclusion lemma formally guarantees this mutual exclusion.
lemma lock_mutual_exclusion: assumes "is_locked gs aid" shows "acquire_lock gs aid = None"
And sync_isolation guarantees that synchronization on asset A does not alter the state of asset B in any way.
The whiteboard after the final proof obligation cleared. What remains is not the process, but what the process revealed about the design itself.
Design Improvements Discovered During Proof
The most underrated value of formal verification is not the final proof itself but the design feedback generated during the proof process. When the prover rejects a proof obligation, it points precisely to where the design contains a weakness or ambiguity. We document three discoveries.
Discovery 1: Excluding SEIZED → FROZEN Significantly Reduces Proof Complexity
We debated whether to include this transition in the initial design. From a legal standpoint, seizure is a stronger constraint than freezing, so “relaxing” from seizure to a freeze is semantically unnatural. But the impact on proof complexity was larger than expected.
Allowing this transition would give SEIZED three outgoing transitions (RELEASE, CONFISCATE, FREEZE), increasing state-space branching and significantly complicating the case analysis in the sync_preserves_consistent_state proof. Excluding it secured both legal justification and formal simplicity simultaneously. To go from SEIZED to FROZEN, one must take two steps: RELEASE → ACTIVE → FREEZE, and each step is individually verified.
This is a case where formal verification functions not as a “post-hoc justification” of a design decision, but as a tool for evaluating the quality of design decisions proactively.
Discovery 2: Binary Decomposition of valid_state Cleaned Up Proof Structure
Separating valid_state into consistent_state and no_locked_without_reason had a decisive impact on proof structure. We initially tried defining a single monolithic invariant, but discovered that the preservation proofs for the two properties required independent reasoning during sync’s lock-acquire and lock-release phases.
sync_preserves_consistent_state needs to show that update_all_chains correctly updates connected chains, with the core argument splitting into the “synchronized asset” case and the “other asset” case. sync_preserves_no_locks needs to show symmetry between lock acquisition and release, with the core argument being that update_all_chains does not modify lock state.
These two proofs have different structures, and separating them makes each self-contained. This pattern is a general strategy for handling composite invariants and proves repeatedly useful when verifying complex systems in Isabelle/HOL.
Discovery 3: Separating Interpretation from Predicate Assumptions
When instantiating the generic locale with the concrete model, a conflict arose between the reg_sm already generated by interpretation and the state_machine predicate assumption expected by multi_domain_preservation. An interpretation injects locale theorems into the current context, but multi_domain_preservation takes state_machine as an opaque predicate assumption.
The solution was to create a separate lemma, reg_state_machine_pred, proving the state_machine predicate as a standalone fact. This pattern will apply identically when extending the model with D-quencer’s priority system in Property 2.
All three discoveries are things “learned from what the prover rejected.” This is the kind of feedback on a system’s logical structure that code review or auditing cannot easily provide.
Figure 1: Property 1 Theorem Architecture
What Cross-Domain State Preservation Guarantees
Let us unpack what the theorems actually mean in plain terms.
Regulatory state consistency. When a financial authority freezes a tokenized bond, every chain where that bond exists (Base, Arbitrum, Optimism, etc.) simultaneously transitions to the FROZEN state. Without exception. It is mathematically impossible for one chain to reflect the freeze while another chain allows the asset to remain tradeable.
Concurrent regulatory action prevention. If the SEC and FCA simultaneously issue different regulatory actions on the same asset, preemptive locking ensures only one succeeds while the other is serialized. It is impossible for two conflicting actions to apply simultaneously and push the state into contradiction.
Invariant preservation. Once the system starts in a valid state, no amount of synchronization operations can push it into an inconsistent state. Whether 100 regulatory actions or 10,000, state consistency is preserved.
Isolation. A regulatory action on asset A does not affect the state of asset B. Freezing bond X leaves bond Y in its previous state.
Sequence preservation. Preservation holds not just for individual regulatory actions but for entire action sequences (e.g., FREEZE → SEIZE → CONFISCATE). A valid action sequence on one chain is valid on every connected chain, and the final states match.
None of these guarantees are “theoretical design goals.” They are mathematical facts where every logical path has been exhaustively verified by Isabelle/HOL’s kernel.
Model Boundaries: Intentional Abstraction
Every formal model must choose a level of abstraction. Explicitly recording what has been abstracted away is what strengthens a model’s credibility. When Digital Asset verified Canton’s privacy-aware causality, they likewise started from similar assumptions (synchronous execution, honest nodes) and subsequently pursued a path of gradually relaxing those assumptions.
We summarize the current model’s four key assumptions.
Atomic synchronization. The sync function executes in a single step within the model. In practice, network latency and partial failures exist. The OSS preemptive locking mechanism (with timeouts, auto-release, and per-chain finality tracking) is the implementation-level counterpart to this assumption.
Honest nodes. All nodes are assumed to follow the protocol. Guarantees under Byzantine environments fall within Property 2 (D-quencer determinism), where D-quencer’s BFT consensus serves as the implementation-level counterpart.
Instant lock acquisition. In the model, a lock succeeds immediately when unlocked. Distributed lock contention is handled by lock queues and timeouts.
Finite static chain set. connected_chains does not change during sync execution. Dynamic topologies are addressed through registry-based lookups and halting sync on topology changes.
These abstractions are not weaknesses but standard methodology in formal verification. Declaring assumptions explicitly and transparently documenting how each assumption is realized in implementation is the role of FORMAL_MODEL_MAPPING.md.
Figure 2: Model Assumptions vs. Implementation Reality
Oraclizer’s First Official GitHub Repository
Oraclizer’s first official GitHub repository launches with this formal verification artifact.: github.com/Oraclizer/formal-verification
Under a BSD license, all .thy files, ROOT, root.tex, and FORMAL_MODEL_MAPPING.md are included. Anyone can install Isabelle 2025-2 and re-verify every proof with a single command.
isabelle build -d . Cross_Domain_State_Preservation
If the output reads Finished Cross_Domain_State_Preservation, every proof has been mechanically confirmed. If even a single sorry or oops exists, the build fails. This is the transparency of formal verification. An audit report depends on the reputation of the auditing firm; a .thy file can be verified by anyone.
Starting Oraclizer’s GitHub with proofs rather than product code was a deliberate choice. The fact that our first public artifact is mathematical verification, not application code, signals what kind of project Oraclizer is.
FORMAL_MODEL_MAPPING.md maps each core element of the .thy files to its corresponding implementation target in Go/Solidity. For instance, the reg_state datatype maps to enum RegState in RWAEnforceable.sol, and the sync function maps to OSS’s sync() main loop. Each model assumption is paired with the mechanism that realizes it in implementation, and each gap is documented alongside its mitigation strategy.
The theory document generated from the Isabelle/HOL proof build, available in the repository.
This document is updated as implementation code is developed, transparently providing evidence of the “design → verification → implementation” sequence. For those who want to browse the proof structure without installing Isabelle, the theory document (PDF) is also available in the repository.
AFP Submission: Registration in the World’s Formal Proof Archive
On March 25, 2026, we submitted the Cross_Domain_State_Preservation entry to the Archive of Formal Proofs (AFP). AFP is the official Isabelle/HOL proof archive operated by the Technical University of Munich (TUM) and the University of Cambridge, and serves as the world’s largest repository of machine-checked proofs in mathematics, computer science, and formal methods.
Registration in AFP carries three implications.
First, build verification. All proofs are officially confirmed to build without error under a specific Isabelle release (in our case, 2025-2).
Second, editor review. AFP editors review the proof’s structure, documentation quality, and reusability of the theory.
Third, permanent accessibility. Registered entries become first-class libraries that Isabelle/HOL users worldwide can import into their own proofs. Other researchers can take our locales and use them to verify their own cross-domain systems.
The submission is currently under editor review, with official registration to follow upon completion.
Implications for ERC-TRUST
While Property 1’s results verify Oraclizer’s infrastructure, they also provide direct support for the ERC-TRUST token standard.
The 35 transition rules in reg_transition serve as the reference specification that ERC-TRUST Core’s state transition logic must match. Solidity’s enum RegState, enum RegAction, and state transition functions must correspond exactly to this transition table. confiscated_terminal maps to the require(state != RegState.CONFISCATED) guard, confiscate_universal informs the CONFISCATE function’s precondition design, and no_self_loops maps to post-transition state-change assertions.
Cross-chain extension safety provides the design rationale that regulatory actions defined by ERC-TRUST on a single chain work consistently when extended across chains. When TRUST is submitted to the Ethereum Magicians forum, the .thy files and FORMAL_MODEL_MAPPING.md will be attached as reference materials.
That said, this is not a proof that “ERC-TRUST’s Solidity code is safe.” The formal correspondence (refinement) between model and code is currently out of scope, and remains a future challenge. This distinction must be maintained honestly.
Looking Ahead: From Safety to Liveness
Property 1 proved a safety property: “the system does not reach a bad state.” Specifically, cross-domain state preservation is maintained through synchronization.
But safety alone is not enough. A system not reaching bad states is a different question from a system making progress. Property 2 addresses liveness: “even when conflicting regulatory actions arrive simultaneously, D-quencer’s priority resolution is deterministic, no deadlocks occur, and no asset is trapped in the system indefinitely (starvation freedom).”
Safety (Property 1) and liveness (Property 2) must combine for the system’s correctness to be fully verified. Property 2 will reuse Property 1’s model infrastructure (state definitions, transition functions, global state model) and extend it with D-quencer’s priority function, wait-for graphs, and fairness conditions.
Whether and to what extent Property 2 proceeds (including whether to incorporate Byzantine fault models) will be decided separately.
Cross-Domain State Preservation: An Honest Ledger of What Was Proven
To close, we restate the machine-verified facts.
Oraclizer’s state synchronization theory has been mathematically proven. A state change on one chain is faithfully preserved across every connected chain, verified for all possible cases by machine-checked proof.
The regulatory state transition model (5 states, 7 actions) satisfies the state_machine locale. CONFISCATED is a terminal state, CONFISCATE is reachable from every non-terminal state, and no self-loops exist.
After synchronization, all connected chains agree on the new regulatory state (regulatory homomorphism). Synchronization preserves the global validity invariant (valid state preservation). The generic framework applies parametrically to the regulatory model for any finite domain set.
State preservation extends from single transitions to arbitrary-length action sequences. Synchronization on one asset does not affect other assets.
Network asynchrony, Byzantine fault tolerance, and model-to-code refinement remain outside the current model’s scope; Byzantine environments and liveness are targets for Property 2.
This is not an audit. This is not a test. It is a mathematical proof. No oracle project has achieved this before Oraclizer. And this proof is not just for Oraclizer. 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. Anyone can verify them directly.
References
[1]. Lochbihler, A. (2020). Formalization of Authenticated Data Structures as Functors in Isabelle/HOL. AFP Entry: ADS_Functor. https://www.isa-afp.org/entries/ADS_Functor.html
[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
[3]. Archive of Formal Proofs. https://www.isa-afp.org/
[4]. Lochbihler, A., Schneider, J. (2021). Mechanizing a Verified Merkle Tree in Isabelle/HOL. CPP 2021. https://dl.acm.org/doi/10.1145/3437992.3439921
Learn More
Proving Cross-Domain State Preservation: The Journey
