Smart Contract Security for Institutional Finance on Canton: An Entirely Different Problem

It would not be wrong to say that a big part of the smart contract security industry as it exists today has been purpose built for Ethereum. The tools, taxonomies, and threat models all assume a specific architecture: shared mutable state, a public mempool, and an open execution model. This foundation is undoubtedly excellent and has helped secure billions in on-chain funds. However, the Canton Network provides an alternate architecture for smart contracts that settle institutional transactions. This alternate model is exactly what the Digital Asset team has delivered with their smart contract language, Daml.

Built for regulated financial institutions and running on the Canton Network, it counts Goldman Sachs, DTCC, JPMorgan, Broadridge, BNY Mellon, Citadel Securities, and LSEG among its nearly 600 ecosystem participants. With over $6 trillion in on-chain real-world assets, the Canton Network, powered by Daml, has positioned itself to be a major player in the future of digital global finance.

During the course of our research, what we found expanded how we think about smart contract security, and led us to create three new open source tools for Daml smart contract correctness and security, described below. But the shift in thinking starts with better understanding the differences between Ethereum and Canton.

Two Architectures, Two Threat Surfaces

Ethereum uses an account-based model, with a shared, mutable state. A contract has storage slots, and any authorized caller can invoke a function that mutates the data stored in these slots. The entire chain state and all pending transactions are globally visible.

This design gives rise to a specific and well-documented set of vulnerabilities. For instance, reentrancy arises because an external call can invoke arbitrary code before the calling contract's state update completes. Front-running and sandwich attacks exploit the public mempool, where pending transactions are visible to all participants before confirmation. Oracle manipulation takes advantage of on-chain price feeds that any participant can distort within a single transaction. These are not random bugs. Each can be traced back to an architectural choice: globally visible state, a public transaction queue, and an open execution model where any contract can call any other contract's public interface by default.

On the other hand, Canton uses a fundamentally different architecture. It uses Daml as its smart contract language, which is built on top of a typed functional core based on Haskell (the Daml compiler uses a fork of the GHC frontend). The smart contracts are defined with algebraic data types, and the type system enforces rules at compile time. The execution model is an extended UTXO system: contracts are immutable, you don't update them, you archive the old one and create a new one. Transaction views are encrypted per-recipient, and the sequencer and mediator coordinate consensus without ever seeing transaction content. Double spending is prevented by a lock-based conflict-detection protocol: if two transactions attempt to archive the same contract, the sequencer's ordering determines priority, and the later transaction is rejected. The protocol runs on a two-phase commit scheme with cryptographic commitments and sequencer-enforced ordering.

The consequences are structural. Reentrancy cannot occur because the execution model does not allow arbitrary external calls within a transaction. MEV extraction is not possible because there is no public mempool and the sequencer only sees encrypted payloads. The sequencer cannot reorder based on content it cannot read. The oracle-manipulation surface is narrower than on public blockchains: the privacy model limits attacker visibility into contract state, and no flash loan facility currently exists in the Canton ecosystem to amplify capital-free attacks. The mediator only receives an informee tree (participant identities, transaction tree shape, confirmation responses), while the sequencer only sees sender/recipient identities, message sizes, and timing.

However, this does not mean that Daml contracts are free of bugs. It means that the bugs are different from those found in Solidity contracts.

The Bug Classes That Matter

The crypto security community has built an impressive vulnerability taxonomy over the past decade. Standardized contract libraries, static analyzers, fuzzers, formal verification tools, audit methodologies. The quality of that work is genuinely high, but none of it directly applies to Daml-based smart contracts. The detectors check for vulnerability classes that cannot exist in an extended UTXO model. However, the disciplines, including static analysis, property-based testing, formal verification, adversarial threat modeling still fully carry over. It’s just that they simply need to be directed at a different attack surface.

As a result of our analysis of Daml smart contracts, we were able to identify the following classes of bugs.

Conservation violations

In a system with multiple transfer paths — self-transfer for merging tokens, direct transfer via preapproval, two-step transfer through locked holdings — the invariant that total inputs equal total outputs must hold across every path. When there are three paths, each with different intermediary steps, it is remarkably easy to get one wrong.

Arithmetic faults arising from governance-controlled parameters

Daml contracts frequently contain parameters set by governance choices: a price field, a fee rate, a cap-per-coupon value. These values flow into arithmetic operations. Daml raises an `ArithmeticError` on overflow and division by zero, which aborts the entire transaction. If a governance-controlled value appears as a denominator (and this occurs frequently), a misconfiguration can render an entire workflow inoperable. This is not a code defect. It is a defect in the relationship between code and configuration. The code trusts the governance process, which in turn is operated by humans.

Temporal assumptions in settlement logic

