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

- 10.3K All Categories
- 4.8K Mining
- 192 Pool Discussion
- 900 General Project Discussion (non-technical)
- 281 Education
- 623 Protocol and Client discussion
- 119 web3-js
- 20 Whisper
- 11 Swarm
- 2 RLP
- 171 IoT & Hardware
- 767 Smart Contracts and Dapps
- 28 Serpent
- 272 Solidity
- 298 Projects
- 1.1K Reference clients code and builds
- 243 Eth & AlethZero- Cpp Implementation
- 408 Geth - Go Implementation
- 186 Mist
- 14 Node.js Implementation
- 34 Python Implementation
- 47 Mix
- 20 Other Implementations
- 135 Meetups
- 23 Other Events
- 126 Jobs & Skills
- 162 Press and Articles
- 70 Audio/Video
- 238 Ether Sale
- 647 Other Languages
- 33 Chinese
- 104 German
- 18 Italian
- 82 French
- 2 Hebrew
- 6 Japanese
- 48 Portugese
- 27 Romanian
- 109 Russian
- 147 Spanish
- 27 Turkish
- 99 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

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

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

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

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

Cheers

170Member ✭✭✭