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

to prove an implementation in EVM bytecode conforms to the spec, or
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.

Getting Started

act uses Nix for dependency management and building. If you don't have Nix installed yet, you can use the Determinate Nix installer.

Installation

To build from source

Clone the repository:

git clone https://github.com/argotorg/act.git
cd act

Build the project:

nix build

Once you have built, for development, enter a Nix development shell to get all dependencies:

nix develop

Test your installation by running the commands in basic usage section.

Note: You can also use Cabal as normal from the root directory.

Basic Usage

Once you are in the Nix shell, test your installation by running the HelloWorld contract specification:

The hevm backend:

cabal run act --equiv --spec tests/helloworld/helloworld.act --sol tests/helloworld/helloworld.sol

(the output should conclude with No discrepancies found.)

The Rocq backend:

cabal run act -- rocq --file tests/helloworld/helloworld.act

(the output should conclude with Qed. End HelloWorld.)

Alternatively, if you've run make first, you can run the executable directly:

act <OPTIONS>

For advanced options, consult the hevm backend documentation and Rocq backend documentation, or list the options by calling

cabal run act -- --help

A First Look: ERC20 as Running Example

In this section, we present a first look at an act specification by walking through a simple example: an ERC20 token contract. The goal is to illustrate the overall structure of an act specification and how it relates to the underlying smart contract code.

From EVM Smart Contract to act

We start from an ERC20-style contract written in Solidity respectively Vyper:

(code snippets from erc20.sol and erc20.vy; storage and function signatures only)

contract Token {
    uint256 public totalSupply;
    mapping(address => uint256) public balanceOf;
    mapping(address => mapping(address => uint256)) public allowance;

    constructor(uint256 _totalSupply);
    function transfer(address to, uint256 value) public;
    function transferFrom(address from, address to, uint256 value) public;
    ...
}

  totalSupply: public(uint256)
  balanceOf: public(HashMap[address, uint256])
  allowance: public(HashMap[address, HashMap[address, uint256]])

  @deploy
  def __init__(_totalSupply: uint256)
  @external
  def transfer(value_: uint256, to: address) -> bool
  @external
  def transferFrom(from_: address, to: address, value_: uint256) -> bool
  ...

An ERC20 token is a standard type of smart contract on Ethereum that represents a fungible asset, meaning all units of the token are interchangeable (like dollars or euros, rather than NFTs). The contract maintains a ledger that records how many tokens each address owns and provides a small, fixed interface for moving tokens between addresses. The core piece of state is the balanceOf mapping, which assigns to every address its current token balance; the sum of all balances represents the total supply of the token.

A token holder can move tokens directly using transfer, which subtracts a specified amount from the caller’s balance and adds it to the recipient’s balance, provided the caller has sufficient funds.

In addition to direct transfers, ERC20 supports delegated transfers through the allowance mechanism: an address can authorize another address (a “spender”) to transfer up to a certain number of tokens on its behalf. These authorizations are recorded in the allowance mapping, which maps an owner and a spender to an approved amount. The transferFrom function uses this mechanism to move tokens from one address to another while decreasing both the owner’s balance and the remaining allowance of the spender. Together, balanceOf, allowance, transfer, and transferFrom define a simple but powerful accounting model that enables tokens to be held, transferred, and used by third-party contracts without giving them unrestricted control over a user’s funds.

An act specification describes the externally observable behavior of this contract. At a high level, an act specification consists of one or more contracts, where each contract has:

a constructor, describing what storage is created and how it is initialized
a set of transitions, one for each callable function
explicit preconditions under which function calls succeed
explicit storage updates describing the resulting state

The Shape of an act Contract

The translation of the code above into an act specification has the following top-level structure:

(snippet from erc20.act, high-level structure only)

contract Token:

constructor(uint256 _totalSupply)
creates
  uint256 totalSupply := _totalSupply
  mapping(address => uint) balanceOf :=  [CALLER => _totalSupply]
  mapping(address => mapping(address => uint)) allowance := []

transition transfer(uint256 value, address to)
iff  ...
case CALLER != to:
  updates
    ...
case CALLER == to:
  updates
    ...

transition transferFrom(address from, address to, uint256 value)
iff ...

Even without understanding the details, several aspects are already visible:

For each contract the act spec starts with contract <NAME>:.
Afterwards the constructor contructor(<input_vars>) follows.
Lastly all smart contract functions are listed as transitions transition <fct_name>(<input_vars>)
Within the constructor and the transitions:
- The list of preconditions (the iff block) comes first and lists the necessary and sufficient conditions on when this operation succeeds. If the iff block is not satisfied, the corresponding function in Solidity/Vyper would revert. If there are no preconditions, the iff block is omitted.
- In the constructor the creates block is next. It lists all the storage a contract has and initializes it. As expected, it mirrors the Solidity/Vyper code closely. The creates block is the last block of the constructor.
- Similar to creates for constructors works the updates block for transitions. It updates all the changes to the storage. Thereby, summarizing the effects a transition has on the storage.
- If there are any branches in the underlying Solidity/Vyper code, then act distinguishes what happens to the storage relative to a case. In the ERC20 example, that happens in line 11 and line 14: depending on whether the function caller CALLER is the same address as the one where the money is supposed to be transfered to, to, the storage is updated differently.
act is aware of some Ethereum environment variables such as the caller of a function CALLER or the amount that was "paid" to a contract upon a function call CALLVALUE.

In the next sections, we will build up the meaning of these pieces by incrementally refining the ERC20 specification.

Jump to Running the ERC20 Example if you want to try out running the ERC20 example with the equivalence checking backend. To explore the Rocq extraction of the ERC20 example, go to act Export.

Syntax of the Act language

A specification of one or more contracts written in act consists of a contract block for each contract, which in turn contains a single constructor and a set of transitions.

The constructor specification defines the structure of the contract state, the initial value for the state, and the conditions under which the contract can be created.

Each transition specification determines how a contract function updates the state, its return value, and the conditions that must be satisfied in order for it to be applied.

Alternatively, they can be thought of an initial state and a set of state transitions, determining an inductively defined state transition system.

The specifications can be exported to different backends in order to prove that the claims that are being made hold with respect to an implementation.

Basic Elements

Types:

in act there are three kinds of types: simple ABI types (e.g., uint256, address, bool), mapping types (e.g., mapping(address => uint256)), and contract types (e.g., Token). These types are explained in detail in Types.
Expressions:

expressions in act are used to initialize storage variables, describe state updates and to express conditions. They can be simple variables, constants, arithmetic expressions, or more complex expressions such as mapping lookups. Expressions are explained in detail in Expressions.
Storage:

The storage is the key element of a contract's state. It is declared and initialized in the creates block of the constructor. Storage updates are specified in the updates block of transitions. Storage is explained in detail in Storage.
Constructor:

The constructor defines the initial state of the contract and the conditions for its creation. Constructors are explained in detail in Constructors and Initial State.
Transitions:

Transitions define how the contract state changes in response to function calls. They specify preconditions for the function calls and the resulting state updates. Transitions are explained in detail in Transitions and Storage Updates.

A tutorial on how to write your own act specification can be found in How to Write Your Own Spec.

Storage, Typing and Expressions

In act, each contract explicitly declares its storage in the constructor and initializes it. The types of storage variables are explicit and checked. This section explains the storage model of act, the types allowed in storage, and the different kinds of expressions used throughout act specifications.

Storage

In act, each contract explicitly declares its storage in the constructor and initializes it as defined in the source code. If the source code does not initialize a storage field, act uses defaults. For ERC20, the storage consists of two mappings and an integer:

(snippet from erc20.sol, updates block)

    uint256 public totalSupply;
    mapping (address => uint256) public balanceOf;
    mapping (address => mapping (address => uint256)) public allowance;

The respective act declaration including initialization is:

(corresponding snippet from erc20.act, constructor block)

creates
  uint256 totalSupply := _totalSupply
  mapping(address => uint256) balanceOf := [CALLER => _totalSupply]
  mapping(address => mapping(address => uint256)) allowance := []

For each storage variable its initialization has the shape <type> <name> := <storage_expression>. The act storage corresponds directly to the EVM state variables, but with two important differences:

All storage is immutable by default. Storage can only change through explicit updates inside transitions.
Types are explicit and checked. Which types storage can have is detailed next.

Types

act has a rich type system to describe both storage and function parameters/return values. There are three main categories of types in act:

Storage types,
Mapping types, and
ABI types.

Storage Types (a.k.a. Slot Types)

Storage in act can have the following types:

base types e.g. line 2 in the snippet above: uint256 totalSupply
- unsigned integers of various sizes: uint8, uint16, uint32, uint64, uint128, uint256, where uint is a shorthand for uint256.
- signed integers of various sizes: int8, int16, int32, int64, int128, int256, also int is a shorthand for int256.
- booleans: bool
- addresses:address
mapping types
- mappings from one base type to another, e.g. from address to uint256 in line 3 mapping(address => uint256) balanceOf
- nested mappings: from a base type to another mapping, e.g. from address to mapping(address => uint256) in line 4 mapping(address => mapping(address => uint256)) allowance
contract types referencing the storage of other contracts (details in Alasing and Unique Ownership)
- A contract type ContractType can be used as a storage type to denote a reference to the storage of another contract of type ContractType.
- This allows act specifications to model interactions between multiple contracts.
- Artificial example: Another contract OtherContract uses in its storage a reference to an ERC20 Token contract: In OtherContract's storage we would have a field of type Token, which can be initialized with (an address of) a specific deployed ERC20 contract instance. An example of this is shown in Constructor Preconditions.

Mapping Types and Defaults

A mapping in act behaves like a total function with a default value. For example, the type:

mapping(address => uint256) balanceOf

denotes a function from addresses to integers, where all keys not explicitly written map to the default value of uint256, which is 0. If it is initialized as in line 3 of the constructor snippet above:

mapping(address => uint256) balanceOf := [CALLER => _totalSupply]

then the mapping behaves like this:

balanceOf[CALLER] evaluates to _totalSupply
For any other address A, balanceOf[A] evaluates to 0

The defaults for the different mapping types are:

uint* and int*: 0
bool: false
address: 0x00000000000000000000000000000000 which is the zero address.
mapping(<base type> => <mapping_type>): a mapping where all keys map to the default value of <mapping_type>. Note: mapping types here include base types but not contract types.

This matches Solidity’s behavior but is made explicit in act, which is essential for reasoning about invariants.

ABI Types

The following types are used for function parameters and return values, mirroring the Ethereum ABI specification:

All base types (uint*, int*, bool, address) are allowed here.
Additionally, there is another ABI type: specially annotated address types. These are addresses which point to contracts. Intuitively, an annotated address type address<ContractType> can be thought of as a regular address, for which we know that it points to the storage of a contract of type ContractType.

Consider the following act snippet that declares a transition foo which takes an address of an ERC20 contract as parameter:
```
transition foo(address<Token> token_addr)
iff true
updates
    erc_token := address(token_addr)
```
The parameter token_addr has type address<Token>, which indicates that the address points to a deployed contract of type Token (e.g. in our example an ERC20 token).

This special type exists to allow act to reason about calls to this contract now called erc_token, which lives at address token_addr inside the transition body. Ensuring that the spec which includes this annotated address types is equivalent to the implementation which only uses regular addresses is still possible and discussed in Input Space Equivalence.

Note: Not all types in act are allowed everywhere. There is a distinction between ABI types and Storage types:

ABI types include base types and annotated address types. They are used for function parameters and return values.
Storage types include base types, mapping types, and contract types. They are used for storage.

That means in function parameters and return values, mapping types and contract types are not allowed. Whereas in storage, annotated address types are not allowed.

Expressions

Expressions appear throughout constructor and transition declarations: in preconditions (iff blocks), case conditions, storage initialization and updates (in creates and storage blocks) as well as in return statements of transitions. act distinguishes between three kinds of expressions, each serving different purposes:

Overview of Expressions

Storage Expressions (Slot Expressions): Expressions that manipulate storage data. Used in the creates and updates block to initialize or update storage variables. Examples in the ERC20 constructor: _totalSupply, [CALLER => _totalSupply], [], new Token(100).
References: Variable references that denote storage locations or calldata. Used in preconditions, case conditions, and to reference existing values (as it is done in storage updates). Examples in the ERC20: totalSupply, balanceOf[CALLER], CALLVALUE, allowance.
Base Expressions: Composite expressions built from operators and literals. Include arithmetic, boolean logic, comparisons, and conditionals. Used in all contexts (preconditions, cases, storage, returns). Examples: x + y, true, x == 5, if z > 0 then a else b.

Storage Expressions

Storage expressions describe the initial values assigned to storage variables in the creates block and the values they are updated to in the updates block. The syntax for initializing in the creates block is <type> <name> := <storage_expression>. For updating in the updates block, it is <name> := <storage_expression>. Storage expressions can be:

