The specification of EVM in HOL exists already [1] and can be used to prove correctness of EVM code already. EVM is pretty low-level, though; the same can't be

The specification of EVM in HOL exists already [1] and can be used to prove correctness of EVM code already. EVM is pretty low-level, though; the same can't be done for Solidity code. Yoichi has a page that outlines his thinking about what Ethereum's formal verification needs are [2]. What I would like to see is a verified high-level smart contract language layered on top of the Ethereum stack, allowing non-logicians to put together contracts that mean what they think they mean. See [3]. [1]: https://github.com/pirapira/eth-isabelle https://github.com/pirapira/eth-isabelle [2]: https://github.com/pirapira/ethereum-formal-verification-overview https://github.com/pirapira/ethereum-formal-verification-ove... [3]: http://lambda-the-ultimate.org/node/5003#comment-94645 http://lambda-the-ultimate.org/node/5003#comment-94645