Maximal Extractable Value (MEV) refers to a class of attacks to decentralized applications where the adversary profits by manipulating the ordering, inclusion, or exclusion of transactions in a blockchain. Decentralized Finance (DeFi) protocols are a primary target of these attacks, as their logic depends critically on transaction sequencing. To date, MEV attacks have already extracted billions of dollars in value, underscoring their systemic impact on blockchain security. Verifying the absence of MEV attacks requires determining suitable upper bounds, i.e. proving that no adversarial strategy can extract more value (if any) than expected by protocol designers. This problem is notoriously difficult: the space of adversarial strategies is extremely vast, making empirical studies and pen-and-paper reasoning insufficiently rigorous. In this paper, we present the first mechanized formalization of MEV in the Lean theorem prover. We introduce a methodology to construct machine-checked proofs of MEV bounds, providing correctness guarantees beyond what is possible with existing techniques. To demonstrate the generality of our approach, we model and analyse the MEV of two paradigmatic DeFi protocols. Notably, we develop the first machine-checked proof of the optimality of sandwich attacks in Automated Market Makers, a fundamental DeFi primitive.

翻译：最大可提取价值（MEV）指一类针对去中心化应用的攻击，攻击者通过操纵区块链中交易的排序、包含或排除来获利。去中心化金融（DeFi）协议是这类攻击的主要目标，因其逻辑高度依赖于交易排序机制。迄今为止，MEV攻击已攫取数十亿美元价值，凸显其对区块链安全的系统性影响。验证MEV攻击的缺失需要确定合适的上界，即证明任何对抗策略所能提取的价值（若存在）均不超过协议设计者的预期值。该问题 notoriously 困难：对抗策略空间极其庞大，使得实证研究与纸笔推演均缺乏严谨性。本文首次在Lean定理证明器中实现了MEV的机械化形式化。我们提出一种构建机器可验证的MEV边界证明的方法论，提供超越现有技术可能性的正确性保证。为展示方法的通用性，我们对两个典型DeFi协议的MEV进行建模分析。特别地，我们针对自动化做市商这一基础DeFi原语，首次实现了三明治攻击最优性的机器验证证明。