Base Expressions: literals, composed expressions or certain Variable References: 100, x + y, if condition then a else b. See Base Expressions below for details.
Mappings: Expressions that have mapping typ. The syntax of defining new mappings is the following:
- [<key1> => <value1>, <key2> => <value2>, ...] (a mapping with multiple entries)
- [] (an empty mapping where all keys map to the default value) Every key not explicitly mentioned maps to the default value of the mapping's value type. Further, exists the syntax for adapting mappings (used in updates blocks of transitions):
- my_map[my_key => my_value] (defines a mapping, where my_key maps to my_value and every other key has value my_map[key])
- similarly, multple entries can be changed at once: my_map[key1 => value1, key2 => value2,...]
Contract creation: An instance of another contract (an ERC20 Token for example) can be part of a contract's storage. The corresponding storage expression is new Token(100). It creates a new ERC20 contract instance with total supply 100. The keyword new indicates that a new contract instance is created. The parentheses contain the arguments passed to the constructor of the other contract.

Depending on whether this other contract's constructor is payable or not (see Payable and Non-Payable Constructors), the storage expression requires to specify the amount of Ether to send.
- For a non-payable constructor, no Ether is sent and therefore nothing extra has to be specified. Hence new Token(100) suffices.
- For a payable constructor, the amount of Ether to send must be specified. Assume there is a payable constructor TokenPayable, then the storage expression would be e.g. new TokenPayable{value:10}(100) to create a new instance of TokenPayable with initial supply 100 and send 10 wei during construction. The keyword to specify the amount of Ether (wei) to send is value.
references to existing contracts: erc_token (a reference to a deployed contract instance)
Addresses of existing contracts: token_addr (an address of a deployed contract instance)

Example from the ERC20 contract:

In the ERC20 constructor, the storage is initialized as:

(snippet from erc20.act, constructor block)

creates
  uint256 totalSupply := _totalSupply
  mapping(address => uint) balanceOf := [CALLER => _totalSupply]
  mapping(address => mapping(address => uint)) allowance := []

Here we see:

A base expression: _totalSupply
A new mapping: [CALLER => _totalSupply] which assigns the entire supply to the caller and defaults to 0 for all other addresses
An new empty mapping: [] where all addresses map to the default map from address to uint, which is 0.

In a transfer transition of the ERC20 contract the storage is updated as:

(snippet from erc20.act, transfer transition)

  updates

    balanceOf := balanceOf[ CALLER => balanceOf[CALLER] - _value,
                            to     => balanceOf[to] + _value]

Here we see a base expression, variable references (CALLER and to), a parameter _value, subtraction and addition.

Variable References

References denote storage locations or parameters and are used as building blocks in:

Preconditions (iff blocks): e.g., t0 != t1
Case conditions: e.g., case CALLVALUE > 0:
Storage updates in transitions: (covered in the Transitions section)

Basic references include:

Storage Variable names: totalSupply, balanceOf, allowance
Parameter names: _totalSupply, to, value
Environment variables: CALLER, CALLVALUE, ORIGIN, THIS, BALANCE Environment variables represent special values provided by the EVM:
- address CALLER: the address of the entity (externally owned account or contract) that invoked the current function.
- uint256 CALLVALUE: the amount of Ether (in wei) sent with the current call.
- addresss ORIGIN: the address of the original external account that started the transaction.
- address THIS: the address of the current contract.
- uint256 BALANCE: the balance of the current contract in Ether.
Mapping references: balanceOf[CALLER]
Field references: t0.balanceOf (if t0 is a contract reference)

Example from ERC20 transfer transition:

The preconditions in the transfer transition use references:

(snippet from transfer transition in erc20.act)

iff
  inRange(uint256, balanceOf[CALLER] - _value)
  CALLER != to ==> inRange(uint256, balanceOf[to] + _value)

The precondition uses the mapping references balanceOf[CALLER] and balanceOf[to], the parameter names _value, and to, and the environment variable CALLER. The precondition ensures that the transfer does not cause an underflow or overflow in the balances.

Base Expressions

Base expressions are composite expressions built using operators, literals and variable references of certain types. They are used wherever an expression is needed: in preconditions, case conditions, during storage initialization and updates, and in return statements.

Arithmetic operators (for integer types):

Addition: x + y
Subtraction: x - y
Multiplication: x * y
Division: x / y
Modulo: x % y
Exponentiation: x ^ y

Boolean operators:

Conjunction: condition1 and condition2
Disjunction: condition1 or condition2
Negation: not condition
Implication: condition1 ==> condition2

Comparison operators (work on all types):

Equality: x == y
Inequality: x != y
Less than: x < y
Less than or equal: x <= y
Greater than: x > y
Greater than or equal: x >= y

Other operators:

Conditionals: if condition then expr1 else expr2
Range checks: inRange(uint256, x) (checks if x fits in the given type) See Preconditions and Arithmetic Safety for details.

Literals and Other Expressions:

Literals: 5, true, false
Variable references of ABI types (integers, booleans, addresses, and annotated address type address<ContractType>), e.g. totalSupply, CALLER, value

Whenever an expression expr of annotated address type is seen as a regular address (e.g. when used in arithmetic), it has to be cast to a regular address type using address(expr).
Address conversion of deployed contracts: addr(t0) (if t0 is a contract reference)

Examples of Base Expressions:

Consider the following case blocks from the transferFrom transition of the ERC20 contract:

(snippet from transferFrom transition in erc20.act)

transition transferFrom(address src, address dst, uint amount) : uint256

iff
    ...

case src != dst and CALLER == src:
    ...

case src != dst and CALLER != src and allowance[src][CALLER] == 2^256 - 1:
    ...

case src != dst and CALLER != src and allowance[src][CALLER] < 2^256 - 1:
    ...

case src == dst and CALLER != src and allowance[src][CALLER] < 2^256 - 1:
    ...

case src == dst and (CALLER == src or allowance[src][CALLER] == 2^256 - 1):
    ...

Here, various base expressions with exponentiations, comparisons and boolean operators are used. Moreover, variable references like allowance[src][CALLER], src, dst, and CALLER are used to build these expressions.

Contructors and Initial State

Constructors in act specify the initial state of contract storage and the conditions under which a contract can be successfully deployed.

Constructor Structure

The general shape of a constructor in act is:

┌──────────────────────────────────────────────────────────────┐
│         constructor (<parameters>) ?payable                  │
└─────────────────────────┬────────────────────────────────────┘
                          │
                          ▼
                  ┌───────────────--┐
                  │ iff <condition> │
                  └────────┬────────┘
                           │
              ┌────────────┴────────────┐
              │                         │
              ▼                         ▼
      No branching                Branching (cases)
              │                         │
              ▼                         ▼
    ┌──────────────────────┐  ┌──────────────────────────┐
    │ creates              │  │ case <condition>:        │
    │   <storage_init>     │  │   creates <storage_init> │
    └──────────────────────┘  └──────────┬───────────────┘
                                         │
                                         ▼
                                        ...
                                        
                                         │
                                         ▼
                              ┌──────────────────────────┐
                              │ case <condition>:        │
                              │   creates <storage_init> │
                              └──────────────────────────┘

Components:

Constructor Head: constructor (<parameters>) ?payable
- Parameter list with types and names separated by commas.
- Optional payable keyword for accepting Ether during deployment.
Precondition Block: iff <condition>
- Specifies the necessary and sufficient condition for successful constructor execution.
- Can be omitted if there are no preconditions.
Cases Block (optional):
- If present, there are multiple case <condition>: creates ... branches whose conditions are mutually exclusive and exhaustive.
- The absence of a cases block is equivalent to a single implicit case true: block.
- The cases blocks allow the user to specify different storage initializations (creates <storage_init>) depending on which condition the constructor parameters meet. It mirrors the if then else structure in EVM smart contracts.
Creates Block: creates <storage_init>
- Initializes storage variables with initial values
- Every storage variable declared in the contract must be initialized in every creates block.
- The assignments are separated by newlines and have the shape: <type> <name> := <expression>

Payable and Non-Payable Constructors

In EVM smart contracts, constructors can be declared payable or non-payable (the default). A payable constructor allows sending Ether along with contract creation, while a non-payable constructor rejects any Ether sent. In act, the situation is similar: there is a keyword payable in the constructor declaration to mark payable constructors. For every constructor that is not marked payable, act automatically internally adds a precondition that no Ether is sent during construction.

Similarly, if a constructor is marked payable, the user has to declare and initialize the contract's balance in Ether using the special variable uint256 BALANCE. For non-payable constructors, BALANCE is set to 0 implicitly and the user does not have to declare or initialize it.

In the ERC20 example, the constructor is non-payable. Thus, it does not include the payable keyword nor the BALANCE variable:

(constructor from erc20.act)

constructor(uint256 _totalSupply)

creates

  uint256 totalSupply := _totalSupply
  mapping(address => uint) balanceOf :=  [CALLER => _totalSupply]
  mapping(address => mapping(address => uint)) allowance := []

An artificial example of a payable constructor would be:

constructor () payable

case CALLVALUE > 0 :
creates
    bool myFlag := true
    uint256 BALANCE := CALLVALUE

case CALLVALUE == 0 :
creates
    bool myFlag := false
    uint256 BALANCE := 0

act interally tracks the balance (in Ether) of each contract, including during construction. This is required to correctly reason about payable constructors. Although this BALANCE variable is not part of the contract storage per se, it can be affected by the behavior of the constructor or the transitions and is therefore initialized and updated the same way as storage slots.

Further, the user can write conditions on the callvalue sent during construction using the special variable CALLVALUE. See e.g. the payable constructor example above. Additionally to BALANCE, there are 4 such special variables (called environment variables) related to the call environment that the user can access as explained in Variable References.

Constructor Preconditions

Consider the following constructor from an automated market maker (AMM) contract:

(constructor from amm.act)

constructor(address<Token> t0, address<Token> t1)

iff
    address(t0) != address(t1)

creates

    Token token0 := t0
    Token token1 := t1

It is a non-payable constructor that takes two parameters, t0 and t1, which are addresses of ERC20 token contracts. The data type address<Token>, is called annotated address type and indicates that these addresses point to deployed contracts of type Token (i.e., ERC20 tokens) and is explained in ABI Types. Whenever an expression expr of annotated address type is seen as a regular address (e.g. when used in comparisons), it has to be cast to a regular address type using address(expr).

The iff clause specifies the necessary and sufficient condition under which the constructor succeeds. If this condition does not hold, the constructor reverts. In this example, the precondition address(t0) != address(t1) ensures that the two token addresses are distinct. If a user attempts to deploy the AMM contract with identical token addresses, the constructor will revert, preventing the creation of an invalid AMM instance.

The precondition block extends the require/assert statements commonly used in Solidity/Vyper constructors by explicitly listing requirements that are implicit in the code. In the above case the iff block is the same as the require/assert statement in Solidity/Vyper:

(constructor from amm.sol)

 constructor(address t0, address t1) {
        require (t0 != t1);
        token0 = Token(t0);
        token1 = Token(t1);
    }

(constructor from amm.vy)

@deploy
def __init__(t0: address, t1: address):
  assert (t0 != t1)
  self.token0 = Token(t0)
  self.token1 = Token(t1)

As mentioned before, the iff block can be skipped if the condition is trivial (i.e. iff true), as shown in the ERC20 example.

`inRange` in Preconditions

Whenever arithmetic operations are involved in the storage initialization, it is necessary to ensure that these operations do not overflow or underflow. This is done using the inRange expression (Base Expressions), which checks whether a value fits within a specified type. In solidity these range checks are implicit, but in act they must be made explicit in the precondition block.

For example, consider a constructor that initializes a balance by subtracting a value from an initial amount. To ensure that this subtraction does not underflow, the precondition would include an inRange check:

constructor(uint256 initialAmount, uint256 deduction)
iff
    inRange(uint256, initialAmount - deduction)
    
creates
    uint256 balance := initialAmount - deduction

The same principle applies to transitions and storage updates. How the arithmetic safety is enforced in act is explained in more detail in Arithmetic Safety.

Initializing Storage

The storage is created in the creates block, where each storage variable is initialized as <type> <name> := <expression>. The allowed types and expressions are explained in Storage, Typing and Expressions.

We revisit the storage initialization of the ERC20 constructor:

(snippet from erc20.act constructor)

creates 
  uint256 totalSupply := _totalSupply
  mapping(address => uint) balanceOf :=  [CALLER => _totalSupply]
  mapping(address => mapping(address => uint)) allowance := []

All storage variables declared in the contract must be initialized in every creates block of the constructor. If the constructor is payable, the special variable BALANCE must also be declared and initialized. Here, the constructor initializes three storage variables and specifies their types:

totalSupply of type uint256, initialized to the constructor parameter _totalSupply.
balanceOf, which maps addresses to integers and therefore has type mapping(address => uint). It is initialized such that the deployer (CALLER) receives the entire supply. Every other address is not mentioned and thus defaults to 0.
allowance maps pairs of addresses to integers and therefore has (the curried) type mapping(address => mapping(address => uint)). It initialized to an empty mapping (all values default to 0).

This should be read as: “In the initial state, the total supply of tokens is totalSupply, balanceOf(CALLER) = totalSupply, and all other addresses have 0. Further allowance(addr0, addr1) = 0 for all pairs of addresses.”

Note that the act spec describes only the end-result of the constructor execution, not the intermediate steps.

Constructors Cannot Modify Existing Contracts

An important design choice in act is that constructors:

