Formalization of MEV: Modeling, Security Requirements, and Mitigation Strategies

Maximal Extractable Value (MEV) threatens the fairness and decentralization of blockchain systems. It arises when entities controlling transaction ordering such as miners, validators, and builders exploit that position for financial gain, unbalancing incentives and undermining impartial execution. Despite prior work, the field remains fragmented: definitions conflict, terminology overlaps, and many studies focus on narrow behaviours while overlooking dynamics across roles and protocol layers. This paper formalises MEV as a role dependent optimisation problem that unifies attacker strategies, security requirements, and mitigation mechanisms within a single framework. We model adversarial behaviours including front-running, back-running, sandwiching, and suppression attacks and express MEV extraction as a constrained optimisation defined by actor roles, information asymmetries, and timing assumptions. On this foundation, we introduce a taxonomy of mitigation approaches covering proposer–builder separation (PBS) architectures, threshold-encryption and Verifiable Delay Function (VDF) schemes, mempool-secrecy techniques, priority gas auctions (PGAs) and auction-based mechanisms, machine-learning detection frameworks, and Layer 2 rollup sequencing designs. This view enables comparison of trade-offs in decentralisation, verifiability, latency, and trust assumptions. To demonstrate applicability, we analyse three samples, BEAST-MEV, SUAVE, and MEV-Boost, used as case studies of confidentiality, hybrid coordination, and economic separation. These examples show how mitigation philosophies can be compared through the model, revealing strengths, dependencies, and performance implications. The framework introduces metrics for sequencing fairness and mitigation effectiveness, unifies Proposer Extractable Value (PEV) and Builder Extractable Value (BEV) within a single model, and connects formalism to deployable protocol designs. The paper concludes by outlining challenges, including cross-domain MEV and shared sequencer dynamics.