首个“携带交互式形式化证明”的智能合约库发布

【链得得播报】链得得（微信号：ChainDD）7月7日讯，安比（SECBIT）实验室联合 ConsenSys中国发布了全球首个携带交互式形式化证明的智能合约库，为目前漏洞频出的数字货币智能合约开发工作提供安全保障手段。

此次发布的智能合约库借助交互式定理证明工具COQ，提供了对ERC20智能合约中的一些高阶逻辑特性的形式化证明。经过证明的 ERC20合约具有以下特性：不存在溢出漏洞、其账户余额总量满足和totalSupply一致、Token中的总量不变、合约转账无法影响非相关账户余额等。