may create new contracts. E.g. Token new_token := new Token(100) could be used to create a new ERC20 contract with an initial supply of 100 and assign it to the storage variable new_token.
must initialize their own storage (e.g.uint256 totalSupply := _totalSupply in the ERC20 example).
may not mutate existing contract storage. I.e. only assigning existing contracts to storage variablesis allowed. E.g. Token token0 := t0 as in the AMM constructor. This restriction ensures that contract creation is local and predictable, and it plays a key role later when we reason about ownership and functional semantics.

For ERC20, this restriction is invisible — but it becomes crucial in more complex examples.

Transitions and Storage Updates

Transitions in act specify the behavior of contract functions and the conditions under which storage is updated or values are returned.

Transition Structure

The general shape of a transition that returns a value in act is:

┌──────────────────────────────────────────────────────────────┐
│  transition <name> (<parameters>) ?payable : <return_type>   │
└─────────────────────────┬────────────────────────────────────┘
                          │
                          ▼
                  ┌───────────────--┐
                  │ iff <condition> │
                  └────────┬────────┘
                           │
              ┌────────────┴────────────┐
              │                         │
              |                         |
      No branching                Branching (cases)
              │                         │
              ▼                         ▼
    ┌──────────────────┐      ┌──────────────────────┐
    │ updates <storage>│      │ case <condition>:    │
    └────────┬─────────┘      │   updates <storage>  │
             │                └──────────┬───────────┘
             ▼                           │
    ┌──────────────────┐                 ▼
    │ returns <value>  │      ┌──────────────────────┐
    └──────────────────┘      │ returns <value>      │
                              └──────────┬───────────┘
                                         │
                                         ▼
                                        ...

                                         │
                                         ▼
                              ┌──────────────────────┐
                              │ case <condition>:    │
                              │   updates <storage>  │
                              └──────────┬───────────┘
                                         │
                                         ▼
                              ┌──────────────────────┐
                              │ returns <value>      │
                              └──────────────────────┘

The general shape of a transition that does not return a value in act is:

┌──────────────────────────────────────────────────────────────┐
│     transition <name> (<parameters>) ?payable                │
└─────────────────────────┬────────────────────────────────────┘
                          │
                          ▼
                  ┌───────────────--┐
                  │ iff <condition> │
                  └────────┬────────┘
                           │
              ┌────────────┴────────────┐
              │                         │
              |                         |
      No branching                Branching (cases)
              │                         │
              ▼                         ▼
    ┌──────────────────┐      ┌──────────────────────┐
    │ updates <storage>│      │ case <condition>:    │
    └──────────────────┘      │   updates <storage>  │
                              └──────────┬───────────┘
                                         │
                                         ▼
                                        ...

                                         │
                                         ▼
                              ┌──────────────────────┐
                              │ case <condition>:    │
                              │   updates <storage>  │
                              └──────────────────────┘

Components:

Transition Head: transition <name> (<parameters>) ?payable ?(: <return_type>)
- Function name <name> and parameter list <parameters> with types and names.
- Optional payable keyword to mark transitions that accept Ether.
- Optional return type specification (e.g., : uint256). If a return type is specified, the transition must include a returns <value> statement after each updates block.
Precondition Block: iff <condition>
- Specifies the necessary and sufficient condition for successful execution.
- Can be omitted if there are no preconditions.
- If the precondition fails, the transition reverts and makes no state changes.
Cases Block (optional):
- If present two or more case <condition>: updates <storage> branches.
- Conditions must be mutually exclusive and exhaustive.
- Each case describes storage updates (state transitions) for a particular execution path.
- The absence of a cases block is equivalent to a single implicit case true: block.
Updates Block: updates <storage>
- Updates storage variables based on the current execution path (i.e. the case).
- Storage fields that are not mentioned remain unchanged.
- The updates are separated by newlines and have the shape: <variable> := <expression>
- Updates are simultaneous: all right-hand sides are evaluated in the initial state.
- Can be skipped if no storage updates are performed.
Returns Block: returns <value>
- present after each updates block if and only if the transition has a return type.
- Specifies the return value of the function.

Transition Signatures

Each externally callable function of the EVM smart contract source is specified as a transition. Similarly to constructors, transitions can be marked payable or non-payable (the default). Similarly to the constructors, for transitions that are not marked payable, act automatically internally adds a precondition that CALLVALUE == 0.

For example the transfer transition of the ERC20 contract is non-payable and specified as:

(signature from erc20.act)

transition transfer(uint256 _value, address to) : bool
     ...

This declares the function parameters and the return type bool.

The other transitions of the ERC20 contract are:

(signatures from erc20.act)

transition transferFrom(address src, address dst, uint amount) : bool
       ...
transition approve(address spender, uint256 amount) : bool
   ...
transition burn(uint256 amount) : bool
   ...
transition burnFrom(address src, uint256 amount) : bool
   ...
transition mint(address dst, uint256 amount) : bool
   ...
transition totalSupply() : uint256
   ...
transition balanceOf(address owner) : uint256
   ...
transition allowance(address owner, address spender) : uint256
   ...

The transitions correspond to the externally callable functions of the ERC20 contract:

(signatures from erc20.sol)

function transfer(uint256 value, address to) public returns (bool) {
   ...
}
function transferFrom(address src, address dst, uint amount) public returns (bool) {
   ...
}
function approve(address spender, uint256 amount) public returns (bool) {
   ...
}
function burn(uint256 amount) public returns (bool) {
   ...
}
function burnFrom(address src, uint256 amount) public returns (bool) {
   ...
}
function mint(address dst, uint256 amount) public returns (bool) {
   ...
}

The transitions totalSupply, balanceOf and allowance correspond to the public getter functions automatically generated by Solidity for the respective public storage variables.

Transition Preconditions

Similar to constructors, see Constructor Preconditions for details.

Case Splits and Control Flow

act uses case blocks to describe control flow explicitly. In the ERC20 transfer transition, we distinguish two cases based on whether the sender (CALLER) is transferring tokens to themselves or to another address:

(transfer transition from erc20.act)

transition transfer(uint256 _value, address to) : bool

iff
   ...

case CALLER != to:

  updates

   balanceOf := balanceOf[
                CALLER => balanceOf[CALLER] - _value,
                to     => balanceOf[to]     + _value ]

  returns true

case CALLER == to:

  returns true

If the sender is transferring to another address (CALLER != to), the balances of both the sender and the recipient are updated accordingly. If the sender is transferring to themselves (CALLER == to), no storage updates are happening, and the transition simply returns 1. This separation is necessary because act updates are non-sequential: all updates refer to the pre-state. Writing the cases explicitly avoids ambiguity. Details on updates are explained next.

Storage Updates Are Simultaneous

Storage updates are not a sequence of assignments, but rather a set of equations that must hold on the final state. Therefore, updates are simultaneous: all right-hand sides refer to the initial state and all left-hand sides are storage slots that are modified by the transition.

Consider the "standard" case of the ERC20 transferFrom transition:

(snippet from erc20.act, transferFrom transition)

case src != dst and CALLER != src and allowance[src][CALLER] < 2^256 - 1:

   updates
   balanceOf := balanceOf[
                  src => balanceOf[src] - amount,
                  dst   => balanceOf[dst]   + amount ]

   allowance := allowance[
                  src => allowance[src][
                           CALLER => allowance[src][CALLER] - amount ]]

This does not mean adapt balanceOf first and allowance second. Instead, it means: “In the final state, the mapping balanceOf equals the old one except the fields from and to where updated, and allowance equals the old mapping except from now maps to a different mapping (the one from before except CALLER maps to allowance[from][CALLER] - _value).” All right-hand sides are evaluated in the initial state. This design avoids accidental order-dependence and makes transitions suitable for formal reasoning.

Note that if the balance in Ether of a contract changes during a transition (e.g., in a payable transition), this has to be reflected in the updates block by updating the special variable BALANCE accordingly.

Storage Updates Are Partially Ordered

In general, the updates block can be arranged in any order, as all updates are simultaneous. There is, however, one subtlety to be aware of: if a storage slot is updated and also a specific field of that slot is updated, the more general references have to be listed before the specific ones.

The most common scenario where this arises is when a contract has another contract other_contract_instance in its storage, and both the entire contract and a specific field some_field of it are updated in the same updates block:

other_contract_instance := <constr_other_contract>(<constr_parameters>) (general update) has to happen before
other_contract_instance.some_field := <expression> (specific field update).

Let's illustrate this with a motivated example. We first define a simple contract Admins that tracks two admin addresses. This contract will be used in another contract Asset below to show the ordering requirement.

contract Admins

constructor(address _admin1)
iff true

creates
   address admin1 := _admin1
   address admin2 := ORIGIN

transition set_admin2(address new_admin2)
iff true
updates
   admin2 := new_admin2

...

Admins is a simple contract that tracks two admin addresses. The first admin is set during construction, while the second admin is initialized to the transaction origin (ORIGIN). We assume that only admin2 can be externally updated via the admin2 transition. (That means in the solidity equivalent, admin1 would be immutable and admin2 would have a setter function.)

contract Asset

constructor(uint256 _value)
iff true
creates
    uint256 _value := _value
    Admins admins := new Admins(CALLER)
    mapping(address => uint256) balanceOf := [THIS => _value]



transition assetTransfer(uint256 amt, address to) : bool

iff CALLER == admins.admin1 or CALLER == admins.admin2
    inRange(uint256, balanceOf[THIS] - amt)
    THIS != to ==> inRange(uint256, balanceOf[to] + amt)

case THIS != to

updates
   balanceOf := balanceOf[
                  THIS => balanceOf[THIS] - amt,
                  to   => balanceOf[to]   + amt ]

returns true

case THIS == to

returns true


transition setAdmins(address new_admin1, address new_admin2)

iff true

case CALLER == admins.admin1 or CALLER == admins.admin2

updates
   admins := new Admins(new_admin1)
   admins.admin2 := new_admin2

case not (CALLER == admins.admin1 or CALLER == admins.admin2)

...

(This example has been added to the benchmarks as ordered_updates.act and can be proven equivalent to the corresponding ordered_updates.sol implementation.)

(Note: the trivial precondition blocks (iff true) could be omitted for brevity.)

Let's consider now the Asset contract above.

The contract Asset is a variation of a drastically simplified token contract (similar to ERC20).
The relevant difference is that only the two admin addresses can transfer tokens from the contract's own balance to other addresses. (See the assetTransfer transition.)
The Admins contract (introduced above) is used to track the two admin addresses. (See the constructor of Asset.)
There is an extra transition setAdmins that allows either admin to update both admin addresses.

Ordered Updates

Consider the setAdmins transition, where in the first case case CALLER == admins.admin1 or CALLER == admins.admin2 both admin addresses are updated. We are in the situation described earlier: there is a general update of a storage slot and afterwards a specific field of that slot is updated:

admins := new Admins(new_admin1) (general update)
admins.admin2 := new_admin2 (specific field update)

This ordering is necessary to ensure that the updates have unambiguous semantics. Otherwise the general update would "rewrite" the specific field update, making the specification of that field obsolete and potentially confusing. The references on the left-hand side of the equations are evaluated sequentially, such that potentially newly created contract addresses can also be reached when updating a specific field of such contract: that means the right-hand side of the second update admins.admin2 := new_admin2 refers to the updated value of admins from the first update.

This ordering is part of act's type system: a specification violating this property would raise an error during type checking.

How to Write Your Own Spec

Table of Contents

This section provides a step-by-step guide on writing your own act specification for an Ethereum smart contract. We will cover the essential components, best practices, and common patterns to help you get started quickly.

Overview: From implementation to act

For the purposes of this tutorial, we will refer to Solidity implementation, but the concepts apply equally to other Ethereum contract languages.

The general process of writing an act specification involves:

Understand the Contract Structure: Identify contract name, constructor parameters, public state variables (storage), and all external/public functions (transitions including getters).
Establish Preconditions: Convert Solidity's require statements to act's iff preconditions and add inRange checks for arithmetic safety to prevent overflow/underflow.
Define the case Blocks: Use case blocks to handle different execution paths (from if-then-else, mapping updates with overlapping keys, or inlined function calls).
Initialize Storage in the Constructor: Initialize all storage variables with their initial values in the creates block.
Specify Storage Updates and Return Values: List all storage updates in the updates block (remembering they are simultaneous) and specify return values for functions with return types.

We will use a running example, that was introduced in Storage Updates are Partially Ordered, to illustrate the steps. Imagine we have the follwing solidity code declaring two contracts, which we want to specify in act:

(code from ordered_updates.sol)

pragma solidity >=0.8.0;

contract Admins {
    address public admin1;
    address public admin2;

    constructor(address _admin1) {
        admin1 = _admin1;
        admin2 = tx.origin;
    }

    function set_admin2(address new_admin2) public {
        admin2 = new_admin2;
    }

}

contract Asset {
    uint256 public Value;
    Admins admins;
    mapping (address => uint256) public balanceOf;

    constructor(uint256 _value) {
        Value = _value;
        admins = new Admins(msg.sender);
        balanceOf[address(this)] = _value;
    }

    function assetTransfer(uint256 amt, address to) public returns (bool) {
        require (msg.sender == admins.admin1() || msg.sender == admins.admin2());

        balanceOf[address(this)] = balanceOf[address(this)] - amt;
        balanceOf[to] = balanceOf[to] + amt;

        return true;
    }

    function setAdmins(address new_admin1, address new_admin2) public {
        if (msg.sender == admins.admin1() || msg.sender == admins.admin2()) {
            admins = new Admins(new_admin1);
            admins.set_admin2(new_admin2);
        }
    }
}

