MEV-Freedom, in DeFi and Beyond (Invited Talk)

Author Massimo Bartoletti

Thumbnail PDF


  • Filesize: 319 kB
  • 1 pages

Document Identifiers

Author Details

Massimo Bartoletti
  • University of Cagliari, Italy

Cite AsGet BibTex

Massimo Bartoletti. MEV-Freedom, in DeFi and Beyond (Invited Talk). In 4th International Workshop on Formal Methods for Blockchains (FMBC 2022). Open Access Series in Informatics (OASIcs), Volume 105, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Maximal Extractable Value (MEV) refers to a class of recent attacks on public blockchains, where adversaries with the power to reorder, drop or insert transactions in a block can "extract" value from user transactions in the mempool. Empirical research has shown that mainstream DeFi protocols, like e.g. Automated Market Makers and Lending Pools, are massively targeted by MEV attacks. This has detrimental effects on their users, on transaction fees, and on the congestion of blockchain networks. Despite the growing knowledge on MEV attacks on blockchain protocols, an exact definition is still missing. Indeed, formally defining these attacks is an essential prerequisite to the design of provably secure, MEV-free blockchain protocols. In this talk, we propose a formal definition of MEV, based on a general, abstract model of blockchains and smart contracts. We then introduce MEV-freedom, a property enjoyed by contracts resistant to MEV attacks. We validate this notion by rigorously proving that Automated Market Makers and Lending Pools are not MEV-free. We finally discuss how to design MEV-free contracts.

Subject Classification

ACM Subject Classification
  • Security and privacy → Formal methods and theory of security
  • Blockchain
  • Smart Contracts
  • Formal Security Notion


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads