Decentralized Finance (DeFi) has brought about decentralized applications which allow untrusted users to lend, borrow and exchange crypto-assets or crypto-derivatives. Many of such applications fulfill the role of markets or market makers, and thus feature complex, highly parametric incentive mechanisms to equilibrate interest rates or prices. This complexity makes the behaviour of DeFi archetypes difficult to understand and to predict: indeed, ineffective incentives and attacks could potentially lead to emergent unwanted behaviours. Reasoning about DeFi applications is made even harder by the lack of executable models of their behaviour: to precisely understand how users interact with DeFi instances, eventually one has to inspect their different implementations, where the incentive mechanisms are intertwined with low-level implementation details. To this end, we are developing new executable specifications of the DeFi archetypes lending pools and automatic market makers, allowing us to prove properties and precisely describe their interactions, vulnerabilities and attacks. In this presentation, we will provide an overview of this new line of research which aims to bridge the research communities of economic.