A Semantic Framework for the Security Analysis of Ethereum smart contracts
Source code of Ethereum Virtual Machine bytecode F* formalization
Technical report