用形式化验证缓解智能合约漏洞
Solidity已经支持对未调用其他合同的某些智能合约进行正式验证。当然，这不包括任何转让代币的合约。下面的Solidity合同模拟了一个原始的众筹合约，该合约可以持有Token，某些人可以根据其股份提取Token。它缺少实际的访问控制，但此处要说明的要点如下：您不能通过递归调用漏洞或任何其他方式提取最多的代币。允许递归调用，但是合约仍然可以处理它们。更具体地说，在合约的整个生命周期中，总余额和代币之间的差额是恒定的。因此，这种差异是所谓的不变性。在Solidity端您需要做的就是将此不变式添加
