[Why3-club] Formal verification of smart contracts

Christian Reitwiessner chris at ethereum.org
Mon Aug 1 17:16:48 CEST 2016


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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20160801/aee658a3/attachment.html>


More information about the Why3-club mailing list