We have just published the first release of the Act specification language!
Act is a formal specification language, designed to allow for the construction of an exhaustive, mathematically rigorous description of a smart contract system. Act allows diverse toolchains to interoperate on a single specification, with each generating and exchanging different kinds of knowledge. It has a builtin analysis engine that can automatically prove properties about the specification itself, as well as an integrated symbolic execution engine (based on hevm) that can prove equivalence between a specification and a given bytecode object. Finally, specifications can be exported into the Coq proof assistant, allowing for the verification of properties of almost arbitrary complexity, all with a proof chain right down to the bytecode level.
While a lot of work still remains to be done before Act can be used to verify properties of
realistic contracts, we’re excited to share what we have, and invite feedback and ideas from the
community. If you want to come chat about Act, we have a matrix
channel, or you can also find us in #formalmethods
in the ethereum r&d discord.
Contents
 Motivation & Design Philosophy
 Installation
 Language
 Bytecode Level Proof
 Automated Analysis
 Coq Export
 Future Work
 Final Remarks
Motivation & Design Philosophy
Smart contract development is difficult. The code we write must secure large sums of money in an extremely adversarial environment, and even a single oversight can easily result in the loss of millions of dollars. In this context being able to define and prove the correctness of key security properties is enormously valuable. Act grew out of the verification work carried out for multicollateral Dai and Uniswap v2, and is a groundup rewrite in Haskell of the prototype specification language developed as a part of that process, incorporating many of the lessons learned along the way.
The following are some key design goals:
Ease of Refinement
Proving properties directly against EVM bytecode is difficult and expensive. Compiler output contains much extraneous detail (e.g. overflow checks, bitmasks in storage access routines, abi encoding / decoding, function selector dispatch logic) that is not generally relevant when proving the correctness of a high level property, but that must still be taken into account. A widely used and powerful technique is to use a process of refinement, where the properties of interest are proven against a high level specification that abstracts much of this detail away. A separate proof can then be carried out to show that a given bytecode object faithfully implements the abstract specification. The SeL4 microkernel is a notable real world application of this technique, where properties are proven against a high level spec in the Isabelle proof assistant, and then successive refinement steps are used to prove these properties down to the binary level ([1][2])
Act is a framework designed to allow for easy refinement. We want to make it as easy as possible for development teams to define a high level specification, which can then either be used “upwards” to prove higher level properties or “downwards” to demonstrate that an implementation in EVM bytecode conforms to the spec.
Modularity
Different tools and techniques for formal verification have different strengths and weaknesses, and with Act we want to make it as easy as possible to combine tools and share knowledge between them. For example an SMT based analysis engine will usually be significantly faster and more convenient than manually constructing a proof in a proof assistant like Coq, but the latter can prove the correctness of statements that would be impossible to even state in the language accepted by an SMT solver.
With Act as an intermediate language, we can combine and share knowledge between many different tools and frameworks in a way that allows us to leverage their different strengths where it makes most sense.
Expressiveness
Much of the work that we have released to date has been focused on making it easy for smart contract developers to prove statements in the language that they are most familiar with (e.g. the SMTChecker built directly into solc, or the integration of symbolic execution into the dstest unit test framework). While this makes it easy to get fast results, and allows developers to quickly build confidence in their implementation, there are limits to the kind of properties that can be expressed in such a framework. For example, some properties may require a greater numeric range than the 256 bit integers available in the EVM allow, while others may require temporal operators or quantifiers, neither of which are expressible in a language like Solidity.
With Act we hope to provide a language expressive enough to natively express a wide range of properties, and combined with its ability to export the specification into the Coq proof assistant, we believe that it should be possible to express almost any property of a given specification.
Installation
Act can currently be installed via nix
with the
following commands:
# configure nix to use prebuilt binaries for hevm (optional)
nixshell p cachix command "cachix add dapp"
# install act v0.1
nixenv iA act if https://api.github.com/repos/ethereum/act/tarball/v0.1
If you want to play around with the examples in this post, you can check out the
actexamples repo. A call to nixshell
from the repository
root will drop you into an environment with all required tools installed and configured.
Language
At a very high level Act is a kind of mathy english over the EVM, where contracts are defined as a set
of pure functions taking a given EVM state (i.e. storage & blockchain context) and some calldata
and producing a new EVM state ((EVM, Calldata) > EVM
).
A specification of a contract written in Act consists of a constructor and a set of behaviours:

