3 ms·
Yoichi Hirai and others are working on completing proof assistant support for EVM, meaning you will be able to prove program properties using logical pre/post-c
by mbrock 9y ago
Yoichi Hirai and others are working on completing proof assistant support for EVM, meaning you will be able to prove program properties using logical pre/post-conditions with machine checked proofs.
There are already useful tools for symbolic execution, and I have a hunch that this kind of verification will be important along with model checking.
- chalst 9y agoThe 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