# Formal Verification: Why and How

Jan 11 · 5 min read

Smart contract’s security is still a crucial challenge in the Ethereum Ecosystem. In fact, since code is law once a smart contract gets exploited, there is no way back. This is important especially if a contract is constructed to manage with large quantities of capital. All of us remember the Parity multi-sig wallet case where 300 million dollars got lost because someone killed one of the main components (Library contract) by mistake. Therefore, debugging smart contracts must be a duty of extreme importance and should be done extremely carefully, thus we need a way to be sure at almost 100% that what’s is written in a solidity smart contract works as expected.

Here is How Formal verification comes to play: What if instead of testing our smart contracts using our own convictions as humans beings, we instead use mathematically generated proofs?

# Here is How:

The core of formal verification is the K Framework.

The K Framework is nothing more than:

a rewrite-based executable semantic framework in which programming languages, type systems and formal analysis tools can be defined using configurations, computations and rules.

In simpler words, K Framework is a language specifically made for defining semantics. Semantics describes the behaviour of computer programs. For example, when we say that a construction x++ for x that is uint256 means that a program in Solidity executing it will always increase the value of x by 1, except for one value x = 2²⁵⁶–1:

Thanks to the K Framework we can write our specifications for our smart contract. Specifications are the set of rules that our smart contract has to follow in order to function correctly.

After our specifications are done we are verifying them using the Z3 Theorem Prover. Z3 is a high-performance theorem prover whose job, in this case, is to verify whether for any input a determined condition is respected. If we have written our specifications and smart contracts correctly then the verification will be successful and the proof will be Accepted.

Here is the workflow:

But How can we accomplish that?

In order to formally verify a contract, you have to verify its semantic

Let’s consider the following contract:

What this contract does is allowing to execute `set` to change `value`and then lock that information by setting `isSet` to true, thus making any attempts to execute `set` result in a `revert`

The Solidity compiler stores the variable `value` in slot 0 and the variable `isSet` in slot 1. If we want to verify whether set does its job as it is supposed to (set `value`only once) we will have to verify:

• If for any possible input with `slot 1` set to false, the contract modifies `value` as it is supposed
• If for any possible input with `slot 1` set to true, the contract always reverts

This may sound like something very hard to do, but in reality, is quite simple and there are multiple options to start formally verifying your smart contracts and there are tools that allow us to perform Formal Verification at a relatively high level. In this article, I am going to use `klab` , a tool provided by DappHub that comes with a high-level specification language.

# Let’s start writing code

Let’s set up our environment like this:

`├── dapp│   ├── out│   │   └── OneWaySetter.sol.json│   └── src│       └── OneWaySetter.sol└── src    ├── prelude.smt2.md    ├── specification.act.md    └── storage.k.md`

where:

