TL;DR
For tokenized financial assets to attract institutional capital, regulatory compliance must be guaranteed as a mathematical property of the system, not as an audit report. The dominant patterns in current RWA infrastructure — post-hoc audits and runtime checks — can identify individual vulnerabilities but cannot guarantee the regulatory coherence of the system as a whole. Digital Asset’s research team using Isabelle/HOL for formal verification of DAML’s authorization and privacy models demonstrates that provable compliance is a feasible goal for financial contracts. This article analyzes why the RWA industry will increasingly demand this level of assurance, and how Oraclizer is building a multi-layered compliant-by-design architecture that extends well beyond DAML/Canton.
Suppose a tokenized bond has been issued, and its interest payment state is managed simultaneously on-chain and off-chain. When a regulatory authority issues a freeze order on that bond, who — and at what level of assurance — guarantees that this order is consistently enforced across every chain, every state layer?
The current RWA industry’s answer to this question is, in most cases, either “we’ve had our smart contracts audited” or “we check with require() statements.” The reason this answer fails to satisfy institutional investors is that it is fundamentally a question of the level of assurance. An audit confirms that no vulnerabilities were found — it does not prove the absence of vulnerabilities. Runtime checks secure regulatory compliance at the individual transaction level, but system-wide state consistency falls outside their scope.
I have been thinking about this problem since 2019. At the time, I was deeply absorbed in a project that barely registered on the blockchain industry’s radar — a smart contract language called DAML from a company called Digital Asset. What captivated me was not DAML’s syntax. It was the fact that Digital Asset’s research team had formally verified core parts of their platform using Isabelle/HOL, a theorem prover [1]. I installed and ran Isabelle/HOL myself. Watching a theorem prover mechanically verify mathematical propositions, I became convinced that the correctness of financial contracts could belong to the domain of proof, not merely testing.
That conviction went on to become a design principle that runs through the entire Oraclizer architecture. If DAML/Canton is one means of realizing that principle, Oraclizer’s compliant-by-design architecture is the extension of that principle to the system as a whole.
The Compliance Assurance Gap in RWA Infrastructure
The tokenized asset market is growing rapidly, but the level of regulatory assurance in its infrastructure has not kept pace. As analyzed in our previous research, if RWA 1.0 was the stage of exploring the possibility that “blockchain can handle real-world assets,” RWA 2.0 represents a mature paradigm that fully embraces each industry’s legal frameworks and legacy systems while achieving complete integration with DeFi.
The critical bottleneck in this transition is not technical performance — it is the level of regulatory compliance assurance.
What institutional investors and regulatory authorities demand of tokenized assets is not simply a declaration that “regulations are being followed.” What they seek is confidence that the system structurally cannot violate regulations. The distinction is subtle but fundamental.
The dominant patterns for securing regulatory compliance in current RWA infrastructure fall into three categories.
Post-hoc audit: After a smart contract is deployed, an external audit firm reviews the code. As Edsger Dijkstra observed, program testing can reveal the presence of bugs but is structurally inadequate for demonstrating their absence. The same holds for audits. “Absence of discovered vulnerabilities” and “absence of vulnerabilities” are qualitatively different guarantees.
Runtime check: require() statements or modifiers inserted to verify regulatory conditions at transaction execution time. These guarantee regulatory compliance at the individual transaction level, but system-wide state consistency falls outside their scope. If a bond has been frozen on Chain A while a derivative on Chain B continues to use that bond as collateral, runtime checks cannot detect this gap.
Formally verified rules: Regulatory rules are embedded in the system’s authorization and privacy models, and the correctness of these models is mathematically proven. In this case, a regulatory violation is not an individual bug but a violation of a proven property — which, within the scope of the formal model, is mathematically impossible.
Figure 1: Three Levels of Regulatory Compliance Assurance in RWA Infrastructure
The reason the third pattern has not yet been widely adopted in the RWA industry is the high cost and complexity of formal verification. However, as the scale of tokenized assets grows and cross-chain operations become routine, the first two patterns alone will prove insufficient to secure institutional trust. The maturation of RWA infrastructure necessarily means an elevation in the level of regulatory assurance.
A Real-World Case: Formal Verification Applied to Financial Contracts
Formal verification is not merely an abstract theory — there exists a concrete case of its application to real financial infrastructure. That case is the work carried out by Digital Asset’s research team.
Verification of Core Properties in the DAML Platform
In 2018, Andreas Lochbihler — Digital Asset’s formal verification engineer, formerly of ETH Zürich, and developer of the CryptHOL framework for formal verification of cryptographic constructions — disclosed that core parts of the DAML platform had been verified using Isabelle/HOL and TLA+ [1]. Specifically:
Authorization model: In DAML, every ledger update cannot be executed without the explicit consent of relevant signatories. The formal verification of this property means it was mathematically proven that unauthorized ledger modifications cannot occur under any execution path.
Privacy model: In DAML’s “need-to-know” ledger model, each party can only see the state of contracts in which they have a stake. The correctness of these visibility rules was formally verified.
Enforcement algorithms: The algorithms that enforce the above authorization and privacy rules at runtime were verified to operate exactly as intended.
The implications for the RWA industry are as follows. When ownership transfers, interest payments, and regulatory freeze orders for tokenized bonds are all expressed as DAML contracts, “who can take which actions” and “who can see which information” are executed in an environment where these properties are guaranteed by proof, not by testing.
Formalization of Canton Protocol Data Structures
In 2020, Lochbihler and Ognjen Marić modeled Canton protocol’s hierarchical transaction structure as an authenticated data structure and formalized it in Isabelle/HOL [2]. The research team composed Canton’s Merkle tree data structures using modular building blocks they called Merkle functors, presenting this work as a foundation for verifying the integrity and security guarantees of the Canton protocol.
In follow-up research (2021), they formalized DAML’s privacy-aware causality and set an explicit verification goal: that causality guarantees and deadlock freedom must hold for honest nodes even in the presence of Byzantine nodes [3]. This represents a significant milestone demonstrating the practical value of formal verification in decentralized environments.
One point that deserves emphasis here: Isabelle/HOL is not a tool confined to DAML or Canton. Developed at the Technical University of Munich and the University of Cambridge [4], it is a general-purpose theorem prover with broad applications in the blockchain domain — including Ethereum smart contract bytecode verification [5], Solidity verification frameworks [6], and safety and liveness proofs for the Stellar Consensus Protocol. This is not a marketing tool for any particular platform; it is general-purpose infrastructure for mathematically verifying core properties of distributed systems.
Language Design Determines the Ceiling for Formal Verification
One of the reasons I became so deeply invested in DAML was the insight that the feasibility of formal verification is a direct consequence of language design.
DAML is a Haskell-based functional language supporting strict evaluation, a strong static type system, and algebraic data types. These characteristics enable formal verification for two reasons.
First, minimization of corner cases. An analogy presented on Digital Asset’s blog illustrates this well [1]. In JavaScript, x + 1 can exhibit diverse behaviors depending on the type of x — string concatenation, floating-point identity operations, and so on. In a strong type system, the same expression has exactly one meaning. Fewer corner cases means fewer cases to handle in formal verification.
Second, the right level of abstraction. In DAML, contracts, parties, rights, obligations, and authorization are primitive constructs of the language [7]. Formal verification tools can directly verify the correspondence between the intent of business logic and the behavior of code. In languages like Solidity, where these concepts must be encoded using low-level primitives, verification tools must first reverse-engineer the encoding, causing verification complexity to escalate dramatically.
From the RWA industry’s perspective, this observation matters because the design of the language in which tokenized financial asset contract logic executes directly determines the upper bound of regulatory assurance. No matter how sophisticated an audit is, if the underlying language is not amenable to formal verification, proof-level assurance is structurally impossible.
What We Learned from DAML, Extended Across Oraclizer
Let me be precise about one thing. Oraclizer’s compliant-by-design architecture does not depend on DAML/Canton — it extends principles learned from DAML/Canton across the entire system.
What I internalized from studying and using DAML since 2019 was not a particular technology but a design philosophy. Regulatory compliance is not something appended after the fact at the application layer — it must be structurally embedded from the system’s lowest layers. If DAML’s signatory/observer model demonstrated this at the contract level, I was convinced that the same principle must apply to the state synchronization system as a whole, and I embedded it into Oraclizer’s design accordingly.
Oraclizer’s compliance-embedded architecture is a multi-layered structure that includes DAML/Canton but is not limited to it:
RCP’s Five Principles — The Regulatory Compliance Protocol, which systematizes 31 core regulations from 15 global financial regulators, is Oraclizer’s proprietary framework. The five principles — Enforceability, Privacy, Traceability, Finality, and Tokenizability — constitute an abstraction of regulatory requirements that is not dependent on any specific technology stack. Every component of the Oraclizer system is designed to adhere to these principles.
OIP Identity Specification — The OCID (Oracle Contract ID) and system-wide AML defined by the Oracle Interoperability Protocol ensure that consistent AML policies are applied at the protocol level across on-chain, off-chain, and cross-chain domains. This is Oraclizer’s proprietary identity management system that extends beyond DAML’s scope.
4-Layer Privacy Stack — Comprising L1 Identity (zk-based ID proofs), L2 Contract (DAML Need-to-Know), L3 State (OSS selective synchronization), and L4 Audit (OCID/RAI conditional identity linking), DAML is responsible for only the L2 layer within this privacy architecture. The remaining three layers are Oraclizer’s proprietary designs.
OSS Compliance Verification — The OIP/regulatory compliance verification performed by the Oracle State Synchronizer when processing state transitions operates independently of DAML as a separate verification layer. In cross-chain environments, the consistent propagation of a regulatory authority’s freeze order across all relevant chains is the responsibility of OSS — an Oraclizer-native assurance mechanism that operates outside the scope of DAML’s formal verification.
D-quencer Regulatory Action Priority Management — The mechanism by which the decentralized sequencer determines priority among conflicting regulatory actions and fast-tracks regulatory rollbacks is likewise Oraclizer’s proprietary design.
Figure 2: Oraclizer’s Multi-Layered Compliant-by-Design Architecture
In summary, DAML/Canton provides the formal verification foundation at the contract layer within Oraclizer’s compliant-by-design architecture. But the way Oraclizer achieves built-in regulatory compliance is not by depending on DAML, but by independently implementing the principle that “compliance must be embedded” — learned from DAML — across every layer of the system: RCP, OIP, OSS, D-quencer, and beyond.
Boundaries of Verification and Open Questions
We must acknowledge that this approach is not a panacea. Several fundamental limitations remain.
Bounded scope of formal verification: Proofs in Isabelle/HOL are carried out over formal semantics. Formal semantics is a model of the real world, and whether the model faithfully reflects reality requires separate verification [1]. No matter how rigorous a proof is, if the model on which it is based is incomplete, the scope of its guarantees is correspondingly limited.
Absence of cross-domain proofs: Properties within a Canton domain have been formally verified, but for state synchronization between Canton and EVM chains to carry the same level of formal assurance, additional formalization work is required. Oraclizer addresses this gap with GKR proofs and zk verification, but these do not provide the same level of guarantee as formal verification.
Cost and accessibility: DAML’s static analysis tools are designed to operate automatically based on symbolic execution [1], but the scope of properties they can verify is more limited compared to a theorem prover. Harnessing the full capabilities of formal verification requires specialized expertise and time — a cost that not every RWA project can bear.
Dynamic regulatory environments: Regulatory requirements change over time. How to efficiently update existing proofs when the set of formally verified properties must be expanded to accommodate new regulations remains an unresolved problem concerning the practical viability of formal verification.
The existence of these limitations does not negate the direction of formal verification itself. Rather, as RWA infrastructure matures, resolving these limitations one by one will become a challenge for the entire industry. “Not perfect” and “unnecessary” are entirely different claims.
What the RWA Industry Should Take Away
If tokenized financial assets are to evolve from mere experiments into institutional-grade infrastructure, the level of regulatory compliance assurance must evolve alongside them. If audit reports and runtime checks were adequate for the early stages, the tokenized capital market at the multi-trillion-dollar scale will demand a higher level of assurance.
Digital Asset’s Isabelle/HOL verification demonstrated that this direction is technically feasible. Since first encountering that research in 2019, I have embedded the conviction that “compliance must be built in” throughout Oraclizer’s design. The result is Oraclizer’s compliant-by-design architecture — implemented as a proprietary multi-layered compliance-embedded architecture comprising RCP, OIP, the 4-Layer Privacy Stack, and OSS compliance verification, with DAML/Canton included as one component among them.
The problem that remains unsolved is composing heterogeneous verification regimes into a single coherent guarantee in cross-domain environments. This is not a challenge unique to Oraclizer but a structural problem that the entire RWA infrastructure will face. And the first step toward solving it is recognizing that the current level of regulatory assurance is not sufficient.
References
[1] 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
[2] Lochbihler, A. & Marić, O. (2020). “Authenticated Data Structures As Functors in Isabelle/HOL.” In: Formal Methods for Blockchain (FMBC 2020). OASIcs vol. 84, 6:1-6:15. https://doi.org/10.4230/OASIcs.FMBC.2020.6
[3] Digital Asset. (2021). “A semantic domain for privacy-aware smart contracts and interoperable sharded ledgers.” Lightning talk, Certified Proofs and Programs 2021. https://www.canton.io/publications/cpp2021-slides.pdf
[4] Nipkow, T., Paulson, L.C., Wenzel, M. (2002). Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer-Verlag.
[5] Isabelle — A Generic Proof Assistant. Technische Universität München. https://isabelle.in.tum.de/
[6] Marmsoler, D., Ahmed, A. & Brucker, A.D. (2025). “Secure Smart Contracts with Isabelle/Solidity.” In: SEFM 2024, LNCS vol. 15280. https://doi.org/10.1007/978-3-031-77382-2_10
[7] Bernauer, A. et al. (2023). “Daml: A Smart Contract Language for Securely Automating Real-World Multi-Party Business Workflows.” arXiv:2303.03749. https://arxiv.org/abs/2303.03749
Learn More
Read more on Oraclizer Research:
• RWA 2.0 Declaration: Blockchain Innovation That Embraces Legacy — A new tokenization paradigm that embraces legacy
• Why Oraclizer Chose DAML/CANTON — Why DAML/Canton was chosen from an institutional liquidity perspective
Follow us: https://x.com/Oraclizer
