Ethereum Heist

Ethereum is a blockchain cryptocurrency of the kind that normally attracts people with a certain political ideology. Ethereum's novelty is the inclusion of a virtual machine that allows running programs on the blockchain (I'm not familiar enough with the concept to understand precisely what that means), that are intended to encode machine contracts. The (first? and) most famous of those contracts is an organization called The DAO, which is a virtual VC of sorts, where people have invested their money and can vote on investments.

It turns out that the DAO contract contains a bug, or an "unintended feature", which has allowed someone to steal $50M worth of funds from the DAO in the last 24 hours.

The Ethereum team (which, I believe, is also the team behind the DAO), has issued a call (reproduced below) to formal method experts to help prevent such events from happening again; they are offering grants:

> Developers, cryptographers and computer scientists should note that any high-level tools (including IDEs, formal verification, debuggers, symbolic execution) that make it easy to write safe smart contracts on Ethereum are prime candidates for DevGrants, Blockchain Labs grants and String’s autonomous finance grants.

The Ethereum VM specification is found here, and I believe that a TLA+ model, which would allow modeling and verifying Ethereum contracts, is a very reasonable effort, which may also be a great marketing opportunity for TLA+ in light of the media attention given to the heist.

Ron