随着区块链技术的传播，智能合约——监管在不可信环境下加密资产交换的计算机协议——已经变得流行起来。智能合约的一个标志性的安全属性是流动性:在非流动性合约中，可能会发生一些资产被冻结的情况，即不能被任何人赎回。这个问题的相关性可以从最近对以太坊的流动性攻击中看出，这些攻击冻结了数亿美元。我们解决了在BitML上验证流动性的问题，BitML是一种智能合约的DSL，带有比特币的安全编译器，具有货币转移、...