This article presents the arbitrage detection engine powering Argos, our blockchain intelligence platform. The underlying research is currently under peer review.
The Problem: Detecting Arbitrage at Scale
Arbitrage is one of the largest components of MEV (Maximal Extractable Value) on Ethereum. Bots exploit transient price discrepancies across decentralized exchanges within atomic transactions, extracting value from the market before anyone else can react. Understanding and detecting these operations is essential for compliance teams monitoring DeFi activity, researchers studying market microstructure, and protocol designers trying to mitigate MEV's impact on users.
The challenge is that the DeFi ecosystem is vast and constantly evolving. Thousands of protocols, each with their own ABIs and interaction patterns, make it impractical to maintain a hand-curated library of detection rules. Every new DEX, every new lending protocol, every new aggregator would require a new pattern. Existing approaches either rely on protocol-specific signatures that break when protocols upgrade, or use machine learning classifiers that produce labels without explainable transfer chains.
We took a different path.
The Approach: Let the Structure Speak
Instead of asking "does this transaction match a known arbitrage pattern?", we ask a more fundamental question: "does the flow of tokens in this transaction form a cycle?"
Our detection engine operates in three stages. First, we reconstruct the full token transfer hierarchy from the EVM execution trace, preserving the call stack structure. This produces what we call a Cash Flow Tree: an abstract syntax tree where each node represents a contract call and each leaf represents a token transfer.
Then we apply a convergent term rewriting system to this tree. Fifteen rewriting rules progressively simplify the structure: chaining adjacent transfers that share endpoints, merging parallel paths, collapsing redundant intermediaries. The rules are applied bottom-up, from the deepest call frames to the root, until no more rules can fire.
At the fixpoint, arbitrage cycles emerge naturally from the canonical form. A cycle means tokens left an address, flowed through a series of swaps, and returned to the same address in the same token with a positive balance. No protocol-specific knowledge is needed. We use only standard ERC token ABIs and the WETH interface, making the approach portable across any EVM chain.
This also handles complex cases like flash loan arbitrages, where the borrow-repay round-trip is recovered through structural pairing of matching transfers, without inspecting any lending protocol's events.
Results
We evaluated the system on 220,000 consecutive Ethereum mainnet blocks (November 2025 to January 2026). The results:
- 457,841 confirmed arbitrage detections
- 83% overlap with Eigenphi, a production MEV detection platform
- 81% overlap with ArbiNet, a GNN-based classifier
- 64,340 exclusive detections: arbitrages our system found that neither Eigenphi nor ArbiNet flagged
Among our exclusive detections, 63% involve flash loan round-trips discovered purely from the structural pairing of transfers. These are arbitrages that profitability-based detectors miss because they don't reconstruct the full borrow-repay cycle.
The system classifies each detection into confidence tiers (confirmed, probable, attempted, uncertain) based on whether cycles are complete, profitable after gas, and free of unexplained leftover transfers. This gives analysts a clear signal-to-noise control depending on their use case.
Performance-wise, the rewriting algorithm runs in 0.04 ms median per transaction, with the full pipeline (excluding trace retrieval) at 0.19 ms median, making it suitable for real-time block-by-block analysis.
What sets this work apart is that the entire detection logic is formally verified in Rocq (formerly Coq). We proved five properties with zero admitted obligations:
- Preservation: every chain in the final tree corresponds to a valid walk in the original transfer graph
- Termination: the rewriting always reaches a fixpoint, in at most 3n-2 passes for n transfers
- Soundness: if the system says "arbitrage", the canonical form contains a cycle with matching tokens and positive net balance
- Confluence: the deterministic traversal order guarantees a unique canonical form for every transaction
- Decidable equivalence: two transactions implement the same strategy if and only if their canonical forms coincide
The Rocq mechanization comprises 146 lemmas across 4,572 lines of proof. This means the detection verdicts are not just empirically accurate, they are mathematically guaranteed to be consistent and reproducible.
To our knowledge, this is the first formally verified MEV detection system.
This detection engine is integrated into
Argos and runs on every Ethereum block in real time. If you are a compliance team, forensic analyst, or researcher interested in MEV detection, visit
argosint.com or
reach out.