Jonas Nick 在 TABConf 2022 大会上介绍了使用 hac-spec 编写规范以实现可证明无 bug 的 BIP 及其实现的方法。Hac-spec 是 Rust 的一个子集，它允许生成简洁、可执行、可验证的密码学规范，并通过形式化验证来减少 bug，并探讨了未来使用工具自动生成安全证明的可能性。
BTCStudy