Towards a Theory of Decentralized Finance

Decentralized Finance (DeFi) has brought about decentralized applications which allow untrusted users to lend, borrow and exchange crypto-assets. Many of such applications fulfill the role of markets or market makers, featuring complex, highly parametric incentive mechanisms to equilibrate interest rates and prices. This complexity makes the behaviour of DeFi applications difficult to understand: indeed, ill-designed incentive mechanisms could potentially lead to emergent unwanted behaviours. We argue that theories, techniques and tools rooted in formal methods can provide useful instruments to better understand, specify and analyze DeFi systems. We summarize in this paper our first steps towards a theory of DeFi based on formal methods, and we overview the open challenges and opportunities for formal methods in DeFi.