FV Team Quarterly Update

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]

Automated Synthesis of External Unknown Functions

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]

Symbolic Execution With ds-test

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]

Symbolic execution for hevm

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]