比特幣白皮書發佈於 2008 年 10 月 31 日，中本聰（Satoshi Nakamoto）在 P2P foundation 網站發布比特幣白皮書《比特幣：一種點對點的電子現金系統》，今天迎來 16 週年生日。

比特幣的初始交易價格為 0.0008 美元，如今升值超過 9,000 萬倍。

眾所周知，比特幣重新定義了人們對價值轉移的信任方式。在去中心化的網路中，信任被科技取代，每一筆交易都由網路本身驗證。然而，隨著去中心化金融（DeFi）和智慧合約的興起，如何在比特幣網路中安全地引入更複雜的運算，建構更豐富的內容，成為了新的挑戰。

BitVM 是什麼？

2023 年12 月，ZeroSync 專案負責人Robin Linus 發表了一篇名為《BitVM：Compute Anything On Bitcoin》的白皮書，引發了大家對於提升比特幣可編程性的思考。

BitVM 的出現，為比特幣帶來了鏈下執行複雜計算、鏈上驗證結果的能力，大大擴展了其功能。更直白來說，BitVM 是一個允許在比特幣網路上執行複雜運算和智慧合約的解決方案。這是一種在不改變比特幣網路共識的情況下，可實現圖靈完備的解決方案。透過成為圖靈完備，比特幣區塊鏈理論上可以用來擴展比特幣的功能，遠遠超出比特幣白皮書中首次提出的「點對點電子現金系統」願景。它允許用戶在比特幣之上創建應用程式——類似於以太坊等其他平台上已經實現的功能，同時，保持了比特幣眾所周知的高度安全性和去中心化。

簡單總結，BitVM 可以讓 Bitcoin 生態不僅滿足交易需求，而且能在 BTC 層上創造更複雜的 DApp。同時，保留了 Bitcoin 的安全性和去中心化的特徵。

然而，複雜性往往伴隨著風險，如何確保這些複雜計算的安全性，成為了亟待解決的問題。

目前，致力於BitVM 研究與開發的團隊眾多，其中包括： BitVM 創辦人Robin 創立的ZeroSync, 加州大學聖芭芭拉分校Prof. Yu Feng 創立的比特幣原生計畫Nubit，致力ZK 擴容比特幣的Alpen Labs，專注於比特幣ZK Rollup 的Chainway Labs，Citrea，以及Fiamma，還有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 判定為正數，這種細微的錯誤可能導致合約執行的嚴重偏差，甚至引發潛在的經濟損失。

透過形式化驗證（Formal Verification），Nubit 的工具能夠在程式碼部署前自動檢查類似的計算邏輯，確保所有執行路徑都符合預期。在這裡，Nubit 團隊設計了一種基於寄存器的 DSL（領域特定語言），將比特幣腳本複雜的堆疊操作轉換為更易於驗證的寄存器操作，從而簡化了開發和驗證流程。此外，針對多次重複的循環式計算，該 DSL 引入了「循環不變量」，以有效地減少程式碼中的重複計算，降低驗證難度。

驗證效果：自動化形式化驗證的高效性

從論文中看，Nubit 的形式化驗證（Formal Verification）工具在98 個BitVM 的SNARK 驗證器基準上進行了廣泛測試，驗證成功率高達94%，且大部分驗證任務在數秒內即可完成。相較於傳統的手動審查，這項工具不僅提高了驗證速度，也避免了人工錯誤的可能性，為 BitVM 智慧合約在比特幣上的可靠執行提供了保障。

這個結果證明，形式化驗證（Formal Verification）在比特幣複雜應用中的確具備極高的實際價值，特別是在對安全性要求在極高的BTCFi 應用中，能夠有效降低風險。

BitVM 與比特幣生態：拓展比特幣智能合約的潛力

透過形式化驗證（Formal Verification），BitVM 的安全性得到了顯著提升，在幫助開發者在比特幣上建立更複雜的合約和應用的同時，讓用戶在去中心化金融和跨鏈應用中享受到比特幣生態的高安全性。作為比特幣生態系統的創新工具，BitVM 為比特幣在複雜應用中的擴展奠定了基礎。

比特幣從未被設計成複雜運算平台，而是專注於價值儲存和轉移的可靠性。然而，隨著 BitVM 推出，比特幣生態正在朝向智慧合約和 DeFi 應用程式邁進。對於去中心化應用的發展而言，完成形式化驗證 BitVM 不僅是技術上的進步，更代表了比特幣在去中心化金融和智能合約上的一個重要里程碑。

BitVM 開啟比特幣未來生態

在BitVM 的發展過程中，Nubit 與ZeroSync 、Alpen Labs、Chainway Labs 和Layer 1 Foundaton 等團隊緊密合作，其推出的形式化驗證BitVM 為比特幣生態帶來了全新的安全和技術標準。同時，Nubit 在 Starkware 和 Fractal Bitcoin 的資助下將繼續推動安全、可驗證的比特幣原生運算的發展。

萬事起頭難，BitVM 帶來的比特幣生態仍在萌芽，但早期專案間深度的協作與創新，將不僅為複雜運算的安全性提供有力保障，也將為比特幣的未來開啟無限可能。一個人人都能信任、人人都能參與的比特幣新時代正在到來。

原文連結