Certifying optimal MEV strategies with Lean

Abstract

Advances in decentralized consensus have enabled applications for exchanging crypto-assets without trusted intermediaries. The rules governing these exchanges are typically encoded as smart contracts — computer programs executed by large-scale decentralized networks, that collectively record all interactions between users and smart contracts, together with their effect on asset ownership, on a public transactions ledger called blockchain. Although consensus protocols guarantee that the execution of smart contracts is faithful to their semantics, this alone is not sufficient to prevent attacks: namely, adversaries can respect the exchange rules and still be able to gain assets to the detriment of honest users. This systemic risk is exacerbated by Maximal Extractable Value (MEV) — a widespread class of attacks where the adversary profits by manipulating the ordering, inclusion, or exclusion of transactions in a blockchain. To date, MEV attacks have already extracted billions of dollars in value, underscoring their systemic impact on smart contracts security. In this paper, we present the first mechanized formalization of MEV, by introducing a Lean 4 library that supports the certification of MEV bounds for arbitrary smart contracts. We showcase our library by analysing the MEV of Automated Market Maker (AMMs), a core mechanism of decentralized financial protocols that enables the swap of assets at algorithmically computed exchange rates. Our main result is the first machine-checked proof of the optimality of arbitrage and sandwich attacks — two widespread MEV attacks to AMMs.