If It Walks Like an Arbitrage: Protocol-Agnostic Detection with Decidable Structural Equivalence

Battle Count: 50

Directly relevant to DeFi algorithmic trading and MEV extraction. The paper provides a protocol-agnostic, formally verified method for detecting arbitrage executions, which is the core activity of MEV bots. The structural equivalence queries enable strategy taxonomy and competitive intelligence. The attempted-arbitrage tier reveals the population of losing bots, informing gas auction dynamics. Cross-chain portability (Arbitrum, BSC) extends applicability. However, the paper focuses on detection/forensics rather than execution strategy optimization, and does not address real-time mempool monitoring or gas-price optimization needed for actual MEV extraction.

High complexity: 16-rule term rewriting system with two stages (leaf manipulation and node manipulation), deterministic kernel, annotation-and-connection loop, validation, profit calculation, and classification cascade. The Rocq formalization is 13,501 lines with 432 lemmas. The production system is an OCaml module within a larger blockchain analysis platform with decode layer, OSINT enrichment, and database dependencies. Requires archive node access for trace retrieval, EVM-compatible chain support, and understanding of ERC-20/721/1155 token standards. The evaluation pipeline involves 25 Python scripts. However, the detection binary itself runs in 0.25ms median per transaction.

Extensive artifact release: (1) Rocq formalization (13,501 lines, 432 lemmas, 13 corollaries, zero admitted obligations) compiles standalone; (2) per-transaction evaluation CSV with verdicts, reasons, cycle counts, and latency for all 220K blocks; (3) EigenPhi and ArbiNet label sets; (4) 25 Python evaluation scripts orchestrated by run_all.py; (5) Docker image with 5 compiled binaries for offline and online detection; (6) pre-exported raw traces for 2,000 blocks; (7) long-form proof companion. The detection algorithm is an OCaml module within a larger platform and cannot be cleanly factored out, but all claims are verifiable through three independent routes: Rocq proofs, compiled binaries, and per-transaction output dataset.