Formal verification has a quiet but consequential history in blockchain. Redbelly Network’s DBFT consensus became the first to be holistically verified through parameterized model checking, published at DISC 2022. The Stellar consensus protocol was verified in Isabelle/HOL and presented at FMBC 2020. The Raft consensus protocol — foundational to many distributed systems — was verified in Coq. Ethereum alone has accumulated multiple layers of formal verification: the EVM received its first complete formal semantics in Isabelle/HOL at CPP 2018, Solidity smart contracts have been verified through Hoare logic and verification condition generation in Isabelle/HOL, and the Beacon Chain consensus has been model-checked for safety and liveness properties.
These efforts share a common thread: each chose a critical property of their system — consensus safety, VM correctness, language semantics, contract behavior — and subjected it to machine-checked mathematical proof. The results are not marketing claims. They are theorems, verified by proof assistants that accept nothing on trust.
We believe this is the right path. And we’re taking it — into territory none of these projects have entered.
Today we’re adding a new category to Oraclizer Research: Proofs.
Applying Our Own Standard
In a recent research article — From Isabelle/HOL to Compliance-Aware Infrastructure — we classified compliance assurance into three patterns: post-hoc audits that find vulnerabilities but cannot prove their absence, runtime checks that verify individual transactions but not system-wide coherence, and formally verified rules that express regulatory guarantees as mathematical properties.
We argued that RWA infrastructure must move toward that third pattern. That argument created an obligation: if we believe formal verification is the standard, we should hold ourselves to it first.
The Proofs category is where we do exactly that. It will document our effort to formally verify Oraclizer’s core regulatory properties using Isabelle/HOL — the same theorem prover behind the seL4 microkernel verification, the EVM formal semantics, and Digital Asset’s DAML authorization model.
What We’re Setting Out to Prove
The verification efforts listed above — DBFT, Stellar SCP, EVM, Solidity, Beacon Chain — all operate within a single domain. They verify properties of one consensus protocol, one virtual machine, or one smart contract language. This makes sense: those are the critical properties of those systems.
For an oracle state machine that synchronizes regulatory state across chains, the critical property is different. It lives between domains. Our primary verification target is a property we call cross-chain regulatory homomorphism: when a regulatory action such as FREEZE is issued against a tokenized asset, every chain where that asset exists must reflect the state change — with the structure of the regulatory transition preserved across chains. Not eventual consistency in a loose sense, but a mathematically precise guarantee that the regulatory state transition on one chain maps faithfully onto another.
No blockchain project has formally verified this class of cross-chain regulatory property. It is the kind of guarantee that regulators and institutional participants will eventually require — and the kind that cannot be achieved through testing alone.
What to Expect
This isn’t a polished retrospective. We’ll be publishing as the work progresses — sharing the real process of formal verification applied to cross-chain regulatory infrastructure:
Motivation and foundations — why we chose Isabelle/HOL, what formal verification can and cannot guarantee, and the mathematical groundwork needed to follow the journey.
Model construction — translating OSS’s state transition rules into mathematical objects, making every assumption explicit, and discovering where our designs hold up and where they break.
Proof attempts, failures, and discoveries — honest documentation of what works, what doesn’t, and what we learn from each cycle. The modeling process itself tends to expose design flaws that would otherwise surface only during implementation — this is where formal verification delivers its most practical value.
Completed theorems — machine-checked proofs with all assumptions explicitly stated and their limitations clearly acknowledged.
A Different Kind of Assurance
Audits examine code. Tests check scenarios. Formal verification proves properties hold for all possible states — regardless of the number of chains, nodes, or concurrent regulatory actions. The projects that have taken this path — from seL4 to Stellar to Ethereum’s own layered verification efforts — set a precedent that serious infrastructure submits its critical claims to mathematical proof.
We intend to follow that precedent, applied to a property that hasn’t been formally addressed: regulatory consistency across heterogeneous blockchain environments. Whether we succeed, and what we discover along the way, will be documented openly in this category.
The first Proofs article will be published soon.
Follow our progress on X.