The constructor specification defines the structure of the contract’s state, the initial value of the state, and a list of invariants that the contract should satisfy.

Each behaviour specification determines how a contract method updates the state, the method’s return value (if any), and any conditions that must be satisfied in order for the state update to be applied.
Alternatively, they can be thought of as an initial state and a set of state transitions, determining an inductively defined state transition system.
A more detailed high level language reference can be found in the documentation.
Types
The types of Act consist of three basic primitives: Integers, Booleans and Bytestrings. Integers are
unbounded, with true integer operations. However, as our integer expressions will often represent
words in the EVM, we allow ourselves a slight abuse of notation and denote by uintN
/intN
integers
together with the constraint that the value fits into a uintN
/intN
. If any
operation could over or underflow this bound, the constraint will be unfulfilled
and the specification will fail to prove.
Using conventional ABI types for typing also allows us to specify function signatures in a concise way. As an example, consider this specification of a trivial contract that adds two numbers and stores the result on chain:
constructor of Add 
interface constructor() 
creates 
uint result := 0 
behaviour add of Add 
interface add(uint x, uint y) 
iff in range uint 
x + y 
storage 
result => x + y 
returns x + y 
Expressed in English and math, this specification would read:
The contract Add
has a single state variable, named result
, which is an integer such that 0 <= result < 2^256
.
Given any pair of integers x
and y
, s.t. 0 <= x < 2^256
and 0 <= y < 2^256
, an ABI encoded
call to the contract Add
with the signature add(uint256,uint256)
, with its respective arguments named x
and y
, will:
 store
x + y
inresult
and returnx + y
if0 <= x + y < 2^256
 revert otherwise
Bytecode Level Proof
Act leverages the symbolic execution engine in hevm to provide a backend that can prove equivalence between a contract specification and an implementation of that specification in EVM.
Two claims are generated for each behaviour, Pass
and Fail
. The Pass
claim states
that if all preconditions in the iff
block are true, then all executions will succeed, storage
will be updated according to the storage
block, and the specified return value will, in fact, be returned. The
Fail
claim states that should any of the preconditions be false, all executions will revert.
In both cases we begin the proof by constraining calldata to be of the form specified in the behaviours’
interface
blocks, as well as making the relevant assumptions
depending on whether the claim is Pass
or Fail
, and then symbolically executing
the bytecode object with storage held to be completely abstract.
This produces a tree of potential executions where each node represents a potential branching point, and each leaf represents a possible final state of the contract after the execution of a single call.
In the case of a Fail
claim, we can then check that each leaf represents a state in which execution
has reverted, while for a Pass
claim we can check that storage has been updated as expected, and that the contents of
the return buffer matches what was specified in the behaviour’s returns
block.
As an example, consider the following contract:
contract Simple {
uint val;
function set(uint x) external payable returns (uint) {
require(x > 100);
val = x;
return x;
}
}
We can represent this in Act as:
constructor of Simple 
interface constructor() 
creates 
uint val := 0 
behaviour set of Simple 
interface set(uint x) 
iff 
x > 100 
storage 
val => x 
returns x 
Act needs to have access to the storage layout metadata output by solc to compute the index in
storage for each variable mentioned in the spec, so we need to pass a solc output json when trying
to prove equivalence. In the examples repo you can run dapp
build
and then act hevm spec src/simple.act soljson out/dapp.sol.json
to attempt to prove
equivalence of the spec and the runtime bytecode:
< act hevm spec src/simple.act soljson out/dapp.sol.json
checking postcondition...
Q.E.D.
Successfully proved set(Pass), 2 cases.
checking postcondition...
Q.E.D.
Successfully proved set(Fail), 2 cases.
==== SUCCESS ====
All behaviours implemented as specified ∎.
If we try to prove equivalence of the spec and a faulty implementation like the one below:
contract Simple {
uint val;
function set(uint x) external payable returns (uint) {
require(x > 100);
if (x == 2000) {
val = x + 1;
} else {
val = x;
}
return x;
}
}
Then Act will give us a counterexample showing a case where the implementation differs from the specification:
< act hevm spec src/simple.act soljson out/dapp.sol.json
checking postcondition...
Calldata:
0x60fe47b100000000000000000000000000000000000000000000000000000000000007d0
Caller:
0x0000000000000000000000000000000000000000
Callvalue:
0
Failed to prove set(Pass)
checking postcondition...
Q.E.D.
Successfully proved set(Fail), 2 cases.
==== FAILURE ====
1 out of 2 claims unproven:
1 Failed to prove set(Pass)
Automated Analysis
Act has an integrated analysis engine that is currently able to automatically prove two kinds of properties:
 Behaviour level postconditions (i.e. properties that are always true in every possible poststate of a single behaviour)
 Contract level invariants (i.e. properties that are true in all possible poststates of the constructor, as well as in all possible pre and poststates of any behaviours)
