It looks like you're new here. If you want to get involved, click one of these buttons!

- 15.9K All Categories
- 8.9K Mining
- 497 Pool Discussion
- 1.3K General Project Discussion (non-technical)
- 420 Education
- 754 Protocol and Client discussion
- 148 web3-js
- 24 Whisper
- 12 Swarm
- 3 RLP
- 289 IoT & Hardware
- 969 Smart Contracts and Dapps
- 28 Serpent
- 332 Solidity
- 514 Projects
- 1.2K Reference clients code and builds
- 248 Eth & AlethZero- Cpp Implementation
- 462 Geth - Go Implementation
- 237 Mist
- 15 Node.js Implementation
- 35 Python Implementation
- 48 Mix
- 30 Other Implementations
- 157 Meetups
- 35 Other Events
- 193 Jobs & Skills
- 199 Press and Articles
- 73 Audio/Video
- 279 Ether Sale
- 1K Other Languages
- 68 Chinese
- 238 German
- 31 Italian
- 102 French
- 2 Hebrew
- 9 Japanese
- 66 Portugese
- 44 Romanian
- 163 Russian
- 211 Spanish
- 41 Turkish
- 114 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✭✭✭