Step 1: Understand the Contract Structure

Begin by analyzing your Solidity contract:

Identify the contract name and specify it in act using the contract keyword.
Specify the constructor: Look for the constructor function and note its parameters. Specify it using the constructor keyword and copy the constructor parameters. If the parameter is address and is later cast to a contract type <ContractName>, use an annotated contract type address<ContractName>. If the constructor is payable in the source code, mark it as payable in act (constructor (<parameters>) payable). Leave the iff blank for now.
Identify all state variables. These become storage in act and will be initialized in the constructor. In solidity they are listed at the top of the contract. List them in the constructor's creates block: Specify the type and name of each storage variable.
List all external and public functions. These become transitions. Also the getter functions for public state variables which are automatically generated by Solidity have to be listed as transitions. You have to name these getter functions the same as corresponding storage variables. Specify the transitions after the constructor using the transition keyword (respectively transition (<parameters>) payable for payable ones), copy the parameters from the source code. If the parameter is address and is later cast to a contract type <ContractName>, use an annotated contract type address<ContractName>. If a function has a return value, specify its type after the parameter list using : <return_type>.

What we would have at this point for our example:

contract Admins
 
constructor(address _admin1)
iff <todo>

creates
    address admin1 := <todo>
    address admin2 := <todo>

transition set_admin2(address new_admin2)
<todo>

transition admin1() : address
<todo>

transition admin2() : address
<todo>


contract Asset

constructor(uint256 _value)
iff <todo>
creates
    uint256 Value := <todo>
    Admins admins := <todo>
    mapping(address => uint256) balanceOf := <todo>

transition assetTransfer(uint256 amt, address to) : bool
<todo>

transition setAdmins(address new_admin1, address new_admin2)
<todo>

transition Value() : uint256
<todo>

transition balanceOf(address account) : uint256
<todo>

Step 2: Establish Preconditions

The preconditions of a transition are specified in the iff block. They define the conditions that must hold for the transition to execute successfully. It combines explicit and implicit requirements:

Explicit requirements: These are conditions that are explicitly checked in the Solidity code using require statements. Each require statement translates to a line in the iff block. Some preconditions arise from the unique ownership requirement, i.e. storage of the contract does not contain any aliased reference to another contract, see aliasing section. This would usually mean that if many contract addresses are taken as parameters to constructors or transitions, the ones stored in the storage have to be distinct. Note that these need to already be present in the Solidity implementation of the contract, not merely in the act specification.
Implicit requirements: These are conditions that are not explicitly listed in the code but are necessary for the correct execution of the transition: These are checks to prevent arithmetic overflow/underflow. Arithmetic safety is addressed using the inRange expression. To ensure every arithmetic operation is safe, an inRange check has to be added for every occurring operation.

Guidelines:

Convert each require(condition) to a line in the iff block
Multiple conditions are implicitly conjunctive (all must be true)
Each arithmetic operation that can overflow/underflow must have a corresponding inRange check (Syntax inRange(<type>, <expression>))
Use logical operators (and, or, ==> (implication), etc.) as needed. Full list of operators can be found in Base Expressions
The syntax to access fields of a mapping is mapping_name[key].
When using annotated addresses as pure addresses (e.g., in comparisons), cast them to regular address type using address(<expression>).
When accessing fields of other contracts, use dot notation: contract_instance.field_name
Use the special variables to describe EVM environment:
- CALLER instead of msg.sender
- CALLVALUE for the amount of Ether sent
- THIS for the contract's own address
- ORIGIN for tx.origin

Our example specification would look like this after adding the preconditions. In practice one would fill one transition at a time. But for clarity we follow each step for the whole spec. We also chose to explicitly fill all the iff blocks, even though most of them are trivial (iff true) in this example and could be omitted.

contract Admins
 
constructor(address _admin1)
iff true

creates
    address admin1 := <todo>
    address admin2 := <todo>

transition set_admin2(address new_admin2)
iff true
<todo>

transition admin1() : address
iff true
<todo>

transition admin2() : address
iff true
<todo>

contract Asset

constructor(uint256 _value)
iff true
creates
    uint256 Value := <todo>
    Admins admins := <todo>
    mapping(address => uint256) balanceOf := <todo>

transition assetTransfer(uint256 amt, address to) : bool
iff CALLER == admins.admin1 or CALLER == admins.admin2
    inRange(uint256, balanceOf[THIS] - amt)
    THIS != to ==> inRange(uint256, balanceOf[to] + amt)
<todo>

transition setAdmins(address new_admin1, address new_admin2)
iff true
<todo>

transition Value() : uint256
iff true
<todo>

transition balanceOf(address account) : uint256
iff true
<todo>

The only interesting precondition is in the assetTransfer transition, which corresponds to the require statement in the Solidity code and two inRange checks. Let us look closer into the inRange checks:

In the Solidity function assetTransfer, the line balanceOf[address(this)] = balanceOf[address(this)] - amt; performs a subtraction. To ensure that this subtraction does not underflow, we add the precondition inRange(uint256, balanceOf[THIS] - amt).
If the previous line did not revert, the code proceeds to the line balanceOf[to] = balanceOf[to] + amt;, where it performs an addition. If to is different from this, this addition could overflow, otherwise (if to == this) it will just go back to its original value. To ensure that this addition does not overflow, we add the precondition THIS != to ==> inRange(uint256, balanceOf[to] + amt).

Step 3: Define the `case` Blocks

If the constructor or a transition has multiple paths either explicit, through e.g. an if then else or implicit where the transition's behavior changes depending on something (e.g. whether THIS == to in the step above), case blocks have to be used to separate these paths. Each case block has a condition and the corresponding storage initialization or updates.

To paraphrase, within each case block the what happens to the storage of the contract can be defined through the same set of equations that hold after the execution of the function in this particular case. This set of equations is defined in the creates block for constructors and in the updates block for transitions.

When there is just one single path in a constructor or transition, no case block is needed. Proceed to step 4 in this case.

Common Patterns for case Blocks

If-then-else: When there are two or more paths (e.g., an if-else), use case blocks with complementary conditions.
Changing Values of Mappings: When two or more keys of a mapping are assigned new values, the end state of the mapping depend on if some of the keys were equal or not. Use case blocks to separate these scenarios.
Function Calls: As mentioned before: act describes the impact a function has on a contract's storage. Hence, if within a Solidity function, another function is called, this has to be "inlined" in the act specification. That means the called function's logic has to be flattened into the current one's. Which most likely leads to case blocks. Details below in section Inline Function Calls. Note that this only applies to transitions, constructors can in fact be called in act without inlining.

Guidelines:

Conditions of the case blocks must be mutually exclusive and exhaustive
Multiple conditions are implicitly conjunctive (all must be true)
Use logical operators (and, or, ==> (implication), ==, !=, etc.) as needed. Full list of operators can be found in Base Expressions
The syntax to access fields of a mapping is mapping_name[key].
When accessing fields of other contracts, use dot notation: contract_instance.field_name
Use the special variables to describe EVM environment:
- CALLER instead of msg.sender
- CALLVALUE for the amount of Ether sent
- THIS for the contract's own address
- ORIGIN for tx.origin

After considering this step the specification of the running example only the transiitons assetTransfer and setAdmins changed, since all other transitions and constructors hve only one path. The transitions with case blocks look like this:


transition assetTransfer(uint256 amt, address to) : bool
iff CALLER == admins.admin1 or CALLER == admins.admin2
    inRange(uint256, balanceOf[THIS] - amt)
    THIS != to ==> inRange(uint256, balanceOf[to] + amt)

case THIS != to
<todo>

case THIS == to
<todo>



transition setAdmins(address new_admin1, address new_admin2)
iff true

case  CALLER == admins.admin1 or CALLER == admins.admin2
<todo>

case not (CALLER == admins.admin1 or CALLER == admins.admin2)
<todo>

In the assetTransfer function, the values of THIS and to of the balanceOf mapping are changed. Which equations are true afterwards depend on whether THIS and to are identical.

In setAdmins, there is a simple if that splits two paths, hence also in the act spec we have two paths accordingly.

Step 4: Initialize Storage in the Constructor

The constructor initializes all storage variables. Every storage variable must be initialized in every execution path (i.e. in every case block). This has been mostly prepared already in step 1. What is left to do is

copy the behavior of Solidity's constructors while considering the following guidelines
and for payable constructors: the contracts balance in Ether has to be initialized. This is done using the special variable BALANCE with type uint256:

Most of the time this is just uint256 BALANCE := CALLVALUE, but if there are more complex behaviors in the Solidity constructor, such as forwarding some of the CALLVALUE to another contract's constructor, this has to be reflected here (e.g. uint256BALANCE := CALLVALUE - <forwardedAmount>).
ensure that no two storage instances refer to the same contract (unique ownership invariant, see Aliasing section). This has to already hold in the Solidity implementation.

Guidelines:

Use := to assign the initial value
For payable constructors, initialize the contract's balance in Ether using the special variable BALANCE
For mappings, use [] for empty mappings or [<key> => <value>, ...] to initialize specific entries. Entries that are not specified are set to the type's default value.
In every case block all storage variables must be initialized.
As in Solidity, constructors of other contracts can be called and assigned using the keyword new.
Use the special variables to describe EVM environment:
- CALLER instead of msg.sender
- CALLVALUE for the amount of Ether sent
- THIS for the contract's own address
- ORIGIN for tx.origin
- BALANCE for the contract's balance in Ether

In our example the constructors of the two contracts have this final form:

contract Admins

constructor(address _admin1)
iff true

creates
   address admin1 := _admin1
   address admin2 := ORIGIN

...

contract Asset

constructor(uint256 _value)
iff true
creates
    uint256 Value := _value
    Admins admins := new Admins(CALLER)
    mapping(address => uint256) balanceOf := [THIS => _value]

Step 5: Specify Storage Updates and Return Values

What is left to do now, is to explicitly list all storage slots that were updated in each transition and each case block. As well as specify the return value if there is a return type in the transition signature. We start with the storage updates.

Storage Updates

If for a transition and case no storage slot was changed, then the updates block is skipped. A common example for such a case are getter functions.

For all other transitions and case blocks, there has to be an updates block. The updated storage slots are listed after the keyword; one update per line. The syntax to update a storage slot is <storage_slot> := <new_value>.

Be aware that Storage updates are simultaneous! That means that all right-hand sides of the updates are evaluated in the pre-state (before the function call). This avoids order-dependence and makes transitions suitable for formal reasoning. As mentioned before, these update statements serve as a set of equations that hold after execution. They are not to be seen as assignments.

Consequently, every storage slot can be mentioned within the same case block at most once (except for the special case explained below). Further, mappings are updated as a whole in one single statement, not one update per mapping entry.

If the contract's balance in Ether changes during its execution (e.g. by calling a payable constructor), this has to be reflected in the updates block by updating the special variable BALANCE accordingly.

There is one special case about updates. If a contract uses an instance of another contract in its storage, as the Asset contract contains an instance of the Admins contract in our example, which is called admins; and if now, within one transition and case block, the entire admins contract instance is updated and also one of admins' fields is updated, the more general update has to be stated before the more specific one. For details see Storage Updates Ordering.

Guidelines:

The syntax for updating a mapping is : mapping_name := mapping_name[key1 => new_value1, key2 => new_value2]
All right-hand sides use pre-state values (e.g., balanceOf[CALLER] - _value subtracts from the old balance)
Right-hand-sides of updates cannot be transition calls. Transition calls have to be inlined as described in step 3 and section Inline Function Calls
If the contract's balance in Ether changes, update it using the special variable BALANCE
Every storage slot can be mentioned at most once per case block, except for the explained special case
Consider the special case: state more general updates before more specific ones
Ensure that no two storage instances refer to the same contract (unique ownership invariant, see Aliasing section).

Return values

For each transition where the signature specifies a return type, returns <expression> has to be present for each case block. The returned expression can reference storage and parameters but always refers to the pre-state.

Guidelines:

Use returns <expression> to specify the return value
The return value can reference storage and parameters but always refers to the pre-state

The final act specification of the Solidity code at the beginning of this page is the following:

(also available as ordered_updates.act)

contract Admins

constructor(address _admin1)
iff true

creates
   address admin1 := _admin1
   address admin2 := ORIGIN

transition set_admin2(address new_admin2)
iff true
updates
   admin2 := new_admin2

transition admin1() : address
iff true
returns admin1

transition admin2() : address
iff true
returns admin2





contract Asset

constructor(uint256 _value)
iff true
creates
    uint256 Value := _value
    Admins admins := Admins(CALLER)
    mapping(address => uint256) balanceOf := [THIS => _value]



transition assetTransfer(uint256 amt, address to) : bool

iff CALLER == admins.admin1 or CALLER == admins.admin2
    inRange(uint256, balanceOf[THIS] - amt)
    THIS != to ==> inRange(uint256, balanceOf[to] + amt)

case THIS != to

