Oraclizer’s formal verification research is now on arXiv.
Safety and Liveness of Cross-Domain State Preservation under Byzantine Faults: A Mechanized Proof in Isabelle/HOL (arXiv:2604.03844) presents the combined Property 1 + Property 2 result as a single, unified formal verification of Oraclizer’s regulatory state synchronization system. The paper is 16 pages, backed by 2,348 lines of mechanized Isabelle/HOL proof, and to the best of our knowledge it is the first mechanized proof in any theorem prover that combines cross-domain state preservation with BFT consensus liveness for a blockchain regulatory system.
The first mechanized proof of cross-domain state preservation under Byzantine faults in Isabelle/HOL.
Property 2 of our formal verification program is now complete. This is also the moment when it becomes public. Alongside the arXiv paper, the GitHub repository has been updated to include the full Property 1 + 2 integrated theories, and Property 2 is now ready for AFP entry update submission.
What the Paper Proves
The paper establishes two properties connected by a single chain of reasoning.
Property 1 — Safety. A regulatory state change on one chain is faithfully preserved across every connected chain. Bidirectional, multi-domain, with isolation guarantees. The regulatory_homomorphism and valid_state_preservation theorems establish that synchronization is structure-preserving and invariant-preserving. (We announced the Property 1 completion in March.)
Property 2 — Liveness under Byzantine Faults. Under the standard BFT threshold (f < n/3), the D-quencer consensus mechanism guarantees three properties: determinism (conflicting regulatory actions resolve to a unique outcome), deadlock freedom (no asset can be locked indefinitely, even by a malicious node), and starvation freedom (every pending request is eventually processed). All three are now proven in Isabelle/HOL, with no sorry and no oops.
The technical centerpiece is the combined_safety_liveness theorem. It does not simply conjoin the two properties. It establishes that Property 2 discharges the honest-node assumption that Property 1 implicitly carried. This is the assume-guarantee reasoning pattern, and it lifts a conditional safety guarantee into an unconditional safety + liveness guarantee under Byzantine faults. One theorem, closing the loop.
Why This Formal Verification Paper Matters
Formal verification of blockchain consensus is not new. Byzantine fault tolerance proofs exist in Coq (Velisarios), Agda (HotStuff), and various model checkers. Cross-chain state preservation has been explored in Canton’s Merkle Functor pattern by Andreas Lochbihler.
What makes this paper distinct is the combination. The same Isabelle/HOL framework, the same locale hierarchy, the same proof kernel now verifies both the structural correctness of cross-domain synchronization and the liveness of Byzantine consensus. Neither property alone is a first. The unified proof is.
Three claims in the paper are, to the best of our knowledge, without prior precedent:
First Isabelle/HOL proof of BFT consensus liveness in a blockchain context. Prior BFT liveness proofs used other tools. The Isabelle/HOL community has Canton’s safety-focused work but no comparable liveness result for blockchain consensus.
First formal verification of regulatory-specific consensus properties under Byzantine faults, in any theorem prover. Regulatory action priority, regulatory asset deadlock freedom, and regulatory request starvation freedom are properties that no prior formalization has addressed.
First bidirectional, multi-domain cross-chain state preservation proof. Existing cross-chain verification work covers unidirectional or 2-domain cases. This paper proves the structure-preserving roundtrip property and the N-domain consistency property within a single locale hierarchy.
Seven Reusable Locales
The paper is also a contribution to verification infrastructure. The proof is built on seven domain-independent locales — four for state preservation (Property 1) and three for priority resolution and liveness (Property 2). None of them mention regulation, blockchain, or anything specific to Oraclizer.
Anyone working on distributed databases, MEV ordering, DeFi lock mechanisms, PoS consensus variants, or multi-shard state synchronization can import these locales into their own Isabelle/HOL project and instantiate them for their domain. If the instantiation fits the abstract pattern, the theorems already hold. This is the same design philosophy that Lochbihler applied to Canton’s Merkle Functor, now extended along a different axis of abstraction.
Where to Find It
arXiv paper: arxiv.org/abs/2604.03844 — 16 pages, open access, cs.CR primary / cs.LO cross-list.
GitHub repository: github.com/Oraclizer/formal-verification — the full Isabelle/HOL theories, ROOT file, generated PDF (46 pages), model-to-implementation mapping, and build instructions. Install Isabelle 2025-2 and run isabelle build -d . Cross_Domain_State_Preservation to verify every proof directly.
AFP entry: Property 1 is currently under editor review at the Archive of Formal Proofs as the entry Cross_Domain_State_Preservation. Property 2 will be submitted as an entry update after Property 1 is accepted.
What Comes Next
A reflection on what Property 2 achieves on its own and what Properties 1 + 2 together establish — the meaning of Byzantine-tolerant liveness, the assume-guarantee structure that lifts conditional safety into an unconditional guarantee, and the reusability of the seven locales beyond Oraclizer — will close the Property 2 series in the Proofs category soon. This update is the announcement. The reflection is the meaning.
Beyond Property 2, the next milestone is Property 3: composing the Cross-Domain State Preservation Functor with Lochbihler’s Merkle Functor to establish end-to-end formal assurance from Canton off-chain ledgers through Oraclizer synchronization to on-chain EVM state. That work is the long-term goal of this research program, and it will be submitted as a separate AFP entry when complete.
For now: the paper is public, the proofs are public, the code builds. You can access the paper via the button below. For questions, reach us at jay@oraclizer.io or on X.