Postcondition syntax
Postconditions are defined in an optional ensures
block of each behaviour
. All references to storage
in an ensures
block must specify whether they talk about the variable’s value in the pre or
the poststate, by using pre(x)
or post(x)
.
An example:
behaviour f of F 
interface f(uint z) 
storage 
y => z 
x => 30 * z 
ensures 
post(x) == 30 * post(y) 
Invariant syntax
Invariants are defined in the invariants
block in the constructor specification. Each invariant is
a predicate that should hold between the execution of any state transitions. Invariant predicates have access to
the constructor’s calldata. Note that since invariant predicates are defined over a single abstract
contract state (as opposed to predicates in ensures
blocks which have access to a pair of states),
it is neither necessary nor allowed to disambiguate storage references using pre(x)
and post(x)
in invariant predicates.
An example:
constructor of C 
interface constructor(uint _x, uint _y, uint _z) 
iff _x * _y == _z 
creates 
uint x := _x 
uint y := _y 
invariants 
x * y == _z 
Implementation
In order to discharge these proofs, we construct an SMTbased encoding of each behaviour in the spec, and then dispatch queries based on this encoding to an SMT solver (currently z3 and cvc4 are supported). An SMT solver is a system that takes a collection of constraints (a query), where each constraint is a statement in first order logic, and determines whether there exists an assignment of values to the abstract variables in the query such that all constraints are satisfied.
As an example, we could encode the query “for all integers x and y, is there an assignment of values to x and y such that x + y == 13 and y  7 == x” in the widely supported smtlib language as follows:
(declareconst x Int)
(declareconst y Int)
(assert (= (+ x y) 13))
(assert (= ( y 7) x))
(checksat)
(getmodel)
When passed to an smt solver (e.g. z3), this would return:
sat
(
(definefun x () Int
3)
(definefun y () Int
10)
)
Where sat
means that a satisfying assignment does exist, and the remaining output gives us the
values of the assignment found by the solver (x == 3
and y == 10
).
SMTbased program verification is often done by contradiction: instead of asking the solver to directly provide a proof for a given statement, we instead ask it to find an example where the statement is untrue, and if none are found, we can infer the truth of the original statement. As an example, if we wished to prove distributivity for integer arithmetic, we would encode the query as follows:
(declareconst x Int)
(declareconst y Int)
(declareconst z Int)
(assert (not
(= (* x (+ y z))
(+ (* x y) (* x z)))))
(checksat)
and when run in a solver, we would get unsat
as a result, meaning that there are no possible
assignments to the variables, x
, y
and z
where distributivity does not hold.
Postcondition Encoding
For the postcondition claims, we tell the solver to assume the truth of all preconditions, and that
all storage updates have occurred as defined in the storage
block, and then ask it to find an
assignment for the symbolic variables in the spec (calldata, environment, and storage) that violates
the postcondition. If none can be found, we have a proof that the postcondition always holds.
Invariant Encoding
Invariant claims are proved inductively. For the base case, we ask the solver to once again assume preconditions and storage rewrites, and then to find an assignment for the variables in the constructor that would result in a violation of the invariant predicate over the poststate. If none can be found, we have a proof of the base case.
For the inductive step, we construct a query for each behaviour that assumes preconditions and storage rewrites, and additionally assumes that the invariant claim is true over the prestate. We then ask the solver to find an assignment for the variables in the behaviour that would result in a violation of the invariant predicate over the storage post state. If none can be found, we have an inductive proof that the invariant must hold over all possible contract states.
Proving The Constant Product Invariant
As a larger and practical example, let’s consider the following specification of a highly simplified Uniswapstyle constant product automatic market maker. For the purposes of this example we focus only on the core logic, and ignore e.g. interactions with the underlying tokens.
The Amm
has two state variables representing its underlying token balances, reserve0
and
reserve1
. These are initialized to 1000
units each upon creation.
We define a single invariant, that the product of the two reserves should never decrease. This is an important safety property – if it is violated, an attacker is able to execute a sequence of trades that can drain all funds from the exchange.
behaviour init of Amm 
interface constructor() 
creates 
uint256 reserve0 := 1000 
uint256 reserve1 := 1000 
invariants 
1000 * 1000 <= reserve0 * reserve1 
Next, we define the two swap
methods, that allow a user to exchange tokens. These methods take an
amount (amt
) of input reserves, and the Amm
will adjust the size of the other reserve according
to the x * y == k
constant product formula.
behaviour swap0 of Amm 
interface swap0(uint256 amt) 
iff in range uint256 
reserve0 + amt 
storage 
reserve0 => reserve0 + amt 
reserve1 => (reserve0 * reserve1) / (reserve0 + amt) 
behaviour swap1 of Amm 
interface swap1(uint256 amt) 
iff in range uint256 
reserve1 + amt 
storage 
reserve0 => (reserve0 * reserve1) / (reserve1 + amt) 
reserve1 => reserve1 + amt 
If we run act prove
against the above spec, we find that there is in fact an error:
> act prove file src/ammbroken.act
Invariants:
((1000 * 1000) <= (Amm.reserve0 * Amm.reserve1)) of Amm violated:
counterexample:
calldata:
swap0(amt = 1)
storage:
prestate:
Amm.reserve0 = 2
Amm.reserve1 = 500000
poststate:
Amm.reserve0 = 3
Amm.reserve1 = 333333
counterexample:
calldata:
swap1(amt = 1)
storage:
prestate:
Amm.reserve1 = 2
Amm.reserve0 = 500000
poststate:
Amm.reserve1 = 3
Amm.reserve0 = 333333
If the Amm
is in the state reserve0 == 2
and reserve1 == 500,000
, and swap0
is called with amt
== 1
, the final state of the Amm
will be reserve0 == 3
and reserve1 == 333,333
. The same is
true with swap1
if the amounts for reserve0
and reserve1
are switched. In these cases 3 *
333,333
is 999,999
, meaning that the product of the reserves has decreased slightly due to
imprecision introduced by the EVM’s flooring division.
A safe specification for the swap
methods is as follows. Notice the extra + 1
added to the output
reserve in both cases. With this implementation, the rounding error is now in favor of the pool
instead of the trader, and the contract is now safe against this particular attack.
behaviour swap0 of Amm 
interface swap0(uint256 amt) 
iff in range uint256 
reserve0 + amt 
storage 
reserve0 => reserve0 + amt 
reserve1 => (reserve0 * reserve1) / (reserve0 + amt) + 1 
behaviour swap1 of Amm 
interface swap1(uint256 amt) 
iff in range uint256 
reserve1 + amt 
storage 
reserve0 => (reserve0 * reserve1) / (reserve1 + amt) + 1 
reserve1 => reserve1 + amt 
If we again run act prove
against the fixed specification, we see that the invariant holds for all
possible executions of the contract:
> act prove file src/ammfixed.act
Invariants:
((1000 * 1000) <= (Amm.reserve0 * Amm.reserve1)) of Amm holds ∎
Underpowered Invariants
Due to the inductive nature of the proof, there are some true invariants that the SMT backend is unable to prove. For example, consider the following state machine:
constructor of C 
interface constructor() 
creates 
uint x := 0 
invariants 
x < 9 
behaviour f of C 
interface f() 
case x == 0: 
storage 
x => 1 
behaviour g of C 
interface g() 
case x == 1: 
storage 
x => 2 
behaviour h of C 
interface h() 
case x == 7: 
storage 
x => 100 
The contract C
can never be in a state where x == 7
and so the write of 100
to x
in j()
can
never occur, however if we run act prove
against this specification, this exact case (x == 7
) is
found as a counterexample:
> act prove file src/underpowered.act
Invariants:
(C.x < 9) of C violated:
counterexample:
calldata:
h()
storage:
prestate:
C.x = 7
poststate:
C.x = 100
This is due to the inductive nature of the proof: Act checks that the invariant holds after running the constructor, and then for each method assumes that the invariant holds over the pre state and checks that the invariant holds over the post state.
In the case above, the invariant states that x < 9
, and if this is assumed as a precondition, then
the x == 7
branch in h()
is still reachable.
We can fix this by strengthening the invariant to make the x == 7
branch unreachable. Specifically, the
weakest invariant that does hold over the full transition system (while remaining on the same form as the
original) is x < 7
. The strongest is x < 3
.
Coq Export
While the automated proof backend is quite capable, there are still many properties that are too challenging for automated tools. For this reason Act allows exporting the transition system to the Coq proof assistant, where manual proofs of arbitrary complexity can be carried out.
A proof assistant provides tools that help to construct proofs. Coq, 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 Coq, 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 wellaudited kernel. Although occasionally bugs have been found in Coq’s and other systems’ kernels, a proof in these systems is generally quite strong evidence of correctness.
A Brief Introduction to Proof in Coq
Coq is a complex system with a steep learning curve, and while a full tutorial on programming in Coq is out of the scope of this blog post, 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.
The Coq system is composed of three languages: a minimal functional programming language (Gallina), a tactics language for proof construction (Ltac), and a “vernacular” for interaction with the kernel. Let’s start with the very basics: defining the natural numbers and proving something about addition.
We start by defining the type of natural numbers. There are infinitely many natural numbers, so of
course they must be defined inductively. In fact, all type definitions are done with the Inductive
vernacular command, even if they are not in fact inductive. Coq’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
, which when applied to the natural number
n
produces the representation of the number n + 1
(S
as in “successor”). 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 S
s.
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
, Coq is able to simplify plus O n
into n
, leaving us the goal n = n
. This turns out
to be true by the definition of equality, and we invoke definitional equality by reflexivity
.
More complicated proofs do not typically require proving basic facts about arithmetic, because Coq 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
Let’s take a look at using Coq to prove properties about a specification that is too difficult for
the SMT backend. The following defines a contract that implements exponentiation via repeated
multiplication. The contract is initialized with a base (b
) and an exponent (e
). exp()
can
then be repeatedly called until e
is 1
, and the result can then be read from the storage
variable r
. While obviously artificial, this example does highlight a key shortcoming of the SMT
based analysis: exponentiation with a symbolic exponent is simply inexpressible in the smtlib
language used by all major SMT solvers, and so any contract making use of exponentiation where the
exponent is a variable of some kind (e.g. calldata, storage) will be impossible to verify using SMT.
Coq has no such restrictions, and we can export the spec below and prove correctness there.
constructor of Exponent 
interface constructor(uint _b, uint _e) 
iff 
_e > 0 
creates 
uint b := _b 
uint e := _e 
uint r := _b 
behaviour exp of Exponent 
interface exp() 
iff 
e > 1 
iff in range uint 
r * b 
e  1 
storage 
r => r * b 
e => e  1 
b 
You can export the spec into Coq by running make Exponent.v
in the src/exponent
directory of the
examples repo. This will create a file called Exponent.v
which contains a model of the above Act specification in Coq:
(*  GENERATED BY ACT  *)
Require Import Coq.ZArith.ZArith.
Require Import ActLib.ActLib.
Require Coq.Strings.String.
Module Str := Coq.Strings.String.
Open Scope Z_scope.
Record State : Set := state
{ b : Z
; e : Z
; r : Z
}.
Definition exp0 (STATE : State) :=
state (b STATE) (((e STATE)  1)) (((r STATE) * (b STATE))).
Definition Exponent0 (_b : Z) (_e : Z) :=
state (_b) (_e) (_b).
Inductive reachable : State > State > Prop :=
 Exponent0_base : forall (_b : Z) (_e : Z),