updates
   balanceOf := balanceOf[
                  THIS => balanceOf[THIS] - amt,
                  to   => balanceOf[to]   + amt ]

returns true

case THIS == to

returns true



transition setAdmins(address new_admin1, address new_admin2)

iff true

case CALLER == admins.admin1 or CALLER == admins.admin2

updates
   admins := new Admins(new_admin1)
   admins.admin2 := new_admin2

case not (CALLER == admins.admin1 or CALLER == admins.admin2)


transition Value() : uint256
iff true
returns Value

transition balanceOf(address idx) : uint256
iff true
returns balanceOf[idx]

Note that in setAdmins, we are in this special case where a contract instance and one of its fields are updated in the same updates block. So the general update of admins comes first, and the update of admins.admin2 comes second.

Summary

Be explicit about control flow: Use case blocks liberally to avoid ambiguity
Use annotated address type: If an address is used as a contract instance in the source code, annotate it with the contract type (e.g., address<ContractName>). When an annotated address is used as a pure address, cast it to a regular address type using address(<expression>).
Check arithmetic safety: Use inRange for every operation that could overflow/underflow and add it to iff
Remember updates are simultaneous: All right-hand sides refer to the pre-state
Initialize all storage variables: Every storage variable must appear in every creates block (in the constructor).
Make conditions exhaustive: Each set of cases must cover all possibilities
Convert all requirements: Every Solidity require becomes an iff condition or implicit in a case
Specify getters: Even view functions need to be specified as transitions using the same name as storage variables.
Use meaningful variable names: Match your Solidity code for clarity
Inline transition calls: A storage update cannot be a transition call, it's logic and affects have to be embedded as case blocks.
Be aware of ordered updates: When storage updates a contract instance and a field of that contract instance, the contract instance itslef has to be listed first in the updates block
Reference the documentation: Consult the Storage, Typing and Expressions, Constructors, and Transitions sections for detailed explanations

Inline Function Calls

When a function of a smart contract calls another function and uses its return value to update storage, act requires you to inline the called function's behavior (in the transition) rather than representing it as a function call. This design choice is crucial for formal reasoning: it makes the complete state transition explicit and avoids the need to reason about nested function calls.

Why Inlining is Required

In act, storage updates must be explicit expressions that can be evaluated in the pre-state. Function calls are not allowed on the right-hand side of storage updates because:

Formal reasoning: act specifications describe state transitions as mathematical equations. Inlining makes these equations self-contained and verifiable.
Clarity: The complete behavior of each transition is visible in one place, without needing to trace through multiple function definitions.
Composability: Each transition can be analyzed independently without worrying about side effects from nested calls.

How to Inline Function Calls

When you encounter a Solidity function that calls another function, follow these steps:

Identify the called function: Note what function is being called and what it does.
Expand the call: Replace the function call with the logic of the called function.
Add cases if needed: If the called function has multiple execution paths (cases), these must be reflected in the "calling" transition's cases.
Combine preconditions: The preconditions of the called function have to be considered in the calling transition. Possibly, by adding them as implications (<case condition where call occurs> ==> <called transition's precondition>) to the preconditions.

Example: Simple Function Call

Consider this Solidity code where updateBalance calls computeNewBalance:

contract Example {
    uint256 public balance;
    
    function computeNewBalance(uint256 amount) internal view returns (uint256) {
        return balance + amount;
    }
    
    function updateBalance(uint256 amount) public {
        balance = computeNewBalance(amount);
    }
}

Incorrect act specification (function call in update):

// This is NOT valid act syntax
transition updateBalance(uint256 amount)

updates
   balance := computeNewBalance(amount)  // ❌ Function calls not allowed here

Correct act specification (inlined):

transition updateBalance(uint256 amount)
iff inRange(uint256, balance + amount) // ✓ Added the (implicit) precondition of computeNewBalance
updates
   balance := balance + amount  // ✓ Inlined the logic of computeNewBalance

Example: Function Call with Branching

Extending the previous example, consider what happens when the called function has multiple paths:

contract BranchingExample {
    uint256 public balance;
    
    function computeNewBalance(uint256 amount, bool addBonus) internal view returns (uint256) {
        if (addBonus) {
            return balance + amount + 1;
        } else {
            return balance + amount;
        }
    }
    
    function updateBalance(uint256 amount, bool addBonus) public {
        balance = computeNewBalance(amount, addBonus);
    }
}

Incorrect act specification:

// This is NOT valid act syntax
transition updateBalance(uint256 amount, bool addBonus)

updates
   balance := computeNewBalance(amount, addBonus)  // ❌ Function call

Correct act specification (inlined with cases and preconditions):

transition updateBalance(uint256 amount, bool addBonus)
iff addBonus ==> inRange(uint256, balance + amount + 1)
    (not addBonus) ==> inRange(uint256, balance + amount)

case addBonus
updates
   balance := balance + amount + 1  // ✓ Inlined the bonus case

case not addBonus
updates
   balance := balance + amount  // ✓ Inlined the no-bonus case

Note how:

The branching logic from computeNewBalance becomes case conditions
The arithmetic safety check (inRange) is added to the preconditions using implications
Each case explicitly states what value balance takes after the transition

Special Note: Constructor Calls

Unlike transition calls, constructor calls do not need to be inlined. You can write:

creates
   Admins admins := Admins(new_admin1)  // ✓ Constructor call is allowed

This is because constructors create new contract instances rather than modifying existing state, making them fundamentally different from transition calls in terms of formal reasoning.

Type-Checking

act's type-checking process ensures that specifications are both syntactically correct and semantically sound. It combines traditional static type-checking with semantic verification using SMT solvers. Type safety is proven in detail. A full tech report will be available shortly.

The type-checker implements the formal typing judgments defined in act's type system. It verifies that all expressions are well-typed according to typing rules, which take storage declarations, interface parameters, and local bindings into account. The type-checker proceeds systematically: it first type-checks each contract's constructor, memorizing the constructor's storage declarations, then type-checks each transition against the updated environment. This ensures type consistency across the entire specification and catches errors like type mismatches, undefined variables, and invalid operations before proceeding to the verification backends.

Additionally, the type-checker performs semantic checks using SMT solvers to verify properties that go beyond static typing. These checks ensure logical soundness and completeness of specifications and include verifying that:

arithmetic expressions are within the required bounds of their types;
constructor preconditions hold when they are called;
case conditions are exhaustive and non-overlapping.

1. Arithmetic Safety

act requires explicit inRange expressions to verify that arithmetic operations stay within the bounds of their declared types. An SMT solver is used to verify this property symbolically for all intermediate and final arithmetic evaluations.

Why it matters?

To formally verify smart contract specifications, it is crucial to ensure that arithmetic operations do not overflow or underflow their intended types. In Solidity, for example, arithmetic operations are checked at runtime to prevent overflows and underflows, if one occurs, the transaction reverts.

In act, a constructor/transition "reverts" if and only if the preconditions fail. Therefore, for an act specification to type-check, all arithmetic operations that could potentially overflow or underflow in the compiled bytecode must be guarded by inRange checks in the preconditions. (Note that if the contract code does not check for overflow, then act should not check for it either.) If the act spec does not express the possibility of overflow anywhere, then there will be no overflow (assuming the contract's behaviour is also proven equivalent).

How it works:

When you write inRange(uint256, expression) in a precondition, the type-checker generates an SMT query to verify that for all valid pre-states satisfying the preconditions (one of them being the inRange condition itself), no expression in the constructor/transition can evaluate to a value that falls outside the specified type's range (e.g., 0 to 2^256 - 1 for uint256).

Example:

(snippet from erc20.act, transfer transition)

transition transfer(address to, uint256 _value)
iff 
  inRange(uint256, balanceOf[CALLER] - _value)
  CALLER != to ==> inRange(uint256, balanceOf[to] + _value)

case CALLER != to:
  updates
    balanceOf := balanceOf[
                    CALLER => balanceOf[CALLER] - _value,
                    to => balanceOf[to] + _value]

The SMT solver verifies that given

inRange(uint256, balanceOf[CALLER] - _value) and
CALLER != to ==> inRange(uint256, balanceOf[to] + _value)

No arithmetic overflow or underflow occurs in any (sub-)expression anywhere in this transition.

Failure behavior:

If an inRange condition (as any other precondition) fails, the transition reverts and no storage updates occur. This aligns with Solidity's execution model and allows act to precisely characterize the contract's input space.

Technical Limitation

The reason for not only checking the top-level expressions but also all intermediate expressions comes from act's equivalence checker, which is imported from hevm (see hevm backend: Equivalence to EVM bytecode). The equivalence checker uses hevm's internal representation, which does not have unbounded integers, and therefore all expressions must be representable in the EVM's 256-bit integer space.

Note: it is suggested to read section hevm backend: Equivalence to EVM bytecode before continuing.

EVM semantics vs. act semantics

The semantics of the EVM (and subsequently hevm) and act are slightly different when it comes to overflow. The former has modulo arithmetic while the latter has unbounded integers. So, for example, in the case of multiplication,

the semantics of the EVM opcode is: MUL opA opB = (opA * opB) % 256, where * is the mathematical operation of multiplication
whereas in act, the semantics are the actual mathematical ones.

Relevance for Equivalence Checking

Let's see how this difference leads to requiring overflow checks for intermediate expressions. Assume we want to check the equivalence of the following Solidity function with the following act transition:

Solidity function f

contract A {
  uint256 a; uint256 b;

  function f(uint256 x) returns(uint256) {
    require(COND, "some desired precondition");
    a = x;
  }
}

act transition f

contract A
  ...
  transition f(uint256 x) : uint256
  iff
    COND // the same as the solidity code

  updates
    a := x*b/b

In this example both formulations have identical preconditions. In other words the input space is equivalent, and will be demonstrated to be so by hevm.

Therefore let us study the storage updates:

On the one side the final value of the storage variable a is x, while on the other it is x*b/b, where the operators follow act's semantics. Since act's semantics are those of unbounded integers, the spec is equivalent for this transition, and we would want the equivalence checker to confirm this.

However, since act's equivalence checker is imported from hevm, using its Expr representation, which does not have unbounded integers, this will fail: It is not possible to translate act's pure, unbounded * and / to hevm's MUL and keep the same semantics, because

while in act b may be any number in uint256 (and does not need to appear in the preconditions since x*b/b it will simplify to x for any non-zero b),
there will always be value of b in uint256 sufficiently large to cause x*b overflow out of the 256-bit range. And this leads to the the equivalence checker concluding that x == x*b/b is false.

To address this, act implements its additional overflow pass. It checks that given the preconditions, all the intermediate expressions have values within the range representable by hevm. Note that it checks this on the act level, i.e. using SMT passes on unbounded integer theory. This guarantees that we operate under an input space in which the semantics of act's * and the EVM's MUL opcode are identical. So in the above example, the pass will return an error, saying that the specification cannot be equivalence checked because it contains expressions that are not computable by the EVM.

This is not a limitation on the number of contract's we can specify, as any realizable contract's behaviour must be expressible through computable expressions.

Still, we aim to remove this constraint in the future versions.

This output error for the above example looks as follows:

Operands of / must be both signed or both unsigned
counterexample:

  calldata:

    (x = 2)

  environment:

    CALLVALUE = 0

  storage:
    
    prestate:

      x = 2
      pre(b) = 57896044618658097711785492504343953926634992332820282019728792003956564819968


:
9 |       a := x*b/b
                  ^
Result of * must be in the range of int256 or uint256
counterexample:

  calldata:

    (x = 2)

  environment:

    CALLVALUE = 0

  storage:
    
    prestate:

      x = 2
      pre(b) = 57896044618658097711785492504343953926634992332820282019728792003956564819968


:
9 |       a := x*b/b
                ^
Integer expression of type integer is not guaranteed to fit in type uint256
counterexample:

  calldata:

    (x = 0)

  environment:

    CALLVALUE = 0

  storage:
    
    prestate:

      x = 0
      pre(b) = 0


:
9 |       a := x*b/b
                  ^

Subsequent Limitation: Expressing Overflow/Underflow in act

To express overflow/underflow in act, the ideal way would be to use the mathematical formulation (a+b)%max. This works for all ranges, except the 256-bit one, where the additional overflow pass will catch a+b. There is currently no way to express 256-bit-overflow in act without triggering the overflow pass. We aim to cover this in future versions.

2. Constructor Precondition Verification

When a constructor is called to create a new contract instance (e.g., new Token(100) in a storage update), act verifies that the constructor's preconditions are satisfied at the call site.

Why this matters:

Contract creation is a crucial operation. If a constructor's preconditions aren't met, creation fails and the entire transaction reverts, which would therefore not actually initialize/update storage as specified. Therefore act has to ensure every constructor call in the specification is valid, for the entire act spec to be well-typed.

How it works:

The type-checker implements a semantic check to verify if the current state and environment satisfy the constructor's preconditions: For each constructor call (e.g. AMM(t0,t1)), the SMT solver verifies that given the current constraints (preconditions, case conditions and current state, in our example t0, t1) , the constructor's preconditions are entailed.

Example:

We revisit the constructor of an AMM contract.

(snippet from amm.act)

contract Amm

constructor(address<Token> t0, address<Token> t1)
iff   address(t0) != address(t1)
creates
    Token token0 := t0
    Token token1 := t1
...

When Amm's constructor is called, e.g., in another contract's constructor:

contract Wrapper
constructor(address<Token> t0, address<Token> t1)

creates
    Amm amm := new Amm(t0, t1)

For the constructor call Amm(t0, t1), the SMT solver verifies that given the current information:

preconditions: none,
case conditions: none
information about the values t0, t1: they are of type address<Token>

the constructor precondition address(t0) != address(t1) holds. In this example, this is clearly not the case, since t0 and t1 could be equal addresses. Therefore, this semantic check would fail and therefore the act specification does not type-check, reporting an error

Preconditions of constructor call to "Amm" are not guaranteed to hold

and listing a counterexample calldata.

To fix the example, add the precondition address(t0) != address(t1) to the Wrapper constructor.

3. Case Condition Verification

The last semantic check happening during type-checking is about the case conditions in transitions and constructors. As explained before, act uses case blocks to represent different execution paths in constructors and transitions. In this check, the SMT solver verifies two critical properties of case conditions:

a) Exhaustiveness: The case conditions must cover all possible scenarios given the preconditions. Formally, the type system requires:

preconditions ==> (C₁ or C₂ or ... or Cₙ)

where Cᵢ are the case conditions.

b) Non-overlapping: The case conditions must be mutually exclusive. For any two distinct cases i and j, their conditions cannot both be true at the same time:

