- 17.3K All Categories
- 9.5K Mining
- 574 Pool Discussion
- 378 Promotional
- 1.4K General Project Discussion (non-technical)
- 485 Education
- 811 Protocol and Client discussion
- 170 web3-js
- 29 Whisper
- 16 Swarm
- 3 RLP
- 303 IoT & Hardware
- 1.2K Smart Contracts and Dapps
- 28 Serpent
- 359 Solidity
- 664 Projects
- 1.2K Reference clients code and builds
- 249 Eth & AlethZero- Cpp Implementation
- 471 Geth - Go Implementation
- 242 Mist
- 15 Node.js Implementation
- 36 Python Implementation
- 49 Mix
- 36 Other Implementations
- 170 Meetups
- 40 Other Events
- 226 Jobs & Skills
- 281 Press and Articles
- 75 Audio/Video
- 296 Ether Sale
- 1.2K Other Languages
- 96 Chinese
- 255 German
- 33 Italian
- 111 French
- 3 Hebrew
- 42 Japanese
- 75 Portugese
- 46 Romanian
- 185 Russian
- 231 Spanish
- 47 Turkish
- 125 Watercooler

We just merged a first pull request that allows Solidity contracts to be formally verified using a toolkit called why3.

This means that a computer creates and checks a mathematical proof of assertions about the behaviour of the contract.

Only a small subset of Solidity is supported for now, but that makes it already possible to verify a recursive binary search routine on arrays:

https://gist.github.com/chriseth/0c671e0dac08c3630f47

In that example, it is assumed that the given array of integers is sorted and the formal verification toolkit verifies the assertions that

1. if the function returns -1, then none of the elements of the array is equal to the requested value

2. if the function returns some i which is not -1, then the element at position i is equal to the requested value.

As an important part of the verification, why3 actually also checks that arithmetic operations never overflow and you never divide by zero.

After that, you can use "why3 ide /tmp/output_directory/solidity.mlw" to start a graphical version of the toolkit and perform the verification.

As why3 itself is only a frontend to the real workhorses, the provers, you need to install a prover. I tried "alt-ergo" and Z3 - the first is part of the ubuntu distribution, the second has binaries for most platforms.

After installing the prover (and making sure it is in the PATH), call "why3 config --detect" and it should detect your prover.

The blue question marks on the left are assertions that are not yet known to be true or false. If you click on one of them and then on the "Alt-Ergo" or "Z3"-button, it will invoke the prover and try to prove the assertion. The default is to try for 6 seconds which is too short for the whole task for alt-ergo (Z3 will have no problems), but it is also more fun to see what the prover actually does, so let us do an interactive proof:

If you click on "VC for _find_internal" (assuming you are looking at the binary search example), it will show you the source code on the right. The marked parts of the source code are parts which the selected task will reason about. Green are positive assumptions, red are negative assumptions and orange are assumptions to be proven. The three "Strategies" buttons on the left will ask the prover to try a certain strategy. In this case, you should click on "Split", which will create several sub-goals to be proven. If you now click the "Alt-Ergo" button, it will try again to prove all the sub-goals but now allot 6 seconds for each sub-goal. The prover will succeed in verifying most of the sub-goals and the blue circles will turn green. If you repeat the same process for all blue circles, alt-ergo will eventually prove all the assertions.

## Comments

40✭✭1✭16✭16✭I found it MUCH simpler to use the "opam install method" explained here:

https://www.lri.fr/~marche/MPRI-2-36-1/install.html

16✭https://gist.github.com/patcon/1a58a3e84fa36f4beb75

16✭170✭✭✭1✭I doubt I can personally assist, this looks well above my skill level. But I have colleagues who may be able to.

Cheers

170✭✭✭