比特币白皮书 16 周年，解析比特币应用去信任化的关键：BitVM 及其形式化验证

比特币白皮书发布于 2008 年 10 月 31 日，中本聪（Satoshi Nakamoto）在 P2P foundation 网站发布比特币白皮书《比特币：一种点对点的电子现金系统》，今天迎来 16 周年生日。

比特币的初始交易价格为 0.0008 美元，如今升值超过 9000 万倍。

众所周知，比特币重新定义了人们对价值转移的信任方式。在去中心化的网络中，信任被技术所取代，每一笔交易都由网络自身验证。然而，随着去中心化金融（DeFi）和智能合约的兴起，如何在比特币网络中安全地引入更复杂的计算，构建更丰富的内容，成为了新的挑战。

BitVM 是什么？

2023 年 12 月，ZeroSync 项目负责人 Robin Linus 发表了一篇名为《BitVM：Compute Anything On Bitcoin》的白皮书，引发了大家对于提升比特币可编程性的思考。

BitVM 的出现，为比特币带来了链下执行复杂计算、链上验证结果的能力，极大地扩展了其功能。更直白来说，BitVM 是一个允许在比特币网络上执行复杂计算和智能合约的解决方案。这是一种在不改变比特币网络共识的情况下，可实现图灵完备的解决方案。通过成为图灵完备，比特币区块链理论上可以用来扩展比特币的功能，远远超出比特币白皮书中首次提出的“点对点电子现金系统”愿景。它允许用户在比特币之上创建应用程序——类似于以太坊等其他平台上已经实现的功能，同时，保持了比特币众所周知的高度安全性和去中心化。

简单总结，BitVM 可以使 Bitcoin 生态不仅满足交易需求，而且能在 BTC 层上创造更加复杂的 DApps。同时，保留了 Bitcoin 的安全性和去中心化的特征。

然而，复杂性往往伴随着风险，如何确保这些复杂计算的安全性，成为了亟待解决的问题。

当前，致力于 BitVM 研究与开发的团队众多，其中包括： BitVM 创始人 Robin 创立的 ZeroSync, 加州大学圣芭芭拉分校 Prof. Yu Feng 创立的比特币原生项目 Nubit，致力 ZK 扩容比特币的 Alpen Labs，专注比特币 ZK Rollup 的 Chainway Labs，Citrea，还有 BRC20 的创始人 Domo 所在的 Layer 1 Foundation 等。

目前，Nubit 联合 ZeroSync、Alpen Labs、Chainway Labs 以及 Domo 带领的 Layer 1 Foundation， 在 10 月 31 日发表论文《Push-Button Verification for BitVM Implementations》，完成并推出了 BitVM 形式化验证工具。论文中，Nubit 通过形式验证（Formal Verification）自动化数学证明，为 BitVM 应用的安全性提供进一步保障，让开发者和用户能放心地构建和使用应用。

形式化验证是什么？如何帮助确保 BitVM 的安全性？

在 Robin 的论文中，BitVM 引入了一个系统，该系统使任何计算都可以在比特币的区块链上进行验证，其方式不会影响其安全性或更改网络。然而，系统开发以及基于此的应用构建，往往需要专家人工审查代码。在比特币这样对安全性要求极高的生态中，手动审查既耗时又可能出错。形式化验证（Formal Verification）通过纯数学运算，能够自动验证程序逻辑是否符合预期，为 BitVM 整体系统提供安全保障。

想象一下，你正在比特币上部署一个涉及多方交易的智能合约。为了确保合约在各种情况下都能正确执行，传统方法可能需要反复测试每一种可能性。但有了形式化验证（Formal Verification）工具，数学证明将自动检查合约的正确性，极大提升系统运行的安全属性。

BitVM 的特殊挑战：智能合约复杂度与比特币脚本的局限性

与以太坊等具备图灵完备性（Turing-complete）的区块链不同，比特币脚本语言受限于安全性考量，无法直接运行复杂计算。BitVM 通过链下执行和链上验证的模式实现了比特币智能合约的基本功能。换句话说，所有复杂的计算都在链下完成，只有结果在链上得到验证，极大地减轻了比特币链的负载。然而，这一创新带来了显著的实现难度。

首先，BitVM 的设计中包含了大量堆栈操作和寄存器计算，这些操作需要在比特币的非图灵完备脚本中高效地实现和验证。例如，为确保合约执行时能够正确判断数值的正负，一个常用函数是 is_positive，它通过检查数值的最高位判断正负。然而在一个早期版本中，is_positive 函数因为计算偏差而错误地将 0 判定为正数，这种细微的错误可能导致合约执行的严重偏差，甚至引发潜在的经济损失。