Deductive Proof of Ethereum Smart Contracts Using Why3

For the final version the code will be kept in a more permanent location.

The why3 file of the case studies: BEMP.mlw.

why3 ide -L . BEMP.mlw

The implementation of the why3 to EVM compiler, cost evaluation the code in the Why3 development branch.

git clone git@gitlab.inria.fr:why3/why3.git
cd why3
git checkout 844e15d
./configure --enable-local
make
bin/why3 extract  -D drivers/yul.drv
bench/extraction/extraction_evm.mlw --debug evm_gas_checking > asm.evm
evm --codefile asm.evm --input "14bcc435" run