# Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny

arXiv: https://arxiv.org/abs/2303.00152 · HTML: https://mlsanity.com/paper/2303.00152/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 1 Mar 2023.

## Built on by (most cited first, 2 of 2)

- [Laurel: Unblocking Automated Verification with Large Language Models](https://mlsanity.com/paper/2405.16792/) (2024)
- [From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification](https://mlsanity.com/paper/2604.22601/) (2026)

## Abstract (arXiv)

The Ethereum protocol implements a replicated state machine. The network participants keep track of the system state by: 1) agreeing on the sequence of transactions to be processed and 2) computing the state transitions that correspond to the sequence of transactions. Ethereum transactions are programs, called smart contracts, and computing a state transition requires executing some code. The Ethereum Virtual Machine (EVM) provides this capability and can execute programs written in EVM bytecode. We present a formal and executable semantics of the EVM written in the verification-friendly language Dafny: it provides (i) a readable, formal and verified specification of the semantics of the EVM; (ii) a framework to formally reason about bytecode.