(_e > 0)
> ((0 <= _b) /\ (_b <= (UINT_MAX 256)))
> ((0 <= _e) /\ (_e <= (UINT_MAX 256)))
> reachable (Exponent0 _b _e) (Exponent0 _b _e)
 exp0_step : forall (BASE STATE : State),
reachable BASE STATE
> ((e STATE) > 1)
> ((0 <= ((r STATE) * (b STATE))) /\ (((r STATE) * (b STATE)) <= (UINT_MAX 256)))
> ((0 <= ((e STATE)  1)) /\ (((e STATE)  1) <= (UINT_MAX 256)))
> ((0 <= (r STATE)) /\ ((r STATE) <= (UINT_MAX 256)))
> ((0 <= (e STATE)) /\ ((e STATE) <= (UINT_MAX 256)))
> ((0 <= (b STATE)) /\ ((b STATE) <= (UINT_MAX 256)))
> reachable BASE (exp0 STATE )
.
Let’s break this down a bit. We have a definition of contract storage State
, which consists of
three variables b
, e
and r
, all of type Z
. Z
is an integer type using a binary encoding
from the ZArith
library bundled with
Coq.
Next we have exp0
, which defines how the state is updated by the exp
behaviour, and Exponent0
which defines how the state variables are initialized by the constructor arguments.
Finally we have an Inductive Proposition
reachable
that defines the conditions under which a certain state is reachable from another. There
are two parts to this definition:
Exponent0_base
: states that given two integers_b
and_e
, the initial state is reachable from the initial state if_e
and_b
are in the range of auint256
and_e
is greater than0
.exp0_step
: states that for a pair of statesBASE
andSTATE
,exp0 STATE
(i.e. the result of callingexp()
against an arbitrary contract state) is reachable fromBASE
ifSTATE
is reachable fromBASE
, all the state variables inSTATE
(e
,b
,r
) are within the range of auint256
, the result of the calculationsr * b
ande  1
are within the range of auint256
, ande
is greater than1
.
This gives us a pair of inference rules that we can
use to prove facts about the set of reachable states defined by the specification for the Exponent
contract.
An example of such a proof is contained in the Theory.v
file in the src/exponent
directory of
the examples repo. The core fact that we wish to prove is
that when e
is 1
, r
is equal to b ^ e
. This can be expressed in Coq as:
forall (base, s : State),
reachable base s > e s = 1 > r s = (b base) ^ (e base).
Expressed more verbosely: for all states base
and s
, if s
is reachable from base
, and the
value of e
in s
is 1
, then the result variable r
in s
is equal to b
from base
raised to the power of e
from base
.
The full proof is reproduced below. While an explanation of each step is out of scope for this post (and is anyway best made with the proof loaded into an interactive instance of the Coq prover like proof general or CoqIde), we can give a broad strokes overview.
We must first define a helper fact pow_pred
which simply states that given two integers a
and e
, if e
is greater than 0
then a * a ^ (e  1)
is equal to a ^ e
. This fact is
needed in the later steps of the proof. The next step is to define a loop
invariant for exp()
(i.e. a fact that is true
before and after each loop iteration). This is the Lemma invariant
, which states that for every
state s
reachable from base
, r * b ^ (e  1)
over s
is equal to b ^ e
over base
.
Intuitively, this states that the partial result calculated so far (r
), multiplied by the remaining
portion of the input calculation b ^ (e  1)
is equal to the final expected result. Finally, given
these two intermediate facts, we can discharge a proof for the correctness of Exponent
as defined
above.
Require Import Exponent.Exponent.
Require Import ActLib.ActLib.
Require Import Coq.ZArith.ZArith.
Open Scope Z_scope.
Lemma pow_pred : forall a e, 0 < e > a * a ^ (Z.pred e) = a ^ e.
Proof.
intros.
apply eq_sym.
replace (a ^ e) with (a ^ (Z.succ (Z.pred e))).
 apply Z.pow_succ_r.
