hevm

hevm is an implementation of the Ethereum virtual machine (EVM) made for symbolic execution, equivalence checking, and unit testing of smart contracts. hevm can symbolically execute smart contracts, run unit tests, and run arbitrary EVM code. It can run on state set up in a Forge std-test testing harness, or fetched on demand from live network using rpc calls.

hevm was originally developed as part of the dapptools project, and was forked to this repo by the formal methods team at the Ethereum Foundation in August 2022.

Documentation & Support

User facing documentation can be found in the hevm book.

We have a public matrix chat room here.

Installation

Static Binaries

Static binaries for x86 linux and macos are available for each release. These binaries expect to be able to find the following programs on PATH:

solc
z3
(optionally) cvc5
(optionally) bitwuzla

nixpkgs

hevm is available in nixpkgs, and can be installed via:

flakes: nix profile install nixpkgs#haskellPackages.hevm
legacy: nix-env -iA haskellPackages.hevm

nix flakes

hevm can be installed directly from the main branch of this repo via the following command:

nix profile install github:ethereum/hevm

Development

We use nix to manage project dependencies. To start hacking on hevm you should first install nix.

Once nix is installed you can run nix-shell (or nix develop if you use flakes) from the repo root to enter a development shell containing all required dev dependencies. If you use direnv, then you can run direnv allow, and the shell will be automatically entered each time you cd in the project repo.

Once in the shell you can use the usual cabal commands to build and test hevm:

$ cabal build          # build the hevm library
$ cabal build exe:hevm # build the cli binary
$ cabal build test     # build the test binary
$ cabal build bench    # build the benchmarks

$ cabal repl lib:hevm  # enter a repl for the library
$ cabal repl exe:hevm  # enter a repl for the cli
$ cabal repl test      # enter a repl for the tests
$ cabal repl bench     # enter a repl for the benchmarks

$ cabal run hevm       # run the cli binary
$ cabal run test       # run the test binary
$ cabal run bench      # run the benchmarks

# run the cli binary with profiling enabled
$ cabal run --enable-profiling hevm -- <CLI SUBCOMMAND> +RTS -s -p -RTS

# run the test binary with profiling enabled
$ cabal run --enable-profiling test -- +RTS -s -p -RTS

# run the benchmarks with profiling enabled
$ cabal run --enable-profiling bench -- +RTS -s -p -RTS

A high level overview of the architecture can be found in architecture.md.