TL;DR
In previous research, we argued that regulatory assurance for RWA infrastructure must move beyond audit reports and runtime checks into the domain of mathematical proof. Through the launch of our Proofs category, we declared our commitment to applying that standard to ourselves. This article is the first record of that journey. The subject of verification is not code but design (the model) — and this happens to be the most valuable moment to catch design flaws, before any production code exists. Here we present the technical rationale for choosing Isabelle/HOL, the formal meaning of three verification target properties, and a core design idea we call the Regulatory State Functor.
The phrase “mathematical proof” can sound abstract. Before we get to tool selection, formal definitions, and the Regulatory State Functor, it is worth grounding the discussion in what formal verification has actually accomplished in blockchain — because the track record is more substantial than most realize.
What Formal Verification Has Already Achieved in Blockchain
Formal verification is a method of mathematically proving properties of software or protocols. Where testing confirms “it works in this scenario,” formal verification guarantees “this property holds in every possible scenario.” The difference is qualitative, not quantitative.
In the blockchain domain, this approach already has a substantial track record.
Ethereum received formal verification across three core layers. The Ethereum Virtual Machine (EVM) was given a complete formal semantics using Isabelle/HOL, presented at the CSF conference in 2018 [1]. This defined mathematically what every EVM opcode does. Solidity smart contracts have been verified in Isabelle/HOL through Hoare logic and verification condition generation. And the Beacon Chain consensus protocol had its safety and liveness properties verified through model checking. A single blockchain ecosystem received formal verification at three distinct layers — the virtual machine, the smart contract language, and the consensus protocol.
Ethereum is not alone. Redbelly Network’s DBFT consensus was the first consensus protocol verified through parameterized model checking, presented at DISC 2022 [2]. The Stellar Consensus Protocol (SCP) had its safety and liveness proved in Isabelle/HOL, presented at FMBC 2020. The Raft consensus protocol — foundational to distributed systems — was formally verified in Coq. Beyond blockchain, the seL4 microkernel stands as a landmark in operating-system-level formal verification, with 8,700 lines of C code verified by over 200,000 lines of Isabelle/HOL proof scripts [3]. And Digital Asset verified DAML’s authorization and privacy models in Isabelle/HOL, establishing the design correctness of the Canton ledger [4].
A common pattern emerges from these efforts. Each project selected the single most critical property of its system and submitted it to machine-checked proof. The EVM proved the correctness of its opcode semantics. Stellar proved the safety of its consensus. seL4 proved the functional correctness of its kernel. And every one of these verifications occurred within a single domain — one consensus protocol, one virtual machine, one smart contract language.
Figure 1: Formal Verification in Blockchain: Precedents
Oraclizer’s core property is different. It exists between domains. When a regulatory authority issues a FREEZE on a tokenized asset, is the structure of the regulatory state transition preserved across every chain where that asset exists? We call this property cross-chain regulatory homomorphism. And to our knowledge, no cross-chain regulatory property of this kind has been formally verified.
In this article, we develop the technical rationale for our verification tool selection, the formal meaning of three target properties, and a core design idea we call the Regulatory State Functor.
Why Now: Model Verification Precedes Code Verification
There is a common misconception about formal verification — that it is something you do after the code is finished. In practice, the opposite is true. The highest value of formal verification lies in verifying the design before any code is written.
The distinction is fundamental. The target of formal verification is not code (implementation) but the model (design). The core work is converting an abstract model — defined in whitepapers, protocol specifications, and state transition rules — into a mathematical object, then proving that the object satisfies the desired properties. In the formal verification of the seL4 microkernel, the abstract specification was built first, and the proof that the C code was a correct refinement of that specification came after. The seL4 team reported discovering 144 bugs in early C code and roughly 150 issues in the design and specification, respectively, during the verification process [3].
Digital Asset followed the same approach. Before the DAML runtime was complete, they formalized and verified the authorization model and privacy model in Isabelle/HOL [4]. The modeling process itself uncovered design flaws early — this is the true value of formal verification.
Oraclizer is currently in Phase 0 (State Sync Proof of Concept). No production code exists yet. But the state transition rules of OSS (Oracle State Synchronizer), the priority resolution scheme of D-quencer, and the definitions of the six regulatory actions already exist in the whitepaper and protocol specification. This is precisely the right moment to begin formal verification. Discovering a design flaw after code is written means exponentially higher correction costs. Discovering it when no code exists means we can fix the design and build the correct implementation from the start.
The Limits of Program Testing and the Domain of Proof
To understand why formal verification is necessary, we return to an insight from Edsger Dijkstra.
“Program testing can be used to show the presence of bugs, but never to show their absence.”
Edsger W. Dijkstra, Notes On Structured Programming (1970)
The implications of this statement have rarely been fully absorbed in blockchain infrastructure. Dijkstra’s point is that there is a qualitative difference between testing and proof. Passing 100 test cases tells you the code is correct in 100 scenarios. It says nothing about the 101st. A mathematical proof, on the other hand, guarantees that a property holds across every possible execution path — within the scope of the model’s assumptions.
The domain where this difference becomes decisive is cross-chain regulatory enforcement.
Suppose a regulatory authority issues a FREEZE action on an asset on Chain A. If that asset is also used as collateral on Chain B and Chain C, the FROZEN state must propagate consistently to all relevant chains. If this propagation fails — if an unfrozen version of the asset on Chain B can still be used to create new derivatives — the entire regulatory compliance framework collapses.
How would you verify this scenario through testing? The number of chains, assets, regulatory action combinations, network delays, and concurrency patterns explodes combinatorially. Testing every possible scenario is physically impossible.
Formal verification, by contrast, defines the state transition model mathematically, formalizes the property — “upon receiving FREEZE, all relevant chains transition to FROZEN within bounded time” — as a theorem, and proves it. Once the proof is complete, the property holds without exception within the model’s assumptions.
An important caveat applies, of course. The qualifier “within the model’s assumptions” matters. Formal proofs operate on formal semantics — a model of the real world. How faithfully that model reflects reality is a separate question [4]. Acknowledging this limitation honestly is the starting point of any formal verification project.
Why Isabelle/HOL
In the category launch post, we noted that Isabelle/HOL is the common tool behind seL4, the EVM formal semantics, and the DAML authorization model. But we did not cover the technical rationale for selection in detail. Choosing a theorem prover is not merely picking a tool — it is a design decision determined by the nature of the properties being verified and the composability with existing verification ecosystems.
We analyzed the major candidates.
Coq (recently renamed Rocq) is built on dependent type theory (Calculus of Inductive Constructions). It boasts the success of CompCert — the formally verified C compiler. However, Coq’s strength in constructive logic becomes a constraint for our purposes. Properties of cross-chain state synchronization frequently require classical logic, and using it in Coq means introducing additional axioms.
Lean 4 is the fastest-growing theorem prover. It has built an impressive ecosystem with Mathlib — over 1.9 million lines of formalized mathematics. But Lean’s strengths concentrate on pure mathematical formalization, and precedents for distributed systems protocol verification remain relatively scarce compared to Isabelle/HOL.
TLA+, designed by Leslie Lamport, is a formal specification language specialized for verifying temporal properties of distributed systems. However, the TLA+ model checker operates on finite state spaces and cannot provide universal proofs over infinite state spaces. We leave open the possibility of using it as an auxiliary tool — it is useful for quickly detecting model flaws — but decided against adopting it as the primary proof tool.
Our rationale for choosing Isabelle/HOL rests on three pillars.
First, composability with the DAML/Canton verification ecosystem. This was the decisive factor. The properties we aim to verify must ultimately compose with the formal verification results of DAML/Canton. Andreas Lochbihler and Ognjen Marić abstracted Canton’s hierarchical transaction structures into Merkle Functors — modular building blocks registered in Isabelle/HOL’s AFP (Archive of Formal Proofs) [5]. The Canton team also formalized privacy-aware causality in Isabelle/HOL and set deadlock-freedom as a verification target [6]. All of this work lives within Isabelle/HOL. Working on the same tool and the same logical framework makes future proof composition natural.
Second, native support for classical logic. Isabelle/HOL is built on classical higher-order logic. The law of excluded middle and the axiom of choice are available by default. Properties like “every chain is either in FROZEN state or still in propagation” can be expressed naturally.
Third, a proven track record in large-scale system verification. The seL4 microkernel — 8,700 lines of C and 600 lines of assembler verified by over 200,000 lines of Isabelle/HOL proof scripts [3] — and the safety and liveness proofs of the Stellar Consensus Protocol demonstrate that Isabelle/HOL is well-suited for verifying large-scale distributed systems.
Figure 2: Theorem Prover Selection Comparison
Formal Meaning of Three Verification Targets
In the category launch post, we introduced cross-chain regulatory homomorphism as a verification goal. Here we clarify the formal meaning of three properties, including that one. Each property extends the model built by the previous one.
Property 1: Cross-Chain Regulatory Homomorphism — Top Priority
Natural-language specification: “When OSS receives a FREEZE message, the state of all chains linked to the target asset ID transitions to FROZEN within bounded time.”
Formalizing this statement requires several decisions. What exactly does “bounded time” mean? Is the network synchronous, asynchronous, or partially synchronous? Are Byzantine nodes present? Is message delivery guaranteed?
As we emphasized in the category launch post, the mathematical term “homomorphism” was chosen deliberately. A homomorphism is a structure-preserving map. It means that a regulatory action on Chain A is not merely replicated on Chain B as “the same outcome” — the transition structure itself is preserved. If a transition from FREEZE to SEIZE is valid on Chain A, the same transition relation must hold on Chain B.
There is a reason this property comes first. During formalization, the entire OSS state transition model gets built inside Isabelle/HOL. This becomes the foundation for all subsequent verification work.
Property 2: D-quencer Priority Determinism and Deadlock Freedom
Natural-language specification: “Even when conflicting regulatory actions arrive simultaneously, D-quencer’s priority resolution is deterministic and no deadlock occurs.”
Translated into formal terms, this means proving that the priority function forms a total order and that the wait-for graph is acyclic.
This property is significant because it directly corresponds to work by the Canton team. Lochbihler and Marić proposed deadlock-freedom of privacy-aware causality as a verification target at CPP 2021 — exactly the same structural problem, transposed to the regulatory domain. Including Byzantine environments would increase the academic contribution.
Property 3: Heterogeneous Verification Composition (Long-Term Goal)
Natural-language specification: “When the formal verification scope of DAML, the zk proof scope of OSS, and the runtime check scope of EVM chains are combined, end-to-end regulatory coherence of the whole system is guaranteed.”
This is the formal expression of the problem left as an “open question” in a previous RWA study, and the ultimate goal described in the category launch post as “guaranteeing regulatory consistency across heterogeneous blockchain environments.” If solved, it would constitute a paper-level contribution. We will assess feasibility separately, after Properties 1 and 2 are complete.
Regulatory State Functor: The Core Design Idea
There is a core design idea we aim to explore in this project. We call it the Regulatory State Functor.
The idea originates from Lochbihler’s work. He abstracted Canton’s authenticated data structures into Merkle Functors — modular building blocks. These functors encompass sums, products, and function spaces, and are closed under composition and least fixpoints. This abstraction enabled assembling complex transaction trees from small, reusable blocks whose properties could be proved independently.
We want to bring this pattern into the regulatory domain. The idea is as follows.
Early sketch: the homomorphism condition φ(δA(s,a)) = δB(φ(s),a) that Property 1 aims to prove.
Define regulatory state transitions as a chain-independent abstract functor. Each chain-specific implementation (EVM, Canton, etc.) becomes an instance of this functor. Cross-chain regulatory homomorphism then naturally expresses itself as a natural transformation between functors. More importantly, when a new chain is added, defining a new functor instance automatically extends existing proofs.
In category-theoretic terms, the map from the regulatory state category of Chain A to that of Chain B is a structure-preserving functor, and OSS state synchronization is the natural transformation between these functors.
Whether this approach is excessive abstraction or the right level of generality — we do not know yet. That determination must come during the modeling process. It is possible to prove Property 1 directly without functors. But if the functor approach succeeds, there is a structural advantage: the proof of Property 1 would extend directly to Property 2. Academically, extending Lochbihler’s Merkle Functor pattern to the regulatory domain could merit AFP registration or recognition at a venue like FMBC.
Figure 3: Formal Verification Roadmap
Limits of Verification: What It Does Not Guarantee
As we begin formal verification, there is something we must clarify first. We must be honest about what formal proofs do not guarantee.
“done” ≠ system safety. When done appears in Isabelle/HOL, the theorem is proved. But that proof holds over a formal model. Between the model and reality lies a semantics gap. If the model assumes the fraction of Byzantine nodes is below 1/3 but the actual fraction exceeds that threshold, the proof’s guarantee is invalidated.
Assumptions are the boundaries. Every formal proof stands on assumptions. Network model, message delivery guarantees, Byzantine node ratios — whether these assumptions hold in reality is outside the scope of formal proof. We will explicitly document the assumption list for each proof and analyze “what happens if this assumption breaks.”
Model verification, not code verification. What we prove is a property of the abstract model. Whether the actual Go code correctly implements that model is a separate question — it corresponds to the refinement proof between abstract specification and C code in seL4, and is not within the current scope.
Acknowledging these limits does not diminish the value of formal verification. Quite the opposite. Explicitly declaring assumptions and boundaries is itself a higher level of transparency — one that audit reports and runtime checks cannot provide. “No vulnerabilities found within our testing scope” and “under these assumptions, this property holds without exception” are qualitatively different kinds of assurance.
The Road Ahead
The next article will cover the foundations of Isabelle/HOL — why Higher-Order Logic goes beyond first-order logic, how to model state transition systems, basic patterns for proving invariants, and the mathematical foundations of functors. That article serves as a primer for readers and simultaneously marks our own team’s learning starting point.
After that, we will fix the scope and assumptions of Property 1 (cross-chain regulatory homomorphism), build the formal model in Isabelle/HOL, and attempt to prove theorems. At each stage, we will share honestly what we tried, where we got stuck, and how we resolved it.
There is no guarantee that every proof attempt will succeed. We may need to revise the model, strengthen assumptions, or approach the problem from an entirely different angle. But there is one thing we are certain of: the process itself improves the design. The true value of formal verification is not the final proof certificate at the moment done appears, but the design flaws discovered and corrected along the way.
Whether this journey ends in success or reaches an outcome different from what we expect, we believe the process itself will elevate the discourse on regulatory assurance for RWA infrastructure to a new level.
References
[1] Hildenbrandt, E. et al. (2018). “KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine.” In: 31st IEEE Computer Security Foundations Symposium (CSF). https://doi.org/10.1109/CSF.2018.00022
[2] Bertrand, N. et al. (2022). “Holistic Verification of Blockchain Consensus.” In: 36th International Symposium on Distributed Computing (DISC). https://doi.org/10.4230/LIPIcs.DISC.2022.10
[3] Klein, G. et al. (2009). “seL4: Formal Verification of an OS Kernel.” In: 22nd ACM SIGOPS Symposium on Operating Systems Principles, pp. 207–220. https://dl.acm.org/doi/10.1145/1629575.1629596
[4] Digital Asset. (2018). “How difficult is it to write correct smart contracts? Depends on your tools!” https://medium.com/daml-driven/how-difficult-is-it-to-write-correct-smart-contracts-depends-on-your-tools-5f6bceb2d510
[5] Lochbihler, A. & Marić, O. (2020). “Authenticated Data Structures As Functors in Isabelle/HOL.” In: FMBC 2020. OASIcs vol. 84, 6:1-6:15. https://doi.org/10.4230/OASIcs.FMBC.2020.6
[6] Digital Asset. (2021). “A semantic domain for privacy-aware smart contracts and interoperable sharded ledgers.” Lightning talk, CPP 2021. https://www.canton.io/publications/cpp2021-slides.pdf
Learn More
Read more on Oraclizer Research:
- From Isabelle/HOL to Compliance-Aware Infrastructure: Why RWA Needs Provable Compliance — Analysis of Pattern 3 necessity and Digital Asset’s verification case study
- Introducing Our New Research Domain: Proofs — Background on the Proofs category launch and verification goals overview
