智能合约是在区块链（如以太坊）中执行以操纵数字资产的程序。由于智能合约中的错误可能导致巨大的经济损失，人们对证明其正确性有相当大的兴趣。然而，智能合约的规范和验证面临着在其他应用领域很少出现的挑战。智能合约经常与未经验证的、潜在的对抗性外部代码交互，这大大削弱了所作出的假设的合理性。此外，智能合约的核心功能是操纵和转移资源，简洁地描述这种功能需要专门的规范支持。目前的推理技术并没有完全解决这些挑战...