A formal framework for the economic security of DeFi compositions

Decentralised Finance (DeFi) protocols are usually built by composing a variety of smart contracts. Although composability is a key driver of DeFi innovation, it also introduces security risks: adversaries may exploit interactions between newly deployed contracts and the existing blockchain state to cause economic losses. We introduce a formal security notion for DeFi composability, called MEV non-interference, which requires that interactions with the existing blockchain state do not increase the Maximal Extractable Value (MEV) obtainable from a set of newly deployed contracts. To formalise this notion, we define local MEV, a new measure of economic attacks that quantifies the losses incurred by a given set of victim contracts. We study MEV non-interference under two adversarial models, corresponding to bounded and unbounded adversarial wealth, and establish sufficient conditions and locality principles that enable modular reasoning about secure composability. We apply our framework to representative DeFi compositions including exchanges, automated market makers, options, lending pools, routers, and arbitrage contracts, and show that it distinguishes secure compositions from vulnerable ones. Our results provide a formal foundation for analysing the economic security of DeFi systems built through smart contract composition.