not (Cᵢ and Cⱼ)

Why this matters:

If one of this two properties does not hold, the specification is ambiguous or incomplete and therefore unsound: If the case conditions are not exhaustive, there exist inputs for which no case applies, leading to undefined behavior. Similarly, if case conditions overlap, multiple cases apply simultaneously, causing ambiguity in the contract's behavior.

Example

We revisit the transfer transition of the ERC20 contract:

(snippet from erc20.act, transfer transition)

transition transfer(address to, uint256 _value) : bool
iff
    inRange(uint256, balanceOf[CALLER] - _value)
    CALLER != to ==> inRange(uint256, balanceOf[to] + _value)

case CALLER != to:
  storage
    balanceOf := balanceOf[
                    CALLER => balanceOf[CALLER] - _value,
                     to    => balanceOf[to] + _value ]
    returns true

case CALLER == to:
    returns true

✓ The SMT solver verifies:

Exhaustive: (CALLER == to) or (CALLER != to) is always true
Non-overlapping: (CALLER == to) and (CALLER != to) is always false

Aliasing and Unique Ownership

In order to reason about smart contracts in a purely functional way, we leverage the concept of unique ownership. This means that each contract has a single owner, and there are no shared references to the contract's state. This simplifies reasoning about state changes and ensures that contracts cannot inadvertently interfere with each other.

We showcase an issue with aliasing in the following example: suppose we have a contract A that contains two storage variables that contain an ERC20 token: Token t0 and Token t1.

contract A 
    constructor(address<Token> a0, address<Token> a1) 
        creates 
            Token t0 := a0
            Token t1 := a1
    transition transfer (uint256 _value, address to)
        updates 
            t0.balanceOf := t0.balanceOf[CALLER => t0.balanceOf[CALLER] - _value]
            t1.balanceOf := t1.balanceOf[to => t1.balanceOf[to] + _value]

To reason about the contract A in Rocq in a purely functional way, we would map the contract to a Rocq record of type

Record State := {t0: Token.State; t1: Token.State}

In this example, if a0 and a1 point to the same ERC20 Token contract, then the transfer transition update of t0.balanceOf will also affect t1.balanceOf, breaking the functional abstraction we want to achieve (namely modifying only the t0 field in the record).

However, if we can prove that t0 and t1 can never alias then we can safely reason about their state changes independently. Note that including an iff address(a0) != address(a1) condition in the constructor's preconditions is required, but not sufficient, as the Token contract itself also needs to avoid aliasing. But since we also have the Token contract specification ready, act will verify the unique ownership property also for that.

This unique ownership property is verified automatically for act specifications using symbolic execution and SMT solving. Note that the unique ownership property is not an implicit check in act, but rather an implicit assumption, which is then check to hold in the post-state, to make sure it is upheld as an invariant.

hevm Backend: Checking Equivalence with EVM Bytecode

Table of Contents

EVM bytecode can be formally verified to implement an act spec. This means that each successful behavior of the bytecode should be covered by the act spec and vice-versa.

To check equivalence, act leverages the symbolic execution engine in hevm. The act spec is translated to Expr, the intermediate representation of hevm, and the EVM bytecode is symbolically executed to obtain its Expr representation. Then equivalence can be checked with the equivalence checker of hevm.

Usage

The hevm backend performs automated equivalence checking between act specifications and EVM bytecode implementations. It is language agnostic, currently (version 0.2.0) supporting verification of contracts written in both Solidity and Vyper.

Basic Usage Patterns

1. Single contract with Solidity:

act equiv --spec <PATH_TO_SPEC> --sol <PATH_TO_SOL>

2. Single contract with Vyper:

act equiv --spec <PATH_TO_SPEC> --vy <PATH_TO_VY>

3. Multi-contract projects: (more info in Multi-Contract Projects)

act equiv --json <PATH_TO_CONFIG_JSON>

4. Direct bytecode verification:

act equiv --spec <PATH_TO_SPEC> --code <RUNTIME_BYTECODE> --initcode <CONSTR_BYTECODE> --layout Solidity

Command-Line Flags

Flag	Type	Default	Description
`--spec`	Path	-	Path to the act specification file (.act)
`--sol`	Path	-	Path to Solidity source file (.sol)
`--vy`	Path	-	Path to Vyper source file (.vy)
`--json`	Path	-	Path to JSON configuration file for multi-contract projects
`--solver`	`cvc5\|z3\|bitwuzla`	`cvc5`	SMT solver to use for verification
`--smttimeout`	Integer (ms)	`20000`	Timeout for each SMT query in milliseconds
`--debug`	Boolean	`false`	Print verbose output including raw SMT queries

Running the ERC20 Example

The act repository includes a complete ERC20 example demonstrating equivalence checking. The example files are located in tests/hevm/pass/multisource/erc20/.

Verify ERC20 against Solidity implementation:

act equiv --spec tests/hevm/pass/multisource/erc20/erc20.act \
         --sol tests/hevm/pass/multisource/erc20/erc20.sol

Verify ERC20 against Vyper implementation:

act equiv --spec tests/hevm/pass/multisource/erc20/erc20.act \
         --vy tests/hevm/pass/multisource/erc20/erc20.vy

The hevm backend will:

Compile the source code to EVM bytecode
Symbolically execute the bytecode
Check equivalence between the specification and implementation
Report success or provide counterexamples if differences are found

Expected Output for Successful Verification

When the ERC20 implementation matches its specification, you should see output similar to this:

Checking contract Token
Constructing the initial state.
Success. 
Checking if constructor results are equivalent.
Found 1 total pairs of endstates
Asking the SMT solver for 1 pairs
Success. 
Checking if constructor input spaces are the same.
Success. 
Checking if the resulting state can contain aliasing.
Success. 
Checking behavior transfer of Token
Constructing the initial state.
Success. 
Checking if behaviour is matched by EVM
Found 2 total pairs of endstates
Asking the SMT solver for 2 pairs
Success. 
Checking if the input spaces are the same
Success. 
Checking if the resulting state can contain aliasing.
Success. 
...
Checking behavior allowance of Token
Constructing the initial state.
Success. 
Checking if behaviour is matched by EVM
Found 1 total pairs of endstates
Asking the SMT solver for 1 pairs
Success. 
Checking if the input spaces are the same
Success. 
Checking if the resulting state can contain aliasing.
Success. 
Checking if the ABI of the contract matches the specification
Success.

Understanding the output:

Consult the how it works section for more details.

Checking contract Token: Initial verification that the contract structure is valid
Checking if constructor results are equivalent: Verifies that the constructor in the implementation produces the same storage state as the act specification
Found X total pairs of endstates: The number of distinct execution paths (success nodes, see here) that were identified during symbolic execution
Asking the SMT solver for X pairs: How many queries are sent to the SMT solver to verify equivalence between corresponding endstates
No discrepancies found: The SMT solver confirmed that for all inputs satisfying the path conditions, the results and storage are identical between specification and implementation
Checking if the input spaces are the same: Verifies that both the act spec and EVM implementation accept and reject the same set of inputs (no missing cases), see here
Checking if the resulting state can contain aliasing: Verifies that the state after a constructor or a transition cannot contain aliasing.
Checking if the ABI of the contract matches the specification: Ensures all function signatures match between the specification and implementation

What each transition check involves:

Checking transition X of act: Start verification of a specific function
Checking if transition is matched by EVM: Confirm the EVM implementation has corresponding behavior
Endstate equivalence: For each execution path, verify that when the same inputs are provided:
- Storage updates are identical
- Return values are identical
- Both succeed or both revert
Input space equivalence: Verify that the sets of inputs that succeed (or fail) are the same in both spec and implementation

When Verification Fails: Example with Broken ERC20

If the implementation doesn't match the specification, act provides a detailed counterexample. Consider a faulty ERC20 implementation where transfer incorrectly updates balances:

// Broken implementation
    function transfer(uint256 value, address to) public returns (bool) {
        require(balanceOf[msg.sender] >= value);
        if (to == address(0xdead)) {
            balanceOf[msg.sender] = balanceOf[msg.sender] - value;
            balanceOf[to] = balanceOf[to] + value + 1;  // Bug: adds extra token!
        } else {
            balanceOf[msg.sender] = balanceOf[msg.sender] - value;
            balanceOf[to] = balanceOf[to] + value;
        }
        return true;
    }

Running verification on this broken implementation produces:

Checking behavior transfer of act
Checking if behaviour is matched by EVM
Found 4 total pairs of endstates
Asking the SMT solver for 4 pairs
Not equivalent.

-----

The following input results in different behaviours
Calldata:
  transfer(0,0x000000000000000000000000000000000000dEaD)
Storage:
  Addr SymAddr "entrypoint": [(0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff01,0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe),(0x8000000000000000000000000000000000000000000000000000000000000001,0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)]
Transaction Context:
  TxValue: 0x0
Addrs:
  SymAddr "caller": 0xFF0000000000000000000000000000000000DEAD
  SymAddr "to": 0x000000000000000000000000000000000000dEaD

Interpreting the counterexample:

Calldata: The specific function call that triggers the bug: transfer(0, 0x000000000000000000000000000000000000dEaD) - transferring 0 tokens to address 0xdead
Storage: The contract state where the discrepancy occurs. The storage shows:
- Key-value pairs in hexadecimal representing storage slots
- 0x7fff...f01 ↦ 0xfff...ffe: Storage location and its value
- 0x8000...001 ↦ 0xfff...fff: Another storage location (likely total supply or balance)
Transaction Context:
- TxValue: 0x0 - No ETH sent with the call (0 wei)
Addrs: The symbolic addresses involved:
- SymAddr "caller": 0xFF...DEAD - The address executing the transaction
- SymAddr "to": 0x000...dEaD - The recipient address

This counterexample tells us that transferring 0 tokens to address 0xdead produces different results in the implementation versus the specification, allowing developers to locate and fix the bug.

Verifying Multiple Contracts with --sources

For complex projects with multiple interacting contracts, use a JSON configuration file, that might look like this:

JSON Structure (project.json):

{
  "specifications": ["<path-to-spec1>/spec1.act", "<path-to-spec2>/spec2.act"],
  "sources": {
    "<path-to-source1>/source1.sol": { "language": "Solidity" },
    "<path-to-source2>/source2.vy": { "language": "Vyper" },
    "<path-to-source3>/source3.vy": { "language": "Vyper" }
  },
  "contracts": {
    "Contract1": { "source": "<path-to-source1>/source1.sol" },
    "Contract2": { "source": "<path-to-source2>/source2.vy" },
    "Contract3": { "source": "<path-to-source3>/source3.vy" },
    "Contract4": { "source": "<path-to-source3>/source3.vy" },
    "Contract5": {
      "code" : "<path-to-bytecode-runtime>/bytecode.bin-runtime",
      "initcode" : "<path-to-bytecode-init>/bytecode.bin",
      "layout" : "Solidity"
    }
  }
}

Fields explained:

specifications: Array of act specification files. Note that the order matters. Any specification may only have dependencies on specifications that exists earlier in the list.
sources: Map of source files to their language (Solidity or Vyper)
contracts: Map of contract names to their source files

Note that specifications and sources may contain multiple contracts.

Running verification:

act equiv --sources project.json --solver bitwuzla --smttimeout 60000

Example: Automatic Market Maker (AMM) with Solidity and Vyper:

The act repository includes an example with mixed languages in tests/hevm/pass/multisource/amm/:

{
  "specifications" : ["../erc20/erc20.act", "amm.act"],
  "sources" : {
    "../erc20/erc20.vy" : { "language" : "Vyper" },
    "amm.sol" : { "language" : "Solidity" }
  },
  "contracts" : {
    "Token" : { "source" : "../erc20/erc20.vy"},
    "Amm" : { "source" : "amm.sol"}
  }
}

This allows verification of specifications against implementations in different languages, and verification of multiple contracts that interact with each other.

