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.

Ethereum is a platform that makes it possible for any developer to write and distribute next-generation decentralized applications.

Borrowing the concept of distributed consensus and cryptographic proof that makes cryptocurrencies such as Bitcoin so effective in trustless payments, Ethereum extends the use of these technologies to trustless agreements. This allows developers to easily build innovative new products on a censorship and collusion-resistant foundation.

Ethereum will go live in Q4 2014, in the meantime we are regularly releasing alpha software so you can try your hand at building distributed applications.

Main site: https://www.ethereum.org

Forums: https://forum.ethereum.org

Github: https://github.com/ethereum

Blog: http://blog.ethereum.org

Code Releases: https://code.ethereum.org

Wiki: http://wiki.ethereum.org

Meetups: http://ethereum.meetup.com

Whitepaper: http://ethereum.org/ethereum.html

Facebook: https://www.facebook.com/ethereumproject

Google+: http://google.com/+EthereumOrgOfficial

IRC Freenode: #ethereum