DevCon 2: Formal Verification for Solidity
Published in
1 min readNov 16, 2016
Writing code correctly is difficult. It’s hard to even define what correct is. Correct is when the program does what the programmer expected, but it’s hard to test the infinite set of undesired behaviors. Formal verification allows us to proof correctness on all inputs — it can even let developers ask questions about the program’s execution. Why3 annotates Solidity with pre- and post-conditions. Future work will model the msg variable, multi-contract conditions and multi-transaction conditions for use in proofs.
This series was a collaborative research project written by Bill Gleim, Simon de la Rouviere, Paul Kohlhaas, and Niran Babalola. It was crowdfunded by the Ethereum Movement, a decentralized nonprofit built on Benefactory.