Additional Options

Choosing SMT solvers:

Different solvers have different strengths:

Bitwuzla: Specialized for bitvector reasoning; excellent for bitwise operations. Recommended for equivalence checking.
CVC5 (default): Good all-around performance, handles most common contracts. May fail at some contracts due to errors.
Z3: Alternative when CVC5 times out; sometimes faster on arithmetic-heavy specs

act equiv --spec contract.act --sol contract.sol --solver z3

Debugging failed proofs:

Use the --debug flag to see detailed SMT queries:

act equiv --spec contract.act --sol contract.sol --debug

This outputs:

The symbolic execution trace
Path conditions
Storage constraints
Raw SMT queries sent to the solver
Detailed counterexamples when equivalence fails

How it works

Success nodes

The Expr representation of an act program is a list of Success nodes, that contain the possible successful results of the computation. The Expr representation of the EVM bytecode can also be flattened to a list of result nodes from which we only keep the successful executions, filtering out failed and partial execution paths. An informative warning will be thrown when partial executions are encountered.

A success node in Expr, Success cond res storage, is a leaf in the Expr tree representation and contains the path conditions, cond that lead to the leaf, the result buffer res, and the end state storage.

In order to compute the index in storage for each variable mentioned in the spec, act needs to have access to the storage layout metadata output by the compiler.

Equivalence check

To check equivalence between the two Expr representations the following checks are performed.

Result equivalence

The two lists of Success nodes are checked for equivalence using the hevm equivalence checker. For each pair of nodes in the two lists, we check that for all inputs that satisfy the combined path conditions the result and final storage are the same.

In act v0.2.0 the order of creating new contracts is relevant. Writing

A a := new A()
B b := new B()

is not equivalent to

B b := new B()
A a := new A()

as the pointers to the contract storage are not the same. The order of contract creation must match the one in the EVM bytecode for the equivalence checker to succeed. This restriction might be lifted in later releases of act.

Input space equivalence

We also need to check that the EVM bytecode implementation and act specification revert at the same inputs. Since the input space of the two lists is not necessarily exhaustive, some inputs may lead to failed execution paths that are not present in the list. We therefore need to check that the input space of the two lists are the same. That is, there must not be inputs that satisfy some path condition in the first list but none the second and vice versa.

Say that the act program has the Expr representation

Success c1 r1 s1, ..., Success cn rn sn

and the the EVM bytecode has the Expr representation

Success c1' r1' s1', ..., Success cn' rn' sn'

then we need to check that c1 ∨ .. ∨ cn ⟺ c1' ∨ .. ∨ cn' that is, we require that

c1 ∨ .. ∨ cn ∧ ¬(c1' ∨ .. ∨ cn') and c1' ∨ .. ∨ cn' ∧ ¬(c1 ∨ .. ∨ cn)

are both unsatisfiable.

Exhaustiveness checks for bytecode

The hevm backend performs public interface matching between the EVM bytecode implementation and the act specification. It verifies that each contract defines the same constructor and the same set of transitions, with matching function signatures.

Rocq Backend: Proving Properties of Specifications

Table of Contents

In order to reason about the contracts and prove their properties, the Rocq backend of act shallowly embeds the act specification into the logic of the Rocq proof assistant.

For this embedding to be sound, we ensure that the storage of the contract (and the contracts reachable from it) satisfies the unique ownership invariant (see aliasing section), meaning that its storage may never contain any aliased references to other contracts. act checks this invariant automatically immediately after the type-checking phase.

A proof assistant provides tools that help to construct proofs. Rocq, in particular, is highly interactive. The user typically builds proofs step by step, with the software giving feedback as the proof progresses.

The requirements on proofs in a system like Rocq, Isabelle, or Lean are quite strict. These tools only accept proofs that are algorithmically verifiable to be valid series of applications of the system’s inference rules. This is generally stricter than what is typically expected of pen and paper proofs, which often omit tedious details in the interest of clarity and concision.

The verification of these proofs is performed in a minimal and well-audited kernel. Although occasionally bugs have been found in Rocq’s and other systems’ kernels, a proof in these systems is generally quite strong evidence of correctness.

Usage

Generate Rocq formalization: To generate the Rocq code run

act rocq --file <PATH_TO_SPEC>

against your spec, or

act rocq --json <PATH_TO_JSON>

where the JSON file has the following format

{
  "specifications" : ["<PATH_TO_SPEC>",..],
}

Note: In the current implementation the specifications must be ordered, so that any specification only depends on others earlier in the list.

Rocq Command-Line Flags

Flag	Type	Default	Description
`--file`	Path	-	Path to the act specification file (.act)
`--json`	Path	-	Path to the sources JSON file (.json)
`--solver`	`cvc5\|z3`	`cvc5`	SMT solver used during type-checking and unique ownership verification
`--smttimeout`	Integer (ms)	`20000`	Timeout for SMT queries
`--debug`	Boolean	`false`	Print verbose output during generation

Setting Up a Rocq Project

To fully use this feature you should also set up a Makefile and _RocqProject. Following the example in tests/rocq/ERC20/, the project structure should look something like this:

my-contract/
├── mycontract.act       # Your act specification
├── MyContract.v         # Generated (by act rocq)
├── _RocqProject         # Rocq project configuration
├── Makefile             # Build automation
└── Theory.v             # Your custom proofs

act's Rocq backend generates code that depends on the ActLib library, which provides foundational definitions for reasoning about EVM contracts. It should be included in your Rocq project through the configuration files, as will be shown bellow.

1. Create a `_RocqProject` file:

The _RocqProject file tells Rocq where to find dependencies and which files to compile:

-Q . MyContractDir
-Q /path/to/act/lib ActLib

/path/to/act/lib/ActLib.v
MyContract.v
Theory.v

Explanation:

-Q . MyContractDir - Maps current directory to the logical name MyContractDir
-Q /path/to/act/lib ActLib - Makes ActLib available (adjust path to your act installation)
List all .v files that should be compiled

For the ERC20 example in the act repository:

-Q . ERC20
-Q ../../../lib ActLib

../../../lib/ActLib.v
ERC20.v
Theory.v

2. Create a `Makefile`:

This Makefile automates the entire workflow from act spec to verified proofs:

.PHONY: verify
verify: RocqMakefile MyContract.v
	make -f RocqMakefile

MyContract.v: mycontract.act
	act rocq --file mycontract.act > MyContract.v

RocqMakefile: _RocqProject
	rocq makefile -f _RocqProject -o RocqMakefile

.PHONY: clean
clean:
	if [[ -f RocqMakefile ]]; then make -f RocqMakefile clean; fi
	rm -f MyContract.v RocqMakefile RocqMakefile.conf
	rm -f *.glob *.vo *.vok *.vos .*.aux

.PHONY: regenerate
regenerate: clean MyContract.v verify

Makefile Targets Explained:

make verify (or just make) - Full build pipeline:
1. Generates MyContract.v from your .act file if needed
2. Creates RocqMakefile from _RocqProject
3. Compiles all Rocq files and checks proofs
make clean - Removes all generated and compiled files:
- Generated .v file
- Compiled Rocq artifacts (.vo, .vok, .vos, .glob)
- Makefile artifacts
make regenerate - Clean rebuild from scratch

3. Write custom proofs in `Theory.v`:

Start with the basic structure:

Require Import MyContractDir.MyContract.
Require Import ActLib.ActLib.

(* Import generated definitions *)
(* MyContractName is the name of a contract in the generated MyContract file *)
Import MyContract.MyContractName

(* Prove invariants and properties about the contract *)

This structure gives access to the MyContractName module that is generated by act, corresponding to the contract with name MyContractName, inside the MyContract.v file, located in the directory mapped to MyContractDir in _RocqProject. Writing your proofs in a file separate than the one generated by act is recommended, so that the latter can be regenerated if necessary, without affecting any manual work.

4. Build and verify:

After everything is set, you can use the following commands in your proof development workflow

# Initial build (generates .v file and compiles everything)
make verify

# After modifying Theory.v, just rebuild
make -f RocqMakefile

# After modifying the .act spec, regenerate
make regenerate

Interactive Proof Development

If you are using Rocq in your editor in an interactive mode, make sure your editor links to the Rocq executables (rocqtop) from the nix shell. Alternatively you can use a local Rocq executable, if present, and make outside of the nix shell, once the act rocq command has terminated.

A Brief Introduction to Proof in Rocq

Rocq is a complex system with a steep learning curve, and while a full tutorial on programming in Rocq is out of the scope of this documentation, we can give a little taste of how things work. For a more thorough introduction, the books Software Foundations and Certified Programming With Dependent Types are both excellent. Software Foundations in particular is a great introduction for users with little experience in the fields of formal logic and proof theory.

We start by defining the type of natural numbers. There are infinitely many natural numbers, so they must be defined inductively. In fact, all type definitions are done with the Inductive command, even if they are not in fact inductive. Rocq’s Inductive is analogous to Haskell’s data and OCaml’s type (with the added power of dependent types).

We define two constructors: O, representing 0, and S, representing the successor function, which when applied to the natural number n produces the representation of the number n + 1. To give a concrete example, 3 would be represented in this encoding as S (S (S 0))) i.e 1 + (1 + (1 + 0)).

Inductive nat : Type :=
  | O
  | S (n : nat).

This is an example of a unary number representation. It can often be helpful to represent numbers this way, since the inductive nature of the definition lends itself to inductive proof techniques.

Let’s continue by defining addition over our nat type:

Fixpoint plus (n : nat) (m : nat) : nat :=
  match n with
  | O ⇒ m
  | S n' ⇒ S (plus n' m)
  end.

Here we define a recursive function (a Fixpoint) that takes two numbers n and m and returns the sum of these two numbers. The implementation is defined recursively with pattern matching. You might think of this definition as “unwrapping” each application of S from the first argument until we reach its O. Then we start wrapping the second argument in the same number of Ss.

Now we’re ready to prove something! Let’s prove that 0 + n == n:

Theorem plus_O_n :
  forall n : nat, plus O n = n.
Proof.
  intros n. simpl. reflexivity.
Qed.

We first define our Theorem and give it a name (plus_O_n). Then we define the proof goal, in the form of a dependent type. We claim that for all n, where n is an instance of our nat type, 0 + n is equal to n. Finally, we construct a proof, in the form of a series of tactics. Tactics may implement either backwards inference (transforming the goal) or forwards inference (transforming evidence).

The best way to understand the system is to run the software yourself, and play around with the various tactics. In this case the goal is simple enough; once we’ve specified that the proof will be on n (intros n), Rocq is able to simplify plus O n into n (simpl), leaving us the goal n = n. This turns out to be true by the definition of equality, and we invoke definitional equality by reflexivity (reflexivity).

More complicated proofs do not typically require proving basic facts about arithmetic, because Rocq ships a substantial standard library of useful definitions and theorems. The above example hopefully serves to illustrate the formal nature of proof in these systems. In many cases it can be surprisingly hard to convince the kernel of the correctness of a statement that seems “obviously” true.

act Export

Calling act rocq ... will generate a Rocq file that encodes the contract as a state transition system, following the formal value semantics, given and proven sound in the tech report (to be available shortly).

The generated Rocq output will contain:

type definitions for contract state.
For every case of the constructor and every transition:
- State transition relation (used for the step relation).
- Precondition predicates (additionally to the given preconditions, also requirements on integer bounds) for every storage variable, where applicable.
- Return value proposition (only for transitions).
Transition system with a step relation (and then generalised to multistep)
Predicate characterising a reachable state from any initial state.
Predicate characterising a reachable state from the initial state produced by given constructor parameters.
Definition schema for invariants*:
- Parametrized by the invariant property IP : Env -> {argument-types} -> address -> State -> Prop, where {argument-types} represents the types of the constructor's arguments. The property's arguments of types Env, {argument-types} and address refer to the environment, the arguments and the next address at the time of construction.
- Invariant predicate definition for the Initial State.
- Invariant predicate definition for the Step.
- Proof of the invariant holding in all reachable states if IP holds in the initial state and for every step.

*) Invariants are properties that hold in all reachable states of the state transition system, and can be used to prove properties about the contract.

Let us explore the generated Rocq output for the ERC20 Token contract from erc20.act.

The output will begin with importing the necessary libraries:

(* --- GENERATED BY ACT --- *)

Require Import Stdlib.ZArith.ZArith.
Require Import ActLib.ActLib.
Require Stdlib.Strings.String.

Module Str := Stdlib.Strings.String.
Open Scope Z_scope.

Then it will start a module for the token contract:

Module Token.

Record State : Set := state
{ addr : address
; BALANCE : Z
; allowance : address -> address -> Z
; balanceOf : address -> Z
; totalSupply : Z
}.

The contract will be represented as a record with the fields corresponding to the storage variables, and two additional fields: the address of the contract addr and the balance of the contract (the number of wei sent to it) BALANCE. Note that we use the type Z for integers, which is the integer type from the ZArith library bundled with Rocq; and we also use the type address for Ethereum addresses, which is also represented by Z in the ActLib.

The Actlib also defines an environment type, which is a record that represents the context in which the contract is executed. It also contains Ethereum environment variables, such as the call value (Callvalue), the caller address (Caller). The structure of the environment in Rocq is as follows:

