Aarhus University Seal

Formalising Decentralised Exchanges in Coq

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperConference articleResearch


The number of attacks and accidents leading to significant losses of crypto-assets is growing. According to Chainalysis, in 2021, approx. $14 billion has been lost due to various incidents, and this number is dominated by Decentralized Finance (DeFi) applications. To address these issues, one can use a collection of tools ranging from auditing to formal methods. We use formal verification and provide the first formalisation of a DeFi contract in a foundational proof assistant capturing contract interactions. We focus on Dexter2, a decentralized, non-custodial exchange for the Tezos network similar to Uniswap on Ethereum. The Dexter implementation consists of several smart contracts. This poses unique challenges for formalisation due to the complex contract interactions. Our formalisation includes proofs of functional correctness with respect to an informal specification for the contracts involved in Dexter's implementation. Moreover, our formalisation is the first to feature proofs of safety properties of the interacting smart contracts of a decentralized exchange. We have extracted our contract from Coq into CameLIGO code, so it can be deployed on the Tezos blockchain. Uniswap and Dexter are paradigmatic for a collection of similar contracts. Our methodology thus allows us to implement and verify DeFi applications featuring similar interaction patterns.

Original languageEnglish
JournalCPP 2023 - Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2023
Pages (from-to)290-302
Number of pages13
Publication statusPublished - 11 Jan 2023
Event12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023 - Co-located with POPL 2023 - Boston, United States
Duration: 16 Jan 202317 Jan 2023


Conference12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023 - Co-located with POPL 2023
CountryUnited States

Bibliographical note

Funding Information:
We would like to thank the LIGO team and in particular Tom Jack, Raphaël Cauderlier, Exequiel Rivas, Rémi Lesénéchal and Gabriel Alfour for the pleasant discussions. This research was partially supported by a grant from Nomadic Labs, by the Concordium Blockchain Research Center, and by a grant from CopenhagenFinTech.

Publisher Copyright:
© 2023 ACM.

    Research areas

  • blockchain, Coq, decentralized finance, smart contracts, software correctness

See relations at Aarhus University Citationformats

ID: 308234344