Ask HN: Will smart contract security bring attention to formal verification?

10 points

8 years ago

In the past there have been numerous incidents caused by flawed smart contract code, leading to significant financial losses. One example is the DAO hack in May 2016 [1], which resulted in a hardfork of the ETH blockchain.

Isn't this a beautiful opportunity to highlight the strengths of formal verification methods as a means to prevent such disasters from the outset?

The area is actively being researched for example at ETH Zürich [2]. The SF-based startup Quantstamp [3] are designing a system based on an Ethereum ERC20 token with the goal to automate and effectively decentralize smart contract verification and auditing. Think fuzzers as well as SAT+SMT solvers running on nodes in a decentralized network competing for rewards akin to proof of work based systems [4].

In the near future I can see the Quantstamp network develop into a leading platform for software verification services. Starting with Ethereum smart contracts, they plan to expand to other platforms like NEO, WAVES or ADA. Maybe the computational power of the verification network can be leveraged to verify more general purpose software as well? I'm excited to see what will come.

Is that a realistic outlook in your opinion?

[1] https://en.wikipedia.org/wiki/The_DAO_(organization)

[2] Securify, Formal Verification of Ethereum Smart Contracts, http://www.securify.ch/

[3] https://quantstamp.com/

[4] Quantstamp whitepaper, https://docsend.com/view/shcsmhe

6 comments