Record Env : Set :=
  { Callvalue : Z;
    Caller : address;
    This : address;
    Origin : address;}.

Finally, a parameter of note is NextAddr, which is used in constructor and transition relations. It represents the next address to be allocated by the EVM. There are 2 instances of it in each relation, corresponding to the next address prior to and after the constructor/transition.

Next, the output contains some additional type definitions, like noAliasing and stateIntegerBounds. They are used in the conditions generated for constructors/transitions.

Inductive addressIn (STATE : State) : address -> Prop :=
| addressOf_This :
     addressIn STATE (addr STATE)
.

Inductive noAliasing (STATE : State) : Prop :=
| noAliasingC : noAliasing STATE
.

Inductive stateIntegerBounds (STATE : State) : Prop :=
| integerBoundsC :
     0 <= Token.addr STATE <= UINT_MAX 160
  -> 0 <= BALANCE STATE <= UINT_MAX 256
  -> (forall i0 i1, 0 <= allowance STATE i0 i1 <= UINT_MAX 256)
  -> (forall i0, 0 <= balanceOf STATE i0 <= UINT_MAX 256)
  -> 0 <= totalSupply STATE <= UINT_MAX 256
  -> stateIntegerBounds STATE
.

Definition nextAddrConstraint (NextAddr : address) (STATE : State) :=
  forall (p : address), addressIn STATE p -> NextAddr > p
.

Next the preconditions for the constructor are generated as follows:

Inductive constructor_conds (ENV : Env) (_totalSupply : Z) (NextAddr : address) : Prop :=
| constructor_condsC : forall
  ( H_iff0 : ((Callvalue ENV) = 0) )
  ( H_argConstraints_intBounds__totalSupply : 0 <= _totalSupply <= UINT_MAX 256 )
  ( H_CallerBound : 0 <= Caller ENV <= UINT_MAX 160 )
  ( H_OriginBound : 0 <= Origin ENV <= UINT_MAX 160 )
  ( H_ThisBound : 0 <= This ENV <= UINT_MAX 160 )
  ( H_NextAddressBound : 0 <= NextAddr <= UINT_MAX 160 )
  ( H_Caller_lt_NextAddr : Caller ENV < NextAddr )
  ( H_Origin_lt_NextAddr : Origin ENV < NextAddr )
  ( H_This_eq_NextAddr : This ENV = NextAddr ),
  constructor_conds ENV _totalSupply NextAddr

The proposition holds, when the preconditions specified in the constructor's iff block are satisfied, the integer bounds are respected, the addresses are in range, and the environment is well-formed (for instance the next address is greater than all current addresses).

Next, the Token constructor state transition of type Env -> Z -> Env * State is defined as follows:

Inductive constructor (ENV : Env) (_totalSupply : Z) (NextAddr : address)
                      : State -> address -> Prop :=
| Token_case0 : forall NextAddr1
  ( H_conds : constructor_conds ENV _totalSupply NextAddr )
  ( H_case_cond : True )
  ( H_bindings0 : NextAddr1 = NextAddr + 1 ),
  constructor ENV _totalSupply NextAddr
      (state NextAddr
      0
      (fun _binding_0 => (fun _ => 0))
      (fun _binding_0 => if ((_binding_0) =? (Caller ENV))%bool then _totalSupply else 0)
      _totalSupply)
      (NextAddr1)

The constructor relates the environment, its input arguments and the address to be allocated next, to a new state for the token contract, and the new next allocated address. The contract will be stored in the next address NextAddr and initialize the BALANCE field to 0 (as the constructor is not payable). The allowance function will be initialized to return 0 for all pairs of addresses, the balanceOf function will return the total supply for the contract creator, and the totalSupply will be set to the initial total supply.

Similarly preconditions are generated for every transition in the contract specification. For instance for the transfer transition, the preconditions are the following

Inductive transfer_conds (ENV : Env) (_value : Z) (to : address)
                         (STATE : State) (NextAddr : address) : Prop :=
| transfer_condsC : forall
  ( H_iff0 : ((Callvalue ENV) = 0) )
  ( H_iff1 : (((0 <= ((Token.balanceOf STATE) (Caller ENV)))
              /\ (((Token.balanceOf STATE) (Caller ENV)) <= (UINT_MAX 256)))
              /\ (((0 <= _value)
              /\ (_value <= (UINT_MAX 256)))
              /\ ((0 <= (((Token.balanceOf STATE) (Caller ENV)) - _value))
              /\ ((((Token.balanceOf STATE) (Caller ENV)) - _value) <= (UINT_MAX 256))))))
  ( H_iff2 : (((Caller ENV) <> to) -> (((0 <= ((Token.balanceOf STATE) to))
              /\ (((Token.balanceOf STATE) to) <= (UINT_MAX 256)))
              /\ (((0 <= _value)
              /\ (_value <= (UINT_MAX 256)))
              /\ ((0 <= (((Token.balanceOf STATE) to) + _value))
              /\ ((((Token.balanceOf STATE) to) + _value) <= (UINT_MAX 256)))))) )
  ( H_nextAddrCnstrnt_State : nextAddrConstraint NextAddr STATE )
  ( H_argConstraints_intBounds__value : 0 <= _value <= UINT_MAX 256 )
  ( H_argConstraints_intBounds_to : 0 <= to <= UINT_MAX 160 )
  ( H_CallerBound : 0 <= Caller ENV <= UINT_MAX 160 )
  ( H_OriginBound : 0 <= Origin ENV <= UINT_MAX 160 )
  ( H_ThisBound : 0 <= This ENV <= UINT_MAX 160 )
  ( H_NextAddressBound : 0 <= NextAddr <= UINT_MAX 160 )
  ( H_This_lt_NextAddr : This ENV < NextAddr )
  ( H_Caller_lt_NextAddr : Caller ENV < NextAddr )
  ( H_Origin_lt_NextAddr : Origin ENV < NextAddr )
  ( H_no_self_call : (forall (p : address), addressIn STATE p -> Caller ENV <> p) )
  ( H_no_self_origin : (forall (p : address), addressIn STATE p -> Origin ENV <> p) )
  ( H_This_eq_addState : This ENV = addr STATE ),
  transfer_conds ENV _value to STATE NextAddr

The hypotheses begin with the conditions specified in the transition's iff block. The first precondition requires that the call value is zero, as the transition is not payable. The second precondition ensures that the caller has a sufficient balance to cover the transfer amount, and the value being transferred is within the allowed range. Then the precondition ensures the case we are in. Next, the to address needs to not overflow and has to be a valid address. The environment before and after the transition must also be well-formed (for instance the next address is greater than all current addresses).

Then, a state transition is generated for every transition in the contract specification.

Additionally, for every transition, a return value predicate is generated as follows:

Inductive transfer_ret (ENV : Env) (_value : Z) (to : address)
                       (STATE : State) (NextAddr : address) : bool -> Prop :=
| transfer_case0_ret :
     transfer_conds ENV _value to STATE NextAddr
  -> ((Caller ENV) <> to)
  -> transfer_ret ENV _value to STATE NextAddr true

| transfer_case1_ret :
     transfer_conds ENV _value to STATE NextAddr
  -> ((Caller ENV) = to)
  -> transfer_ret ENV _value to STATE NextAddr true

.

The predicate holds if the preconditions hold, the case condition is satisfied, and the return value is as expected (in this case true).

Finally the state transition system is defined by the step relation and the reachable proposition. The Contract_transition is a relation on pairs of states and next-addresses, given a starting environment, and it includes one constructor for every transition of the contract. For the ERC20 Token example, the Token_transition relation has the following form:

Inductive Token_transition (ENV : Env) (STATE : State) (NextAddr : address)
                           (STATE' : State) (NextAddr' : address) : Prop :=
| transfer_Token_transition : forall (_value : Z) (to : address),
   transfer_transition ENV _value to STATE NextAddr STATE' NextAddr'
-> Token_transition ENV STATE NextAddr STATE' NextAddr'
| transferFrom_Token_transition : forall (src : address) (dst : address) (amount : Z),
   transferFrom_transition ENV src dst amount STATE NextAddr STATE' NextAddr'
-> Token_transition ENV STATE NextAddr STATE' NextAddr'
| transferFrom_Token_transition : forall (src : address) (dst : address) (amount : Z),
...

| allowance_Token_transition : forall (idx1 : address) (idx2 : address),
   allowance_transition ENV idx1 idx2 STATE NextAddr STATE' NextAddr'
-> Token_transition ENV STATE NextAddr STATE' NextAddr'

To define the reachability relation, we introduce the transition relation on pairs of states and next addreses, which includes all transitions of the system, by all of the included contracts. For the ERC20 Token contract example, the transition relation has the following form:

Inductive transition (ENV : Env) (STATE : State) (NextAddr : address) (STATE' : State) (NextAddr' : address) : Prop :=
| transition_Token :
     Token_transition ENV STATE NextAddr STATE' NextAddr'
  -> transition ENV STATE NextAddr STATE' NextAddr'

Since the Token contract does not refer to other contracts in its storage, the transition relation is essentially the same as the Token_transition relation. However, if a contract interacts with other contracts, the transition relation would need to account for those interactions as well. For instance, the Automated Market Maker contract amm.act stores two ERC20 Tokens in its storage, token0 and token1. The state transitions can thus arise from calling the Amm contract's own transitions, or from calling transitions on either of the two stored Token contracts. The transition for Amm thus includes cases for the Amm_Transition, Token_transition for token0, and Token_transition for token1 and has the following shape

Inductive transition (ENV : Env) (STATE : State) (NextAddr : address) (STATE' : State) (NextAddr' : address) : Prop :=
| transition_Amm :
     Amm_transition ENV STATE NextAddr STATE' NextAddr'
  -> transition ENV STATE NextAddr STATE' NextAddr'

| transition_token0 :
     nextAddrConstraint NextAddr STATE
  -> Token.transition ENV (token0 STATE) NextAddr (token0 STATE') NextAddr'
  -> ...
  -> transition ENV STATE NextAddr STATE' NextAddr'

| transition_token1 :
     nextAddrConstraint NextAddr STATE
  -> Token.transition ENV (token1 STATE) NextAddr (token1 STATE') NextAddr'
  -> ...
  -> transition ENV STATE NextAddr STATE' NextAddr'

With the transition relation defined, we can now define the step relation on states, where the environments are also bound by an exists quantifier

Definition step (STATE : State) (STATE' : State) :=
exists (ENV : Env) (NextAddr : address) (NextAddr' : address), transition ENV STATE NextAddr STATE' NextAddr'.

and the reachable proposition, which states that a state is reachable from another state through a series of steps.

Definition reachable (STATE : State) :=
exists STATE', init STATE' /\ multistep STATE' STATE.

Finally, a schema for proving invariant properties on reachable states is defined. Parametric to the invariant property IP : Env -> {argument-types} -> State -> Prop, if we know that invariant property holds at the initial state

Definition invariantInit (IP : Env -> Z -> address -> State -> Prop) :=
  forall(ENV : Env) (_totalSupply : Z) (NextAddr : address) (STATE : State) (NextAddr' : address),
     constructor ENV _totalSupply NextAddr STATE NextAddr'
  -> IP ENV _totalSupply NextAddr STATE

and the step

Definition invariantStep (IP : Env -> Z -> address -> State -> Prop) :=
  forall(ENV : Env) (_totalSupply : Z) (NextAddr : address) (STATE : State) (STATE' : State),
     constructor_conds ENV _totalSupply NextAddr
  -> step STATE STATE'
  -> IP ENV _totalSupply NextAddr STATE
  -> IP ENV _totalSupply NextAddr STATE'

the generated output will contain a proof, that the invariant property holds at all reachable states:

Lemma invariantReachable :
  forall (ENV : Env) 
         (_totalSupply : Z) 
         (STATE : State) 
         (IP : Env -> Z -> State -> Prop) 
         (HIPinvInit : invariantInit IP) 
         (HIPinvStep : invariantStep IP),
     reachableFromInit ENV _totalSupply (STATE : State)
  -> IP ENV _totalSupply STATE.

You are then welcome to use this lemma in the proof of your properties.

Proving properties using the act Rocq export

Now that the state transition system is exported automatically, one can use it to prove properties about the contract. In the Theory.v you can find a proof of the sum of balances invariant, stating that at any possible reachable state the sum of balances is the same, and equal to the total supply:

Theorem Token_sumOfBalances_eq_totalSupply : forall STATE,
    reachable STATE ->
    balanceOf_sum STATE = totalSupply STATE.

The balanceOf_sum function above calculates the sum of the balanceOf STATE function, for all 256 bit addresses by having maintained a MaxAddress field.

Definition MAX_ADDRESS := UINT_MAX 160.

Fixpoint balanceOf_sum' (balanceOf : address -> Z) (n : nat) (acc : Z) : Z :=
    match n with
    | O => balanceOf 0 + acc
    | S n => balanceOf_sum' balanceOf n (acc + balanceOf (Z.of_nat (S n)))
    end.

Definition balanceOf_sum (STATE : State) :=
  balanceOf_sum' (balanceOf STATE) (Z.to_nat MAX_ADDRESS) 0.

The (manual) proof of the theorem then completes the pipeline.

The act Book