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

## TL;DR

This paper provides a formal, verified, and executable semantics of the Ethereum Virtual Machine (EVM) in Dafny, enabling precise reasoning about smart contract execution and system state transitions.

## Contribution

It introduces a formal and executable Dafny-based semantics of the EVM, facilitating verification and analysis of smart contracts.

## Key findings

- Verified semantics of the EVM in Dafny
- Framework for formal reasoning about bytecode
- Enhanced understanding of EVM state transitions

## Abstract

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.