# Formal Analysis of Composable DeFi Protocols

arXiv: https://arxiv.org/abs/2103.00540 · HTML: https://mlsanity.com/paper/2103.00540/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Feb 2021.

## Built on by (most cited first, 3 of 3)

- [PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation](https://mlsanity.com/paper/2405.02580/) (2024)
- [Investigating Similarities Across Decentralized Financial (DeFi) Services](https://mlsanity.com/paper/2404.00034/) (2024)
- [DMind-3: A Sovereign Edge--Local--Cloud AI System with Controlled Deliberation and Correction-Based Tuning for Safe, Low-Latency Transaction Execution](https://mlsanity.com/paper/2602.11651/) (2026)

## Abstract (arXiv)

Decentralized finance (DeFi) has become one of the most successful applications of blockchain and smart contracts. The DeFi ecosystem enables a wide range of crypto-financial activities, while the underlying smart contracts often contain bugs, with many vulnerabilities arising from the unforeseen consequences of composing DeFi protocols together. In this paper, we propose a formal process-algebraic technique that models DeFi protocols in a compositional manner to allow for efficient property verification. We also conduct a case study to demonstrate the proposed approach in analyzing the composition of two interacting DeFi protocols, namely, Curve and Compound. Finally, we discuss how the proposed modeling and verification approach can be used to analyze financial and security properties of interest.