Skip links

Type and hit enter

Subscribe
Oraclizer Research

We Proved It: Cross-Domain State Preservation, Formally Verified

Oraclizer Update

Oraclizer’s first formal verification property is complete.

Cross-domain state preservation, the guarantee that a regulatory state change on one chain is faithfully preserved across every connected chain, has been mathematically proven. State synchronization is a first-of-its-kind concept in blockchain history. With this proof, the theory is now mathematically guaranteed to work.

This is not an audit. This is not a test. It is a mathematical proof where Isabelle/HOL’s theorem-proving kernel exhaustively verified every possible case. No other oracle project has achieved this level of assurance.

What Was Proven: State Preservation Across Chains

Three core theorems have been proven for a regulatory state transition model comprising 5 states (ACTIVE, FROZEN, SEIZED, CONFISCATED, RESTRICTED) and 7 regulatory actions.

Regulatory Homomorphism. After synchronization, all connected chains agree on the new regulatory state.

Valid State Preservation. Synchronization preserves the global validity invariant. Once the system starts in a valid state, no amount of synchronization can push it into inconsistency.

Multi-Domain Parametric Instantiation. These guarantees hold for any finite set of domains, whether 3 chains or 300.

AFP Submission

The state preservation 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. The entry Cross_Domain_State_Preservation is currently under editor review.

GitHub

Oraclizer’s first official GitHub repository launches with this state preservation proof artifact. The complete proof code is available under a BSD license. Anyone can install Isabelle 2025-2 and verify every proof directly.

github.com/Oraclizer/formal-verification

A Generic Framework

This proof is not just for Oraclizer. We built a domain-independent generic locale hierarchy first, then defined the regulatory model as one instance. Any team building cross-chain infrastructure can import this framework and verify their own system to the same standard. We didn’t just prove our protocol. We created a certification standard for cross-chain state preservation.

For the full technical details, design discoveries, and proof structure, see the latest post in our Proofs series:

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

View Theory Document (PDF)

Read Next

Defining the Sync Unit: Oracle Usage Metering for State Synchronization
Defining the Sync Unit: Oracle Usage Metering for State Synchronization
The State Subscription economy has quoted ten Sync Units for a dollar without ever fixing what one Sync Unit counts, leaving three conflicting conversion rates inside one body of work. This study anchors the unit to a single committed state binding and derives its weight from the sync degree hierarchy. Applying it inverts the existing frequency bands.
Oraclizer Core ⋅ Jul 25, 2026
Designing the ERC-TRUST Enforceability Architecture
Designing the ERC-TRUST Enforceability Architecture
A regulator's freeze and a court's confiscation are legally opposite, yet on today's token standards they compile to the same call. This ERC-7943 conformance extension makes each of the six regulatory actions a typed, distinct object whose legal effect is verifiable on-chain, and carries that meaning from the abstract model down to deployed bytecode as evidence.
Oraclizer Core ⋅ Jul 23, 2026
Our State Synchronization Research Is Now on Ethereum’s Research Forum
Our State Synchronization Research Is Now on Ethereum’s Research Forum
Two Oraclizer research posts now stand on ethresear.ch, Ethereum's research forum: machine-checked proofs that atomic cross-domain synchronization behaves correctly, and a follow-up giving synchronization strength a formal, checkable basis. In between, a public exchange with an Ethereum researcher sharpened the work into what it is now.
Oraclizer Core ⋅ Jul 21, 2026
The Cross-Domain State Preservation Functor: What It Closed, and What It Was For
The Cross-Domain State Preservation Functor: What It Closed, and What It Was For
The cross-domain state preservation proofs are closed: homomorphism, functor completion, a natural-transformation tower, and unconditional bounded convergence. Ten theory files, zero sorry. The harder work was catching what passes a prover while saying nothing: a trivial functor, a bypassed threshold, a witness outside the roster. Each retreat left the rest firmer.
Oraclizer Core ⋅ Jul 16, 2026
Sync Degree Enforcement: What Turns a Classification Into a Constraint
Sync Degree Enforcement: What Turns a Classification Into a Constraint
A classification does nothing on its own. Sync degree enforcement closes the gap between labeling an asset S2 and having the system refuse to touch it any other way. It rests on a two-directional result: over-provisioning preserves every guarantee, under-provisioning admits a state that defeats all of them. So the check leaves runtime and enters Rust's type system.
Oraclizer Core ⋅ Jul 16, 2026