Document Open Access Logo

Smart Tests for a Smart Contract Language

Authors Miguel Valido , António Ravara

PDF

File

Thumbnail PDF
PDF
OASIcs.FMBC.2026.5.pdf
  • Filesize: 0.64 MB
  • 14 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Empirical software validation
Keywords
  • Smart contracts
  • Blockchain
  • Daml
  • Property-based testing
  • Hypothesis

Metrics

Abstract

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.

Cite As Get BibTex

Miguel Valido and António Ravara. Smart Tests for a Smart Contract Language. In 7th International Workshop on Formal Methods for Blockchains (FMBC 2026). Open Access Series in Informatics (OASIcs), Volume 142, pp. 5:1-5:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/OASIcs.FMBC.2026.5

Author Details

Miguel Valido
  • NOVA School of Science and Technology, Caparica, Portugal
António Ravara
  • NOVA School of Science and Technology, Caparica, Portugal

Funding

We acknowledge the support of NOVA LINCS (Grant no. UID/04516/2025) with the financial support of FCT.IP and EU Horizon Europe project TaRDIS (Grant Agreement no. 101093006).

Acknowledgements

We would like to thank the anonymous reviewers for their constructive feedback.

Supplementary Materials

References

  1. Property-based and stateful testing via hypothesis (brownie documentation). accessed 2025-08-29. URL: https://eth-brownie.readthedocs.io/en/stable/tests-hypothesis-property.html.
  2. Quickcheck. Accessed: 2025-01-15. URL: https://en.wikipedia.org/wiki/QuickCheck.
  3. Software testing: Property testing. Accessed: 2025-01-15. URL: https://en.wikipedia.org/wiki/Software_testing#Property_testing.
  4. Soliditycheck, 2019. URL: https://github.com/xf97/SolidityCheck.
  5. Solidity and smart contracts: A quick introduction, 2022. Accessed: 2025-01-22. URL: https://www.pluralsight.com/blog/software-development/what-is-solidity-smart-contracts.
  6. An introduction to daml, 2024. Accessed: 2025-01-22. URL: https://docs.daml.com/daml/intro/0_Intro.html#:~:text=Daml%20is%20a%20smart%20contract,abstract%20Daml%20Ledger%20Model%20Concepts.
  7. Testing smart contracts, 2024. Accessed: 2025-01-22. URL: https://ethereum.org/en/developers/docs/smart-contracts/testing.
  8. Daml json api documentation, 2025. Accessed: 2025-09-03. URL: https://docs.daml.com/json-api/.
  9. Danil Annenkov, Jakob Botsch Nielsen, and Bas Spitters. ConCert: a smart contract certification framework in Coq. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 215-228. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373829.
  10. Microsoft Azure. Blockchain workbench: Application and smart contract samples, 2018. Accessed: 2025-01-24. URL: https://github.com/Azure-Samples/blockchain/tree/master/blockchain-workbench/application-and-smart-contract-samples.
  11. Massimo Bartoletti, Fabio Fioravanti, Giulia Matricardi, Roberto Pettinau, and Franco Sainas. Towards Benchmarking of Solidity Verification Tools. In Bruno Bernardo and Diego Marmsoler, editors, 5th International Workshop on Formal Methods for Blockchains (FMBC 2024), volume 118 of Open Access Series in Informatics (OASIcs), pages 6:1-6:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/OASIcs.FMBC.2024.6.
  12. Rob Behnke. Learning daml: Advantages and challenges, 2023. Accessed: 2025-01-22. URL: https://www.halborn.com/blog/post/learning-daml-advantages-and-challenges.
  13. Alexander Bernauer, Sofia Faro, Rémy Haemmerle, Martin Huschenbett, Moritz Kiefer, Andreas Lochbihler, Jussi Mäki, Francesco Mazzoli, Simon Meier, Neil Mitchell, and Ratko G. Veprek. Daml: A smart contract language for securely automating real-world multi-party business workflows. CoRR, abs/2303.03749, 2023. URL: https://doi.org/10.48550/arXiv.2303.03749.
  14. Maryna Cherednychenko. Daml or solidity: What should you choose for smart contracts?, 2025. Accessed: 2025-01-22. URL: https://erbis.com/blog/daml-vs-solidity/#:~:text=Daml%20and%20Solidity%20are%20some,many%20blockchain%20platforms%20behind%20it.
  15. Peer D. Understanding state management: Functional programming vs. imperative approaches, 2024. Accessed: 2025-01-22. URL: https://peerdh.com/blogs/programming-insights/understanding-state-management-functional-programming-vs-imperative-approaches.
  16. Ikram Garfatta, Kais Klai, Walid Gaaloul, and Mohamed Graiet. A Survey on Formal Verification for Solidity Smart Contracts. In 2021 Australasian Computer Science Week Multiconference, pages 1-10. ACM, 2021. URL: https://doi.org/10.1145/3437378.3437879.
  17. Kevin George. The largest cryptocurrency hacks so far, 2024. Accessed: 2025-01-23. URL: https://www.investopedia.com/news/largest-cryptocurrency-hacks-so-far-year/.
  18. Harrison Goldstein, Joseph W. Cutler, Daniel Dickstein, Benjamin C. Pierce, and Andrew Head. Property-Based Testing in Practice. In Proceedings of the IEEE/ACM 46th International Conference on Software Engineering. ACM, 2024. URL: https://doi.org/10.1145/3597503.3639581.
  19. Harrison Goldstein, Jeffrey Tao, Zac Hatfield-Dodds, Benjamin C. Pierce, and Andrew Head. Tyche: Making Sense of PBT Effectiveness. In Proceedings of the 37th Annual ACM Symposium on User Interface Software and Technology. ACM, 2024. URL: https://doi.org/10.1145/3654777.3676407.
  20. Hypothesis Works. Hypothesis quickstart guide. Version 6.138.3. URL: https://hypothesis.readthedocs.io/en/latest/quickstart.html.
  21. Abdul Sami Jay. Property-based testing & fuzzing smart contracts, 2022. Accessed: 2025-01-23. URL: https://abdulsamijay.github.io/posts/fuzzing-property-testing.
  22. Bo Jiang, Ye Liu, and W. K. Chan. ContractFuzzer: fuzzing smart contracts for vulnerability detection. In Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering. ACM, 2018. URL: https://doi.org/10.1145/3238147.3238177.
  23. Cem Kaner. Measuring the effectiveness of software testers, 2003. Supported by NSF Grant EIA-0113539, Improving the Education of Software Testers. URL: https://web.archive.org/web/20100326042728/http://www.testingeducation.org/a/mest.pdf.
  24. Kaan Kaçar. Solidity security practices part viii: Property-based testing, 2023. Accessed: 2025-01-30. URL: https://medium.com/coinmonks/solidity-security-practices-part-viii-property-based-testing-430daf391231.
  25. Satpal Singh Kushwaha, Sandeep Joshi, Dilbag Singh, Manjit Kaur, and Heung-No Lee. Ethereum Smart Contract Analysis Tools: A Systematic Review. IEEE Access, 10:57037-57062, 2022. URL: https://doi.org/10.1109/ACCESS.2022.3169902.
  26. Ye Liu, Yue Xue, Daoyuan Wu, Yuqiang Sun, Yi Li, Miaolei Shi, and Yang Liu. PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation, 2024. URL: https://doi.org/10.14722/ndss.2025.241357.
  27. Haoyang Ma, Wuqi Zhang, Qingchao Shen, Yongqiang Tian, Junjie Chen, and Shing-Chi Cheung. Towards Understanding the Bugs in Solidity Compiler. In Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 1312-1324. ACM, 2024. URL: https://doi.org/10.1145/3650212.3680362.
  28. David MacIver, Zac Hatfield-Dodds, and Many Contributors. Hypothesis: A new approach to property-based testing. Journal of Open Source Software, 4(43), 2019. URL: https://doi.org/10.21105/joss.01891.
  29. Bertrand Meyer. Seven Principles of Software Testing. Computer, pages 99-101, 2008. URL: https://se.inf.ethz.ch/~meyer/publications/testing/principles.pdf.
  30. Mikkel Milo, Eske Hoy Nielsen, Danil Annenkov, and Bas Spitters. Finding Smart Contract Vulnerabilities with ConCert’s Property-Based Testing Framework. OASIcs, Volume 105, FMBC 2022, 105:2:1-2:13, 2022. Artwork Size: 13 pages, 863331 bytes ISBN: 9783959772501 Medium: application/pdf Publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/OASIcs.FMBC.2022.2.
  31. Bernard Njenga. Comparison between daml and solidity, 2022. Accessed: 2025-01-22. URL: https://bernardnjenga.hashnode.dev/comparison-between-daml-and-solidity.
  32. pytest-dev team. pytest-xdist. Accessed 2025-09-13. URL: https://pytest-xdist.readthedocs.io/en/stable/.
  33. Emanuel Trandafir. A guide to property-based testing in kotlin, 2024. Reviewed by Vinicius Peixoto, Accessed: 2025-02-05. URL: https://www.baeldung.com/kotlin/property-based-testing.
  34. Miguel Valido. Hypothesis2Daml. Software (visited on 2026-03-30). URL: https://github.com/miguelvalido/Hypothesis2Daml (visited on 2026-03-30). URL: https://github.com/miguelvalido02/Hypothesis2Daml
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.25682
  35. Miguel Valido. Hypothesis2daml, 2025. URL: https://github.com/miguelvalido02/Hypothesis2Daml.
  36. Cindy Wauters and Coen De Roover. Property-based testing within ml projects: an empirical study. In 2024 IEEE International Conference on Software Maintenance and Evolution (ICSME), pages 648-653, 2024. URL: https://doi.org/10.1109/ICSME58944.2024.00067.
  37. Krl Ziborov. Formal verification of smart contracts in the concert framework, 2025. Accessed: 2025-01-30. URL: https://securityboulevard.com/2025/01/formal-verification-of-smart-contracts-in-the-concert-framework.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact