The rigorous security model of Bitcoin's UTXO architecture often comes at the cost of developer usability, forcing a reliance on manual stack manipulation that leads to critical financial vulnerabilities like signature malleability, unspendable states and unconstrained execution paths. Industry standards such as Miniscript provide necessary abstractions for policy verification but do not model the full imperative logic required for complex contracts, leaving gaps in state management and resource liveness. This paper introduces Bithoven, a high-level language designed to bridge the gap between expressiveness and formal safety. By integrating a strict type checker and a resource liveness analyzer with a semantic control-flow analyzer, Bithoven eliminates major categories of consensus and logic defects defined in our fault model prior to deployment. Our results indicate that this safety comes at modest cost: Bithoven compiles to Bitcoin Script with efficiency comparable to hand-optimized code, demonstrating that type-safe, developer-friendly abstractions are viable even within the strict byte-size constraints of the Bitcoin blockchain.

翻译：比特币UTXO架构的严格安全模型通常以牺牲开发者可用性为代价，强制依赖手动堆栈操作，导致签名延展性、不可花费状态和无约束执行路径等关键金融漏洞。Miniscript等行业标准为策略验证提供了必要的抽象，但未能建模复杂合约所需的完整命令式逻辑，在状态管理和资源活性方面存在缺陷。本文提出Bithoven——一种旨在弥合表达力与形式化安全性之间鸿沟的高级语言。通过将严格类型检查器、资源活性分析器与语义控制流分析器相结合，Bithoven在部署前即可消除故障模型中定义的主要共识与逻辑缺陷类别。实验结果表明，这种安全性的代价可控：Bithoven编译生成的比特币脚本效率与手工优化代码相当，证明即使在比特币区块链严格的字节大小限制下，类型安全且开发者友好的抽象方案仍然具备可行性。