Act

Act is a formal specification language for constructing exhaustive, mathematically rigorous descriptions of EVM smart contracts.

Act specifications are written in a high-level, human-readable language that can be proved equivalent to EVM bytecode, currently via the hevm symbolic execution engine.

Specifications can be extracted to a proof assistant (currently Rocq), accurately modeling contract behavior as a state transition system and enabling verification of complex properties and invariants.

The core vision of Act is to provide a provably correct mapping from EVM bytecode to a high-level mathematical model that can be embedded into a variety of analysis and verification tools.

In-depth documentation is available in The Act Book.

Act builds on the previous Act project.

Building

You can build the project with Nix. If you do not have Nix installed, try the Determinate Nix installer.

Build the act executable from the repository root:

nix build

This produces bin/act, which you can run as described in the Act Book.

For a quick overview of available options:

bin/act --help

Developing

Enter a Nix shell with all dependencies installed:

nix develop

Then use cabal from the project root:

cabal build # build the project
cabal repl  # enter a repl

To execute unit tests:

make test      # run all tests
cabal v2-test  # run Haskell tests

To update project dependencies:

nix flake update

Usage

Once you are in the Nix shell, you can use Act backends for equiv and rocq as follows:

cabal run act -- <OPTIONS>

Run the following command to see options and configuration flags:

cabal run act -- --help

Getting Help

If you have questions, open an issue or reach out on our Matrix Channel. The act development team is happy to help you use Act for smart contract verification.