• config.json is the file that tells to Klab where and what to look at.
• OneWaySetter.sol is our Solidity Smart Contract
• OneWaySetter.sol.json is our compiled Solidity smart contract (in order to compile your smart contract open your terminal, go to the dapp folder `cd dapp` and type
`solc --combined-json=abi,bin,bin-runtime,srcmap,srcmap-runtime,ast src/OneWaySetter.sol > out/OneWaySetter.sol.json`
• specification.act.md is where our specifications are contained (Klab high-level language)
• storage.k.md is used to complete our specifications (high-level semantics) with some K language (low-level semantics). this file will be empty in this case.
• prelude.smt2.md is written using the low-level input format of Z3 theorem prover and contains the prelude of our formal verification. the prelude is the collections of all the facts that could be relevant to our smart contract.

# Our Specification.

First, let’s make our configuration:

For this example, we aren’t using anything that needs storage.k.md so we will keep it empty.

This is our prelude (prelude.smt2.md):

Finally, let’s define our specifications (specification.act.md):

````actbehaviour set of OneWaySetterinterface set(uint256 Value)types   IsSet : boolstorage   0 |-> _ => Value   1 |-> IsSet => 1iff   VCallValue == 0   IsSet == 0````

What we are doing here is:

Types Preamble:

• in the `types preamble` we declare the variables needed for our specification

Storage Preamble:

• in the `storage preamble`, we specify anything that changes the contract’s state and assigns the values declared into the `types premble`
• setting IsSet to represent the value of `slot 1` before the execution of `set` and specify that after the execution `slot 1` changes its value to one.
• Specify that `slot 0` changes to the value given as input.

Iff Preamble:

• in the `iff preamble`we determine the conditions needed for not cause a `revert`
• We say that there should be no ethers sent along with the transaction `VCallValue == 0` and that the `slot 1`must be `0` before the execution of `set`.

now we can run `klab prove-all` and:

`Doing initial spec build, this may take a while...[ 'src/OneWaySetter.sol' ][ 'src/OneWaySetter.sol' ]3410388bb51887b48311a94d8f63166ba1ad88dd98b988ece7a0e734622b2801 OneWaySetter__exhaustiveness51c13b8610bad9cbfd805e52e169b639870b3a24860c265cd82fb2aa6e7a3775 OneWaySetter_set_pass_roughd9f27f2f84fec78589a6c8bd390748a396250bfe5b0195f0bde7daa0f8eda667 OneWaySetter_set_fail_roughSTARTING proof batch 1.Academic tradition requires you to cite works you base your article on.When using programs that use GNU Parallel to process data for publicationplease cite:O. Tange (2011): GNU Parallel - The Command-Line Power Tool,  ;login: The USENIX Magazine, February 2011:42-47.This helps funding further development; AND IT WON'T COST YOU A CENT.If you pay 10000 EUR you should feel free to use GNU Parallel without citing.To silence this citation notice: run 'parallel --citation'.2020-01-11T11:09:38.620Z2020-01-11T11:09:38.624ZUsing evm-semantics from /home/giulio/klab/evm-semantics/Proof STARTING: d9f27f2f84fec78589a6c8bd390748a396250bfe5b0195f0bde7daa0f8eda667.k [OneWaySetter_set_fail_rough] (with state logging)Using evm-semantics from /home/giulio/klab/evm-semantics/Proof STARTING: 51c13b8610bad9cbfd805e52e169b639870b3a24860c265cd82fb2aa6e7a3775.k [OneWaySetter_set_pass_rough] (with state logging)Proof ACCEPT: 51c13b8610bad9cbfd805e52e169b639870b3a24860c265cd82fb2aa6e7a3775.k [OneWaySetter_set_pass_rough] (with state logging)2020-01-11T11:10:51.968Z/home/giulio/klab/bin/klab: riga 2: /home/giulio/klab/bin/../libexec/klab-gas-analyser: File o directory non esistente2020-01-11T11:10:52.293ZUsing evm-semantics from /home/giulio/klab/evm-semantics/Proof STARTING: 3410388bb51887b48311a94d8f63166ba1ad88dd98b988ece7a0e734622b2801.k [OneWaySetter__exhaustiveness] (with state logging)Proof ACCEPT: d9f27f2f84fec78589a6c8bd390748a396250bfe5b0195f0bde7daa0f8eda667.k [OneWaySetter_set_fail_rough] (with state logging)2020-01-11T11:10:54.822ZProof ACCEPT: 3410388bb51887b48311a94d8f63166ba1ad88dd98b988ece7a0e734622b2801.k [OneWaySetter__exhaustiveness] (with state logging)2020-01-11T11:11:48.006Z`

as we can see our formal verification is successful and that was quite simple to do. so what does this tell us:

Making Errors is easy for humans, but for mathematics, it is not, so we should put our trust in math as much as possible rather than in a developer. if you don’t, you will end like the Parity multi-sig wallet.

~ Cheers

Written by

## Giulio Rebuffo

Welcome to a place where words matter. On Medium, smart voices and original ideas take center stage - with no ads in sight. Watch
Follow all the topics you care about, and we’ll deliver the best stories for you to your homepage and inbox. Explore
Get unlimited access to the best stories on Medium — and support writers while you’re at it. Just \$5/month. Upgrade