Finding Smart Contract Vulnerabilities with ConCert’s Property-Based Testing Framework

Authors Mikkel Milo , Eske Hoy Nielsen , Danil Annenkov , Bas Spitters

Thumbnail PDF


  • Filesize: 0.82 MB
  • 13 pages

Document Identifiers

Author Details

Mikkel Milo
  • Department of Computer Science, Aarhus University, Denmark
Eske Hoy Nielsen
  • Department of Computer Science, Aarhus University, Denmark
Danil Annenkov
  • Department of Computer Science, Aarhus University, Denmark
Bas Spitters
  • Department of Computer Science, Aarhus University, Denmark


We would like to thank the LIGO team and in particular Tom Jack, Raphaël Cauderlier, Exequiel Rivas, Rémi Lesénéchal, Gabriel Alfour, Thomas Letan and Arvid Jakobsson for the discussions about testing for LIGO.

Cite AsGet BibTex

Mikkel Milo, Eske Hoy Nielsen, Danil Annenkov, and Bas Spitters. Finding Smart Contract Vulnerabilities with ConCert’s Property-Based Testing Framework. In 4th International Workshop on Formal Methods for Blockchains (FMBC 2022). Open Access Series in Informatics (OASIcs), Volume 105, pp. 2:1-2:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


We provide three detailed case studies of vulnerabilities in smart contracts, and show how property based testing would have found them: 1. the Dexter1 token exchange; 2. the iToken; 3. the ICO of Brave’s BAT token. The last example is, in fact, new, and was missed in the auditing process. We have implemented this testing in ConCert, a general executable model/specification of smart contract execution in the Coq proof assistant. ConCert contracts can be used to generate verified smart contracts in Tezos' LIGO and Concordium’s rust language. We thus show the effectiveness of combining formal verification and property-based testing of smart contracts.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal methods
  • Software and its engineering → Software verification and validation
  • Smart Contracts
  • Formal Verification
  • Property-Based Testing
  • Coq


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Guillermo Angeris, Hsien-Tang Kao, Rei Chiang, Charlie Noyes, and Tarun Chitra. An Analysis of Uniswap markets. Cryptoeconomic Systems, 1(1), 2021. URL:
  2. Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, and Bas Spitters. Extracting Smart Contracts Tested and Verified in Coq. In CPP'2020. Association for Computing Machinery, 2021. URL:
  3. Danil Annenkov, Jakob Botsch Nielsen, and Bas Spitters. ConCert: A Smart Contract Certification Framework in Coq. In CPP'2020, 2020. URL:
  4. Bruno Bernardo, Raphaël Cauderlier, Zhenlei Hu, Zhenlei Pesin, and Julien Tesson. Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts. In FMBC19, 2019. Google Scholar
  5. James Chapman, Roman Kireev, Chad Nester, and Philip Wadler. System F in Agda, for fun and profit. In MPC'19, 2019. URL:
  6. Kim Grauer, Will Kueshner, and Henry Updegrave. Chainalysis 2022 Crypto Crime Report. Chainalysis 2022, 2022. URL:
  7. Gustavo Grieco, Will Song, Artur Cygan, Josselin Feist, and Alex Groce. Echidna: effective, usable, and fast fuzzing for smart contracts. In Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 557-560, 2020. URL:
  8. Zoe Paraskevopoulou, Catalin Hritcu, Maxime Dénès, Leonidas Lampropoulos, and Benjamin C. Pierce. Foundational property-based testing. In Christian Urban and Xingyuan Zhang, editors, 6th International Conference on Interactive Theorem Proving (ITP), volume 9236 of Lecture Notes in Computer Science, pages 325-343. Springer, 2015. URL:
  9. Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter. The MetaCoq Project. Journal of Automated Reasoning, February 2020. URL:
  10. Qingzhao Zhang, Yizhuo Wang, Juanru Li, and Siqi Ma. EthPloit: From Fuzzing to Efficient Exploit Generation against Smart Contracts. In 2020 IEEE 27th International Conference on Software Analysis, Evolution and Reengineering (SANER), 2020. URL:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail