[Why3-club] Formal verification of smart contracts

Jean-Christophe Filliatre Jean-Christophe.Filliatre at lri.fr
Tue Aug 2 08:33:15 CEST 2016

Dear Christian,

Trywhy3 is implemented in OCaml and translated to Javascript using
js_of_ocaml ; see http://ocsigen.org/js_of_ocaml/

The sources of trywhy3 are in the subdirectory src/trywhy3/ of Why3
sources. In this subdirectory, you'll find a README file containing
instructions to build trywhy3 (among other things, a Javascript editor,
a font, and the Alt-Ergo SMT solver are requirements).

Let us know if you have questions.

Best regards,

On 01/08/2016 17:16, Christian Reitwiessner wrote:
> Dear Jean-Christophe,
> thank you for the remarks! I chose to encode the restrictions of the
> virtual machine as part of the code and not as part of the conditions,
> because of the complications with the to_int projection. In the
> meantime, our project is available online, some introduction can be
> found here:
> https://www.reddit.com/r/ethereum/comments/4uu9fb/formal_verification_for_solidity/
> Our main "IDE" can be found at https://ethereum.github.io/browser-solidity
> Just like "try why3" it works fully in the browser, and I would like to
> integrate the browser version of why3 together with alt-ergo directly
> into that IDE.
> I had a look at the javascript code of "try why3", but it seems we
> cannot use it as is. Could you perhaps provide me with some pointers
> about how "try why3" was built, or is there a javascript version of it
> that can be better integrated into browser projects?
> Thanks,
> Christian.
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/why3-club

More information about the Why3-club mailing list