Formal Modeling and Liquidity Improvement in DeFi

Liquidity underpins the efficiency and stability of Decentralised Finance (DeFi). With Decentralized Exchanges (DEXs), new paradigms of provision and trading emerge, making it vital to understand liquidity dynamics, from liquidity-saving mechanisms (LSMs) to aggregators that fuse on- and off-chain depth. This thesis develops three approaches to confronting liquidity challenges. First, we adapt netting LSM to DeFi to minimise the liquidity required by Automated Market Makers execution, introducing a queuing mechanism that selects liquidity feasible sequences and settles them atomically on-chain. Second, we formalize intent-based protocols, where users declare outcomes, solvers compete to realize them, and on-chain settlement verifies correctness in a single workflow. Our model captures the mechanisms related to intent aggregation, solver competition, and trade settlement, addressing liquidity fragmentation, execution inefficiency, and gas costs while enhancing scalability, composability, and user experience. Finally, we present a core calculus for Ethereum smart contracts that adds code-level policy constructs to monitor and enforce desired behaviors during external calls. It detects classic vulnerabilities (e.g., reentrancy) and enforces behavioral properties over execution traces, augmenting static analysis with runtime safeguards. Against the backdrop of DEX price fragmentation, where identical assets trade at different prices across venues, we examine the inefficiencies and vulnerabilities, focusing on liquidity-driven price manipulation attacks (e.g. flash loan arbitrage).