SMART TESTS FOR SMART CONTRACT LANGUAGES
Miguel Valido · Portuguese National Funding Agency for Science, Research and Technology (RCAAP Project by FCT) · 2025
Smart contracts are high-stakes software: their immutable, publicly accessible code may govern assets worth millions. This means that even minor defects can have severe consequences. Unit tests often miss edge cases. Although formal verification is the only route to full correctness, it demands substantial time and expertise. Property-based testing bridges this gap by exploring large input spaces and shrinking failures to minimal counterexamples. Used early, it filters defects and prioritises verification effort on code already validated by tests. Although Solidity benefits from a mature testing ecosystem, comparable support for other languages such as Daml remains limited. This dissertation addresses this gap by introducing Hypothesis2Daml, an open-source library that brings property-based testing to Damlby connecting Hypothesis withthe Daml JSON API. Hypothesis2Daml enables developers to specify invariants, pre/postconditions, and stateful workflows over realistic ledger interactions. It provides automatic input generation, shrinking to minimal counterexamples, party isolation per example, and request helpers that keep tests focused on properties rather than HTTP/JSON wiring. The approach is validated on a benchmark of eight contracts and twenty-seven properties that range from simple invariants to multi-step, role-sensitive workflows. All properties held under testing, with runs completing within practical time bounds, demonstrating that property-based testing is feasible and effective for Daml applications. A comparative evaluation situates Hypothesis2Daml among established tools and methods, highlighting strengths in usability and expressiveness, and acknowledging a throughput trade-off due to JSON-API transport overhead. Contributions include the Hypothesis2Daml library and a reusable benchmark with representative properties. Limitations concern transport overhead, ecosystem specificity, and dependence on developer-authored properties and generators. Future work targets automation, performance, andscope expansion. Together, these results establish a practical path for making property-based testing a routine part of building Daml applications.