ethcheck 0.1.2

A Python tool for verifying Ethereum Consensus Specification using ESBMC

EthCheck

EthCheck is a command-line tool for testing and verifying the Ethereum Consensus Specification using the ESBMC model checker. EthCheck runner includes:

• Automatically generating test cases for each detected issue;
• Executing these tests against eth2spec for confirmation;
• A comprehensive pip package with detailed documentation.

Architecture

The figure illustrates the EthCheck architecture.

Installation

EthCheck is currently supported on Linux.

1. Install dependencies

sudo apt update
sudo apt install -y python3-venv python3-pip git-lfs
./scripts/install_deps.sh

2. Activate the Virtual Environment

Activate the Python virtual environment created during the step above.

source ethcheck_env/bin/activate

3. Install EthCheck

pip install .

Usage

Important: Ensure the virtual environment is active by running the command source ethcheck_env/bin/activate before using EthCheck. The terminal should display <ethcheck_env> if the environment is active.

Verify a specific file

ethcheck --file ethcheck/spec.py

Verify the Deneb fork specification

ethcheck --deneb

ESBMC version

Git hash: 1dffbe270c
Git tag: consensus-v1
MD5: 618f1fd89c399102865f9e366d164cb6

Acknowledgment

We thank the Ethereum Foundation for supporting our research team on this project.