hevm

hevm is an implementation of the Ethereum virtual machine (EVM) made for symbolic execution, equivalence checking, and (symbolic) unit testing of smart contracts. hevm can symbolically execute smart contracts, perform symbolic equivalence testing, and run arbitrary EVM code. In particular, it can run Forge test suites in a symbolic way, thereby being much more thorough than fuzz testing.

Documentation & Support

User facing documentation can be found in the hevm book. We have a public matrix chat room here.

Installing via 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:

• z3
• (optionally) cvc5
• (optionally) bitwuzla

Installing via nix

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

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

hevm flake 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 develop from the repo root to enter a development shell containing all required dev dependencies.

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

$ cabal run hevm -- test --root myproject # run the cli
$ cabal run test                          # run the tests
$ cabal repl test                         # enter the repl for the test.sh
$ cabal run ethereum-tests                # run the ethereum standard tests

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

History

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.