Smart Tests for a Smart Contract Language

Smart contracts are high-stakes software: their immutable, publicly accessible, code may govern assets worth millions, meaning that even minor defects can have severe consequences. The most used techniques to ensure smart contract correctness are testing and formal verification. Testing is almost always employed but is often restricted to unit tests (which often miss edge cases) and has limited coverage, while formal verification can provide strong guarantees but is often costly and complex to apply, demanding substantial time and expertise. Property-based testing bridges this gap by exploring large input spaces and shrinking failures to minimal counterexamples, helping uncover defects early in development. Formal verification can be left to critical features once testing has filtered out common issues. To add to the challenges smart contract developers face, most languages used were not designed with safety and security guarantees built-in. Daml is a smart contract language designed with correctness in mind, featuring a strong static type system, functional programming paradigms, and built-in abstractions for common smart contract patterns. However, Daml currently lacks support for property-based testing, limiting developers' ability to systematically explore input spaces and verify contract properties. This paper introduces Hypothesis2Daml, an open-source library that brings property-based testing to the Daml ecosystem by connecting the Hypothesis testing framework with the Daml JSON API. Hypothesis2Daml enables developers to specify invariants, preconditions, and stateful workflows over realistic ledger interactions, while providing automatic input generation, shrinking, and isolation of ledger state between test cases. The approach is evaluated using a benchmark consisting of eight contracts, three Daml templates, and twenty-eight property-based tests covering happy paths, negative cases, and alternative interaction orders. The results show that property-based testing is feasible for Daml smart contracts, can systematically expose violated properties with minimal counterexamples, and supports effective debugging of realistic, stateful workflows.