Jonas Nick 在 TABConf 2022 大会上介绍了使用 hac-spec 编写规范以实现可证明无 bug 的 BIP 及其实现的方法。Hac-spec 是 Rust 的一个子集，它允许生成简洁、可执行、可验证的密码学规范，并通过形式化验证来减少 bug，并探讨了未来使用工具自动生成安全证明的可能性。
Simplicity 是一种用于区块链智能合约的底层编程语言和机器模型，其设计目标是拥有简单的语义，以便进行形式化分析和推理。它旨在解决在表达能力和可靠性之间权衡的问题，允许开发者设计复杂的智能合约并验证其安全性、可靠性和成本。Blockstream 发布了 Simplicity 的源代码，并计划将其集成到 Elements 平台。
BTCStudy