一句话：提出基于 BitML 的工具链，可自动验证并编译比特币智能合约，确保流动性等性质。
本文针对可在比特币上执行的智能合约，提出一套开发与验证工具链。该工具链以领域特定语言 BitML 为基础，BitML 可计算可靠地嵌入比特币。工具链能自动验证合约的相关性质，其中包括流动性，确保资金不会永久冻结在合约中。工具链还提供编译器，将 BitML 合约翻译成一组标准比特币交易，执行合约相当于把这些交易追加到区块链。作者通过一组代表性合约构成的基准来评估该工具链，展示了其可行性。
We present a toolchain for developing and verifying smart contracts that can be executed on Bitcoin. The toolchain is based on BitML, a recent domain-specific language for smart contracts with a computationally sound embedding into Bitcoin. Our toolchain automatically verifies relevant properties of contracts, among which liquidity, ensuring that funds do not remain frozen within a contract forever. A compiler is provided to translate BitML contracts into sets of standard Bitcoin transactions: executing a contract corresponds to appending these transactions to the blockchain. We assess our toolchain through a benchmark of representative contracts.