Skip to content

Instantly share code, notes, and snippets.



Last active Jul 28, 2017
What would you like to do?
Installing why3 IDE for verifying sample Ethereum contract (Ubuntu 14.04)
# install ocaml and deps
apt-get install ocaml ocaml-native-compilers
apt-get install liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev libocamlgraph-ocaml-dev

# install opam from binaries (ocaml package manager)
# See
wget -O - | sh -s /usr/local/bin/

#### OR

# Can use system package manager if opam >= v1.1.1
apt-get install opam

# install why3
opam install why3

# install alt-ergo prover
opam install alt-ergo altgr-ergo satML-plugin
why3 config --detect

# Open pre-generated output file in why3 IDE
cd /tmp
git clone eth-binsearch-proof.gist
why3 ide eth-binsearch-proof.gist/Output_BinarySearch.mlw
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.