Part 2

Part 3

Part 4

The motivation for Formal Verification
Security of smart contracts is still a crucial challenge: we all remember the DAO, parity hacks, a bunch of smaller attacks and the most recent delayed hard fork. We would like to see the future in which we can be way more confident about our code.

Depending how you count, event over a half a billion dollars (by today’s Ethereum evaluation), was lost in a couple of biggest smart contract hacks.

What about if behind every responsible piece of code stands pure solid mathematics instead of personal conviction of developers? With formal verification tools for Ethereum finally maturing, it is now not only possible but also practical.

In this and following post we will be getting step by step into the world of K-framework, which allows to formally verify EVM smart contracts.