Bithoven：面向表达性比特币智能合约的形式化安全

比特币UTXO架构的严格安全模型往往以开发者可用性为代价，迫使依赖手动堆栈操作，导致关键财务漏洞，如签名可塑性、不可花费状态和不可约束的执行路径。行业标准如Miniscript为策略验证提供必要抽象，但未能建模复杂合约所需的完整命令式逻辑，导致状态管理和资源存活性存在空白。本文引入Bithoven，一个高级语言旨在弥合表达性与形式化安全之间的鸿沟。通过集成严格类型检查器、资源存活性分析器和语义控制流分析器，Bithoven在部署前消除我们fault model中定义的主要共识和逻辑缺陷。我们的结果表明，这种安全性代价适中：Bithoven编译为比特币脚本的效率可与手工优化代码相当，表明即使在比特币区块链严格的字节大小限制下，类型安全、开发者友好的抽象也是可行的。