Too Long; Didn't Read
Vulnerabilities in smart contracts are threatening <a href="https://hackernoon.com/tagged/blockchain" target="_blank">blockchain</a> projects, developers and investors for a long time. A growing number of <a href="https://hackernoon.com/tagged/security" target="_blank">security</a> teams are putting efforts in this field with various approaches to secure contracts. SECBIT Labs proposes combining the formal proofs with the traditional test and security audit. In this article, we take the ERC20 formal proof in our GitHub repository <a href="https://github.com/sec-bit/tokenlibs-with-proofs" title="https://github.com/sec-bit/tokenlibs-with-proofs" target="_blank">tokenlibs-with-proofs</a> as an example to show the use of formal proofs on smart contracts. We hope the formal proofs can help to eliminate buggy contracts, and secure all aspects of smart contracts including design logic, implementation, economic system, <em>etc</em>.