https://writings.flashbots.net/research/formalization-mev/
Thanks to Phil Daian, Alex Obadia, and Mahimna Kelkar for plenty of discussions on the topic.
Since its introduction in the Flashboys 2.0 paper of 2019 by Daian et al., a lot has been said about Miner (now Maximal) Extractable Value, or MEV. In particular, the launch of the Flashbots Auction propelled what is today a billion dollar economy across various blockchains and centralized exchanges. From thrilling Twitter threads to academic research papers, the MEV phenomenon has captured a central spot in the cryptocurrency discourse. Oddly, however, there is no agreed upon formal definition of MEV.
While some may argue that the widely shared, intuitive notion of MEV will be sufficient in most scenarios, we believe that proper formalization is critical to establishing a foundation upon which complex theorizing can take place. As Tim Roughgarden put it in a recent talk on building a theory of DeFi, the first step before "easy" and later "difficult" theorems is to have definitions and basic vocabulary. Further, as was evidenced by a recent public discussion where some claimed that arbitrage is not MEV, it might even be the case that we don't share an intuitive notion of MEV after all! A unifying formal definition of MEV would certainly help.
As it turns out, however, formalizing MEV in a robust, general way is no easy task. In this post, we explore some of the difficulties we encounter when trying to come up with such a definition. We start by reviewing some of the existing formalizations, point out some of their problems, and go on a quest trying to amend some of them. While we present new definitions that improve on some of these issues, our main contribution rests in highlighting many of the subtleties involved, paving the way for a more systematic approach in future work around MEV.
The original Flashboys paper defines MEV as "the total amount of Ether miners can extract from manipulation of transactions within a given timeframe, which may include multiple blocks’ worth of transactions", but stays short of attempting a formal definition. Most recently, the widely adopted working definition rings something like:
MEV is the value that can be permissionlessly extracted by block proposers by reordering, censoring, or inserting transactions.
Perhaps the definition that comes closest to formalizing this is the one given in the recent Clockwork Finance paper via the following two expressions:
\mathsf{EV}(p,B,s)=\max_{(B_1, \ldots, B_k)\in B} \left\{ b(p, s_k)-b(p,s)\right\} \tag{1}
and:
Here, EV is the extractable value by player p in state s given a set of valid block sequences B, (B1,…,Bn) is one such sequence, and b(p,sk) is the balance of player p in the state resulting of applying blocks (B1,…,Bk) to s. k-MEV is the k-maximal extractable value by a player p in state s acting as block proposer, where validBlocksk is the set of all valid block sequences of k blocks that p can create, and single-block MEV is just 1-MEV.
These expressions were slightly tweaked from those in the paper for notational simplicity, but are otherwise equivalent. In particular, we consider balances of players as opposed to accounts (omitting a sum over accounts controlled by a player), and remove the explicit reference to the chain's native asset; we will return to this point later.
We will use this definition of MEV as a starting point, noting that most other papers provide similar definitions that face the same limitations, or do not provide formal definitions at all.
We start by noting a fatal flaw in the above expressions: the maximal extractable value depends on the player p! This means that if p has, say, some pending airdrop claim, their MEV will be larger than for a player who doesn't. While this might make sense for the extractable value, it is certainly at odds with the idea of a "permissionlessly extracted" value.
Upon closer inspection, it is not entirely clear what the notion of "player" is actually referring to. We can identify at least three intertwined meanings: i) a player as a transaction signer, having balances and controlling accounts, ii) a player as an actor in the protocol game, having (or lacking) block proposing rights, and iii) a player in the networking sense, a node operator affected by latencies and having a unique mempool view.
While the latter meaning does probably not apply in this formulation (although we will come back to it later), meanings i) and ii) are somewhat conflated: p certainly refers to i) when talking about balances in (1), but in going from (1) to (2) we also ascribe p block proposing rights, in line with meaning ii). We argue that a proper definition of MEV should be independent of the player in the sense of i), that is, it should not depend on particular signing rights. With respect to ii), we will define MEV given block proposing privileges. This effectively decouples the problem into value extraction on one hand, and obtaining sequencing rights on the other, which might prove useful when thinking about extraction costs, network security, etc.