EthCheck

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

• Verification of individual functions across all available forks;
• Automatic generation of test cases for each detected issue;
• Execution of these tests against eth2spec to confirm results;
• Availability as a pip package for easy installation.

Architecture

The figure bellow 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

List available forks

ethcheck --list-forks

Verify a specific fork

ethcheck --fork <fork-name>

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.