apply Zlt_0_le_0_pred.
assumption.
 rewrite (Z.succ_pred e).
reflexivity.
Qed.
Lemma invariant : forall base s,
reachable base s > (r s) * (b s) ^ ((e s)  1) = (b base) ^ (e base).
Proof.
intros base s H. induction H.
 simpl.
rewrite Z.sub_1_r.
apply pow_pred.
apply Z.gt_lt.
assumption.
 simpl.
rewrite < IHreachable.
rewrite Z.sub_1_r.
rewrite < (pow_pred (b STATE) (e STATE  1)).
+ rewrite Z.mul_assoc. reflexivity.
+ apply Z.gt_lt in H0.
apply (proj1 (Z.sub_lt_mono_r 1 (e STATE) 1)).
assumption.
Qed.
Theorem exp_correct : forall base s,
reachable base s > e s = 1 > r s = (b base) ^ (e base).
Proof.
intros base s H He.
apply invariant in H.
rewrite He in H. simpl in H.
rewrite (Z.mul_1_r (r s)) in H.
assumption.
Qed. Check exp_correct.
While this may seem like quite a lot of work to prove what looks like a pretty simple and obvious fact it is worth noting two things:
 A proof of this property is beyond the reach of any automated tool available today.
 Our mind is full of hidden assumptions, and facts that may seem obvious are not always so. This is not the case for the Coq proof kernel, and once we have convinced it that something is true, we can be very sure that it really is.