Daml's time model is what the documentation calls "slightly fuzzy". The submitting participant proposes a ledger time, and the synchronizer's sequencer assigns a record time. The protocol enforces a bounded skew between the two, if the gap exceeds the configured tolerance, the transaction is rejected. Settlement logic that enforces deadlines using getTime needs to account for this: a transaction submitted near a deadline boundary may be rejected not because it was late, but because the skew between proposed and recorded time pushed it outside the tolerance window. The fuzziness is configurable per synchronizer, but any contract logic that treats ledger time as precise wall-clock time is making an assumption that the protocol does not guarantee explicitly.

Across synchronizers, the problem is exacerbated. The documentation is explicit: there is no global causality guarantee across synchronizers. Events from different synchronizers can arrive in any order. A contract created on one synchronizer, reassigned to another, and then archived may emit those events in a different sequence than expected. Reassignments themselves are non-atomic two-phase operations: unassign from source, assign to target, with a "pending assignment" limbo between them. While getTime is monotonic along transaction dependencies, there is no global ordering across synchronizers. Any settlement logic that assumes ordered timestamps across synchronizer boundaries is making an assumption the protocol does not provide.

Non-deterministic ordering at the application boundary

Canton guarantees causal consistency, not total ordering. Multiple participants can return the same set of contracts in different sequences. Application code that selects the first result of an unordered query compiles, passes single-node tests, and fails intermittently in production. Any logic depending on "first" or "oldest" without explicitly sorting on a contract field is a latent defect.

The above-described bug classes do not appear in the SWC Registry or any existing vulnerability classification. They are structurally different bugs from a structurally different execution model.

Building the Verification Stack

When we began delving into Daml, it had no adversarial-focused security tooling. The compiler caught type errors and a linter checked the style. However, the classes of bugs that matter in Daml smart contracts (e.g., conservation violations, governance-triggered arithmetic faults, and temporal ordering mistakes) were left to manual review. To address this, we built three tools: daml-lint, daml-props, and daml-verify. What we learned from building them was not that any individual technique was novel, but that applying these tools together, each catching what the other may miss, is what improves confidence in a smart contract's correctness.

Static Analysis

The first tool is daml-lint, a static analysis scanner written in Rust. The approach follows the model that Slither established for Solidity: AST-walking detectors that pattern-match against known vulnerability classes.

Daml does not expose a public AST format, so we used haskell-tree-sitter as the parser foundation (Daml is syntactically close to Haskell), with a keyword shim to recognize Daml-specific declarations: template, choice, signatory, observer, ensure, key, maintainer. A custom extraction layer builds an intermediate representation (IR) of templates, choices, and their bodies.

The IR stores both raw text and parsed statement types. This dual representation was the key design decision. Some detectors require structural reasoning — verifying that an assertion precedes a try/catch block. Others only need to locate a division operator and check whether the denominator is guarded. Both representations are available to each detector.

We shipped six detectors targeting the bug classes described above: missing “ensure” clauses on decimal fields, unguarded division, non-deterministic ordering in application-level queries (via the Ledger API), unbounded fields in persistent contracts, and missing positive-amount assertions on choice parameters. Note: Daml itself has no on-ledger query primitives; this refers to client-side logic consuming Ledger API results.

Pattern matching is effective for known vulnerability classes. But patterns are syntactic. They catch what we already know to look for. The bugs that matter most are semantic. That is, they concern the relationship between operations over time.

Property-Based Testing

The second tool is daml-props, a property-based testing framework written in pure Daml. The approach follows the lineage of QuickCheck for Haskell and Echidna for Solidity, adapted to Daml’s constraints without relying on typeclasses or IO, and using a Park–Miller linear congruential generator as the only available pseudorandom number generator (PRNG).

The core abstraction is the stateful sequence test. We define an action type, an executor that applies actions to state, and an invariant that must hold after every step. The framework generates random sequences of actions, executes them, checks the invariant, and when it finds a violation, shrinks the failing sequence to a minimal reproduction.

The shrinking is what distinguishes this from random testing. Identifying a violation with a 47-step sequence is informative, but reducing it to a 1-step minimal reproduction is actionable.

Property-based testing explores the space between what developers intend and what code permits. However, "hundreds of random inputs" is not "all inputs", which brings us to formal verification.

Formal Verification

The third tool is daml-verify, which uses Z3 prover to prove that critical invariants hold for all possible inputs. Not for one sample, but for every decimal value, every timestamp, and every combination of inputs and outputs.

We write symbolic models of Daml logic in Python using Z3 variables, then define properties as precondition-goal pairs. The prover checks satisfiability of the preconditions conjoined with the negation of the goal. If unsatisfiable (i.e., no input exists that satisfies the preconditions while violating the goal), the property is proved universally. If satisfiable, Z3 produces a counterexample.

We verified 14 properties across four categories:

