Formal Verification Blog

The SMTChecker is a formal verification module inside the Solidity compiler. Historically it has been complicated to run the SMTChecker on your own contracts, since you had to compile the compiler with an SMT/Horn solver, usually z3. We have been working on different solutions to this, and nowadays it is quite easy to run it. The Solidity compiler ships binaries targeting 4 different systems, with different SMTChecker support: soljson.js, a WebAssembly binary that comes with z3. solc-macos, an OSX binary... [Read More]

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 built-in analysis engine that can automatically prove properties about the specification itself, as well as an integrated symbolic execution engine (based on hevm)... [Read More]

This is a small update on the things we have been working on and what we would like to achieve until the middle of the year. Act The current focus for Act is the 0.1 release, and we are almost there. This will be Act’s first release including: Support to value types, pre and post conditions, contract invariants, storage updates. SMT backend to prove contract invariants and post conditions. Inductive proofs or Pretty printed counterexamples. hevm integration to prove that... [Read More]

The SMTChecker, a formal verification module built-in the Solidity compiler, received a lot of improvements in 2020. Many improvements are related to Solidity’s language features, such as structs, ABI, hash and math functions, and other important features that were unsupported. When running the tool, the user now has more control and is able to set a timeout per query and choose engines separately between BMC and CHC. The CHC engine encodes Solidity code as Constrained Horn Clauses and is often... [Read More]

The latest release of hevm incorporates the recently introduced symbolic execution features into its unit testing framework. This lets smart contract developers formulate and prove properties in Solidity using the dapp development framework. Formally verifying properties should now be no harder than writing a property based test. In fact, it uses almost the exact same syntax! As an example, the following is a proof of the distributive property for EVM addition and multiplication: function prove_distributivity(uint x, uint y, uint z)... [Read More]

The latest release of hevm introduces symbolic execution features which can be used for checking smart contracts for correctness, step through the execution space of live contracts, or prove equivalence between them. In this tutorial we will show how to use the new capabilities of hevm, and discuss some of its unique features as a symbolic execution engine. Table of Contents About hevm Symbolic Execution and Formal Verification How does it work? Installation Using hevm symbolic Executing against live contracts... [Read More]