Future Work
Automated Spec Generation
Act is designed to be simple and explicit. While this supports automated analysis based on the Act specifications, it does mean that writing specifications by hand often involves quite some boilerplate. In many cases we are mostly interested in whether a given bytecode object satisfies some high level properties, and keeping both the implementation and specification in sync can introduce unwanted overhead to the development process.
For this reason we intend to build an automated spec generation engine into hevm that will utilise the symbolic execution engine to produce an exhaustive description of all possible execution paths as a set of Act specifications. This should allow for fast iteration on the implementation, while keeping the barrier low to at any time performing highlevel analyses using Coq or the Act SMT backend.
There are some additional benefits to this approach. The current symbolic execution backend represents our first attempt at a bytecode level proof engine for Act. Unfortunately while building this out we encountered a fundamental issue: while Act specs are expressed in terms of unbounded integers, the symbolic execution engine in hevm uses bitvectors. This means that checking equivalence between a given bytecode object and a set of Act specs requires conversions from integers to bitvectors. While this is tractable for simple specs, it quickly overwhelms the SMT solver for any nontrivial contract (including any safe arithmetic!).
An automated spec generation engine would allow us to sidestep this issue; since the specs would be
generated directly from the bytecode they are correct by construction, so it would be unnecessary
to prove equivalence between bytecode and specs. Even in the case where specs
have been written by hand, we would still only need to prove equivalence between two sets of specs
(both of which are written in terms of Integers), once again allowing us to avoid the troublesome
bv_to_int
and int_to_bv
SMT operations.
Automated Checks of Spec Integrity
There are currently many specs that typecheck but are still malformed and would invalidate the proofs derived from them. We intend to add automated analysis passes to detect issues of this kind. At the moment we currently have the following planned:
 Arithmetic overflow detection (#109)
 Case consistency checks (#110)
 Collisions in mapping assignments (#111)
Support for Dynamic / Compound Types
While we have some support at the syntax level for specifications involving dynamic types (e.g. string
or bytes
), the various proof backends do not currently support proofs involving these types.
We also intend to add support for compound types (e.g. array / struct / tuple) to the language and its proof backends.
Multi Contract Specifications
Similarly to dynamic and compound types, while syntax does exist that allows for specification of multi contract systems, these features are not well supported in the various analysis backends.
Rounding Error Analysis
Understanding the impact of rounding errors in a smart contract is a critical task for secure
development. As we saw in the AMM
example above, a numeric error introduced by precision loss can
result in unexpected violations of important security properties.
There are generally two properties of rounding errors which are of interest:
 The direction of the rounding error (who loses out)
 The size of the rounding error (by how much do they lose)
We intend to allow users to specify properties relating to rounding by introducing a new operator
(e.g. exact
, or toReal
), which would indicate that the numeric expression contained within
should be expressed in various backends using Reals instead of Ints. This would for example allow
for properties that assert statements about the size and direction of the difference between the
result of the calculation over the real numbers and its rounded result when expressed over the
integers.
For an example of such an analysis performed manually, see the Uniswap v1 model produced by Runtime Verification.
Calls Into Unknown Code
Real world smart contracts must often make calls into unknown code, whether for simple tasks like an ether or token transfer, or for more complex actions (e.g. delegation of control for a flash loan). Each time they do so, they pass control to potentially malicious code that can make arbitrary modifications to the execution context, something that obviously has deep implications for the security of the calling contract. If we wish to prove security properties about realistic smart contracts with Act, we must therefore be able to specify behaviour that includes such calls.
We intend to introduce language constructs and verification routines which will allow specifying and proving properties of such contracts. For more information, we have an issue with early ideas.
Loops and Loop Invariants
Although generally inadvisable, loops are sometimes unavoidable when developing smart contracts (e.g. in numeric routines). We intend to introduce syntax and verification extensions which allow for specification and proving of loop invariants.
For those interested, we have some early thoughts and discussion on the specifics of how to encode loop invariants.
Economic Analysis
Act could be extended with a backend that exports to – possibly even integrates with – an agentbased modelling framework, to allow for complex economic analysis. We believe that Act has some unique advantages here. Simulation could be carried out against the Act expressions (which are generally significantly simpler than the EVM that they model), allowing for fast execution, while still maintaining a formal guarantee that the simulation accurately models the deployed implementation.
Final Remarks
We believe that tools like Act are essential for building high trust smart contract systems, particularly as their scale and complexity increases.
We hope that you’re as excited about this work as we are, and would love to hear your feedback and thoughts on the ideas presented here. Contributions, bug reports and questions are always very welcome in github, or you can always reach us on the chat channels mentioned in the introduction.