• Conservation: Receiver amount plus sender change equals the total input, across all transfer paths.
• Division safety: Every division has a non-zero denominator. This is where formal verification proved to be the most valuable.
• Temporal: Settlement deadlines are well-ordered across synchronizer boundaries.
• Vault: Collateral ratio guards hold, liquidation conserves value, debt accrual is monotonic.

We chose manual model construction over automatic extraction similar to the approach Certora uses with their CVL specifications for Solidity. To mitigate the risk of model-code divergence, we built a validation protocol: every model is checked line-by-line against the Daml source.

Why Three Tools?

Each tool is a layer that catches what the other layers may miss.

While static analysis identifies syntactic patterns (known vulnerability classes and structural anti-patterns), it cannot reason about the relationship between operations across time. Property-based testing discovers semantic bugs by exploring the input space, but it only checks the inputs it generates, and “hundreds” is not “all”. Formal verification proves properties universally, for all inputs. However, it operates on a model, not the code itself, and is only as faithful as the model.

Once these layers are composed, the gaps close. In our tests, daml-lint found the unguarded divisions. daml-props found the zero-input mint, while daml-verify proved the conservation properties that testing alone could only approximate.

There is a natural analogy to depth of field. Unit tests are precise in the scenarios that the developer anticipated. Property-based testing widens the aperture to include scenarios no one thought to check. Formal verification extends focus to the entire input space. Confidence requires all three focal lengths.

What This Means

There is a parallel and growing universe of Daml smart contracts on the Canton Network that many in the blockchain security community have not yet examined. It runs critical financial infrastructure that institutions depend on. Its security model is fundamentally different from the one the crypto world has spent years studying. The difference between "smart contract security" as practiced in the public blockchain ecosystem and the Canton Network is substantial. The two domains use the same vocabulary — smart contracts, ledgers, tokens, settlement — but they refer to different architectures, face different threats, and require different tools.

Verification and security requires more than a tool. It requires a stack. The value of that stack exceeds the sum of its layers, because each layer covers the blind spots of the others. In financial infrastructure, where the cost of a missed defect is measured in real capital and potential regulatory consequence, this composition of layers is what matters.

FAQs

What makes smart contract security on the Canton Network different from Ethereum?

Canton uses an extended UTXO model with encrypted transaction views and no public mempool, which eliminates entire vulnerability classes common to Ethereum, such as reentrancy, MEV extraction, and oracle manipulation. However, Canton introduces its own distinct risk surface: conservation violations across transfer paths, arithmetic faults triggered by governance-controlled parameters, and temporal ordering issues in settlement logic. Securing Daml smart contracts requires purpose-built tools and methodologies, not a direct port of Ethereum security tooling.

What are the most critical bug classes in Daml smart contracts?

Based on OpenZeppelin's research, the most significant bug classes in Daml smart contracts are: (1) conservation violations, where total inputs fail to equal total outputs across all transfer paths; (2) arithmetic faults arising from governance-controlled parameters — particularly unguarded division where a misconfigured denominator can halt an entire workflow; (3) temporal assumption errors in settlement logic, where ledger time fuzziness and cross-synchronizer ordering can cause transactions to be rejected or processed out of sequence; and (4) non-deterministic ordering at the application boundary, where unsorted query results produce latent, intermittent production failures.

Why does securing institutional financial infrastructure on-chain require a multi-layered verification approach?

No single verification technique covers the full risk surface of smart contracts running financial infrastructure. Static analysis catches known syntactic vulnerability patterns but cannot reason about semantic relationships between operations over time. Property-based testing explores unexpected input combinations but only samples the input space. Formal verification proves invariants hold for all possible inputs, but operates on a model rather than the code itself. Composing all three layers — as OpenZeppelin has done with daml-lint, daml-props, and daml-verify — is what closes the gaps and provides institutional-grade security confidence.

What open source tools has OpenZeppelin developed for Daml smart contract security?

OpenZeppelin developed three open source tools specifically for Daml smart contract correctness and security: daml-lint, a Rust-based static analysis scanner with six detectors targeting Daml-specific vulnerability classes; daml-props, a property-based testing framework written in pure Daml that generates random action sequences and shrinks failures to minimal reproductions; and daml-verify, a formal verification tool using the Z3 prover to prove that critical invariants — covering conservation, division safety, temporal ordering, and collateral management — hold across all possible inputs.

Why does smart contract security matter as traditional finance moves on-chain?

As financial institutions, asset managers, and settlement infrastructure migrate to blockchain networks like Canton, the smart contracts underpinning those systems become critical financial infrastructure. A defect in a Daml smart contract governing tokenized assets or settlement logic carries real capital consequences and potential regulatory risk. Applying rigorous, layered security assessments — adapted to the specific architecture and threat surface of each network — is the security standard that on-chain financial infrastructure demands.