Introduction

act is a high-level specification language for EVM programs. That means act captures the nature of Ethereum smart contracts - which compile to EVM bytecode - as their specification. act is designed in a way that allows for easy refinement of a contract and its specification. This property together with it's built-in formal verification backends makes act a powerful tool for smart contract developers.

The goal of act is to make it as easy as possible for development teams to define a high-level specification, which can either be used

1. to prove an implementation in EVM bytecode conforms to the spec, or
2. to prove its higher-level properties.

A more detailed explanation of act's formal verification backends together with examples can be found in Verification with act sections.

To get started with act, you can follow the installation instructions in the Getting Started and Installation section.

act Verification Pipeline

act provides two main verification backends that work with the same specification:

┌─────────────────────────────────────────────────────────────────┐
│                        act Specification                        │
│                   (High-level .act file)                        │
└─────────────────────────┬───────────────────────────────────────┘
                          │
                          ▼
             ┌────────────────────────────┐
             │   Type-checking and        │
             │   No-aliasing Check        │
             └────────────┬───────────────┘
                          │
         ┌────────────────┴────────────────┐
         │                                 │
         ▼                                 ▼
    ┌────────────────────────┐      ┌──────────────────────────┐
    │    HEVM Backend        │      │     Rocq Backend         │
    │  (Automated Proofs)    │      │   (Manual Proofs)        │
    └────────────┬───────────┘      └──────────┬───────────────┘
                 │                             │
       ┌─────────┴─────────┐                   │
       │                   │                   │
       ▼                   ▼                   ▼
┌─────────────┐    ┌─────────────┐  ┌──────────────────────────┐
│  Solidity   │    │   Vyper     │  │  Transition System       │
│ .sol file   │    │  .vy file   │  │  Export to Rocq          │
└──────┬──────┘    └──────┬──────┘  └───────────┬──────────────┘
       │                  │                     │
       └────────┬─────────┘                     │
                ▼                               ▼
    ┌────────────────────────┐      ┌──────────────────────────┐
    │  Symbolic Execution    │      │ Interactive Theorem      │
    │  of EVM Bytecode       │      │ Proving (Gallina/Ltac)   │
    └────────────┬───────────┘      └──────────┬───────────────┘
                 │                             │
                 ▼                             │
    ┌────────────────────────┐                 │
    │ Equivalence Checking   │                 │
    │ Spec ≡ Implementation  │                 │
    │ (via SMT solvers)      │                 │
    └────────────┬───────────┘                 │
                 │                             │
                 ▼                             ▼
    Bytecode conforms              Higher-level properties
    to specification              proven about the spec

HEVM Backend: Automatically proves that EVM bytecode (compiled from Solidity or Vyper) correctly implements the act specification. It uses symbolic execution to explore all possible execution paths and SMT solvers (CVC5, Z3, or Bitwuzla) to verify equivalence.

Rocq Backend: Exports the specification as a formal transition system to the Rocq proof assistant (formerly Coq), enabling manual proofs of arbitrarily complex properties about the contract's behavior.

Further key capabilities of act:

• The semantics of act is fully formally defined. Type safety and soundness are proven in detail. A full tech report will be available shortly.

• act is language agnostic: Conceptually, act could support conformity of spec and implementation written in all programming languages that compile to EVM bytecode. Currently (in v0.2.0), Solidity and Vyper are supported.

• act exhaustively describes a contract's behavior. To do so, symbolic execution is used. For symbolic execution to be sound unbounded loops cannot be supported.

• act achieves a purely functional interpretation of a contract's specification (in a sound way, for contracts without aliasing). This can be accomplished if the storage of the contract does not contain any aliased reference to another contract. Hence, aliasing of contract names is not allowed in act: this unique ownership property is verified automatically for act specifications using symbolic execution and SMT solving.