A Python tool for verifying Ethereum Consensus Specification using ESBMC
Project description
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;
Architecture
The figure bellow illustrates the EthCheck architecture.
Installation
EthCheck is currently supported on Linux.
sudo apt update
sudo apt install -y python3-venv python3-pip git-lfs
pip install eth2spec
pip install ethcheck
Usage
Important: Ensure the virtual environment is active by running the command below:
python3 -m venv ethcheck_env
source ethcheck_env/bin/activate
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>
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
Filter files by name, interpreter, ABI, and platform.
If you're not sure about the file name format, learn more about wheel file names.
Copy a direct link to the current filters
File details
Details for the file ethcheck-0.1.4.tar.gz.
File metadata
- Download URL: ethcheck-0.1.4.tar.gz
- Upload date:
- Size: 70.0 MB
- Tags: Source
- Uploaded using Trusted Publishing? No
- Uploaded via: twine/6.0.1 CPython/3.10.12
File hashes
| Algorithm | Hash digest | |
|---|---|---|
| SHA256 |
dc7462f94d6f44fe94cec8876c74488d38074e12666df3786e26bd68fb1693b1
|
|
| MD5 |
0c0728c7492b19145855589cb9d8a9e6
|
|
| BLAKE2b-256 |
f5fc6228c86d57d802cf15a3ba7bb24f516d98d21599388083076bc782d6421f
|
File details
Details for the file ethcheck-0.1.4-py3-none-any.whl.
File metadata
- Download URL: ethcheck-0.1.4-py3-none-any.whl
- Upload date:
- Size: 70.4 MB
- Tags: Python 3
- Uploaded using Trusted Publishing? No
- Uploaded via: twine/6.0.1 CPython/3.10.12
File hashes
| Algorithm | Hash digest | |
|---|---|---|
| SHA256 |
b3714a6c9134c5efc616c40d656a7a822531d6a454584f365a9e284b93bd2990
|
|
| MD5 |
780293b89d7328c1e471f894f82e5e2b
|
|
| BLAKE2b-256 |
5656832e7a1c5c9bbbbf902bda4e5200ac16669969e478fba9e4c2035c601463
|
