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
