News for hackers. Stuff that matters.

A comment on A hacker stole $31M of Ether – how it happened, and what it means for Ethereum. Parent comment

Re:A hacker stole $31M of Ether – how it happened, and what ... by mbrock on Friday July 21, 2017 @03:04AM (#14818621)
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.

[ Parent | on HN ]
Re:A hacker stole $31M of Ether – how it happened, and what ... by chalst on Tuesday July 25, 2017 @11:36AM (#14848534)
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

[2]: https://github.com/pirapira/ethereum-formal-verification-ove...

[3]: http://lambda-the-ultimate.org/node/5003#comment-94645

[ Parent | on HN ]