Decentralized Finance (DeFi) applications are smart contracts that allow users to exchange crypto assets without the need of a central trusted authority. DeFi platforms hold dozens of billions of USD and process hundreds of millions worth of transactions daily. In a series of works [1-5] we have studied some of the most popular DeFi apps through the lens of formal methods. In this talk I will provide an overview of such works. We have designed models capturing the essence of those applications, and we have used those models to formalize some key properties of DeFi apps, including virtues of their incentive mechanisms and vulnerabilities that can be exploited by malicious agents. Our models are also executable, and hence amenable for automated reasoning and analysis.
