Is formal verification of contracts feasible? Is anyone working on it?
Also, here's a possibly crazy idea: could one create bug bounties for algorithms (or even arbitrary software) on the Ethereum blockchain by writing the algorithm into a contract such that if you somehow break it you receive the bounty?
An example of this would be the massive implicit bounty currently placed on the crypto algorithms (SHA256, ECDSA/Secp256k1, etc) underpinning cryptocurrencies (of course, if those were broken the value of the cryptocurrency would plummet instantly)
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.
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].
Yes, but I'm suggesting designing explicit bug bounties. The point of a bug bounty is to offer a smaller sum of money than would be lost if the vulnerability were exploited maliciously.
Cryptocurrencies are serving as bug bounties for their crypto primitives, but that only benefits other users of those primitives.
Also, here's a possibly crazy idea: could one create bug bounties for algorithms (or even arbitrary software) on the Ethereum blockchain by writing the algorithm into a contract such that if you somehow break it you receive the bounty?
An example of this would be the massive implicit bounty currently placed on the crypto algorithms (SHA256, ECDSA/Secp256k1, etc) underpinning cryptocurrencies (of course, if those were broken the value of the cryptocurrency would plummet instantly)