Certifying optimal MEV strategies with Lean

• URL: http://arxiv.org/abs/2510.14480v1
• Date: Thu, 16 Oct 2025 09:24:28 GMT
• Title: Certifying optimal MEV strategies with Lean
• Authors: Massimo Bartoletti, Riccardo Marchesin, Roberto Zunino,
• Abstract summary: We present the first mechanized formalization of Maximal Extractable Value (MEV)<n>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.<n>We introduce a methodology to construct machine-checked proofs of MEV bounds, providing correctness guarantees beyond what is possible with existing techniques.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• One Token Embedding Is Enough to Deadlock Your Large Reasoning Model [91.48868589442837]
  We present the Deadlock Attack, a resource exhaustion method that hijacks an LRM's generative control flow.<n>Our method achieves a 100% attack success rate across four advanced LRMs.
  arXiv  Detail & Related papers  (2025-10-12T07:42:57Z)
• Adaptive Attacks on Trusted Monitors Subvert AI Control Protocols [80.68060125494645]
  We study adaptive attacks by an untrusted model that knows the protocol and the monitor model.<n>We instantiate a simple adaptive attack vector by which the attacker embeds publicly known or zero-shot prompt injections in the model outputs.
  arXiv  Detail & Related papers  (2025-10-10T15:12:44Z)
• Adversary-Augmented Simulation for Fairness Evaluation and Defense in Hyperledger Fabric [0.0]
  This paper presents an adversary model and a simulation framework specifically tailored for analyzing attacks on distributed systems composed of multiple protocols.<n>Our model classifies and constrains adversarial actions based on the assumptions of the target protocols.<n>We apply this framework to analyze fairness properties in a Hyperledger Fabric (HF) blockchain network.
  arXiv  Detail & Related papers  (2025-04-17T08:17:27Z)
• CoBRA: A Universal Strategyproof Confirmation Protocol for Quorum-based Proof-of-Stake Blockchains [1.5761916307614148]
  We present a formal analysis of quorum-based State Machine Replication (SMR) protocols in Proof-of-Stake (PoS) systems under a hybrid threat model comprising honest, Byzantine, and rational validators.<n>Our analysis of traditional quorum-based protocols establishes two fundamental impossibility results: (1) in partially synchronous networks, no quorum-based protocol can achieve SMR when rational and Byzantine validators comprise more than $1/3$ of participants, and (2) in synchronous networks, SMR remains impossible when rational and Byzantine validators comprise $2/3$ or more of participants.
  arXiv  Detail & Related papers  (2025-03-21T01:39:29Z)
• Maximal Extractable Value in Decentralized Finance: Taxonomy, Detection, and Mitigation [0.534772724436823]
  Maximal Extractable Value (MEV) can be extracted from financial transactions on the blockchain.<n>MEV causes financial losses and consensus instability, disrupting the security, efficiency, and decentralization goals of the DeFi ecosystem.<n>This survey provides valuable insights for researchers, developers, stakeholders, and policymakers.
  arXiv  Detail & Related papers  (2024-10-22T12:11:41Z)
• Maximal Extractable Value Mitigation Approaches in Ethereum and Layer-2 Chains: A Comprehensive Survey [1.2453219864236247]
  MEV arises when miners or validators manipulate transaction ordering to extract additional value. This not only affects user experience by introducing unpredictability and potential financial losses but also threatens the underlying principles of decentralization and trust. This paper presents a comprehensive survey of MEV mitigation techniques as applied to both protocolss L1 and various L2 solutions.
  arXiv  Detail & Related papers  (2024-07-28T19:51:22Z)
• Avoid Adversarial Adaption in Federated Learning by Multi-Metric Investigations [55.2480439325792]
  Federated Learning (FL) facilitates decentralized machine learning model training, preserving data privacy, lowering communication costs, and boosting model performance through diversified data sources. FL faces vulnerabilities such as poisoning attacks, undermining model integrity with both untargeted performance degradation and targeted backdoor attacks. We define a new notion of strong adaptive adversaries, capable of adapting to multiple objectives simultaneously. MESAS is the first defense robust against strong adaptive adversaries, effective in real-world data scenarios, with an average overhead of just 24.37 seconds.
  arXiv  Detail & Related papers  (2023-06-06T11:44:42Z)
• A theoretical basis for MEV [0.9208007322096532]
  Empirical research has shown that mainstream DeFi protocols are massively targeted by these attacks.<n>We propose a formal theory of MEV, based on a general, abstract model of blockchains and smart contracts.<n>Our theory is the basis for proofs of security against MEV attacks.
  arXiv  Detail & Related papers  (2023-02-04T12:13:29Z)
• Versatile Weight Attack via Flipping Limited Bits [68.45224286690932]
  We study a novel attack paradigm, which modifies model parameters in the deployment stage. Considering the effectiveness and stealthiness goals, we provide a general formulation to perform the bit-flip based weight attack. We present two cases of the general formulation with different malicious purposes, i.e., single sample attack (SSA) and triggered samples attack (TSA)
  arXiv  Detail & Related papers  (2022-07-25T03:24:58Z)
• Is Vertical Logistic Regression Privacy-Preserving? A Comprehensive Privacy Analysis and Beyond [57.10914865054868]
  We consider vertical logistic regression (VLR) trained with mini-batch descent gradient. We provide a comprehensive and rigorous privacy analysis of VLR in a class of open-source Federated Learning frameworks.
  arXiv  Detail & Related papers  (2022-07-19T05:47:30Z)
• Online Adversarial Attacks [57.448101834579624]
  We formalize the online adversarial attack problem, emphasizing two key elements found in real-world use-cases. We first rigorously analyze a deterministic variant of the online threat model. We then propose algoname, a simple yet practical algorithm yielding a provably better competitive ratio for $k=2$ over the current best single threshold algorithm.
  arXiv  Detail & Related papers  (2021-03-02T20:36:04Z)
• A Self-supervised Approach for Adversarial Robustness [105.88250594033053]
  Adversarial examples can cause catastrophic mistakes in Deep Neural Network (DNNs) based vision systems. This paper proposes a self-supervised adversarial training mechanism in the input space. It provides significant robustness against the textbfunseen adversarial attacks.
  arXiv  Detail & Related papers  (2020-06-08T20:42:39Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.