Skip to content

Latest commit

 

History

History
61 lines (46 loc) · 1.79 KB

README.md

File metadata and controls

61 lines (46 loc) · 1.79 KB
Raw

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.

image

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.