The 16th anniversary of the Bitcoin white paper: the key to de-trusting Bitcoin applications: BitVM and its formal verification

24-11-01 10:05

Read this article in 14 Minutes

AI summary

View the summary

The Bitcoin white paper was published on October 31, 2008. Satoshi Nakamoto published the Bitcoin white paper "Bitcoin: A Peer-to-Peer Electronic Cash System" on the P2P foundation website. Today is the 16th anniversary.

The initial trading price of Bitcoin was $0.0008, and it has appreciated more than 90 million times today.

As we all know, Bitcoin has redefined the way people trust value transfer. In a decentralized network, trust is replaced by technology, and every transaction is verified by the network itself. However, with the rise of decentralized finance (DeFi) and smart contracts, how to safely introduce more complex calculations in the Bitcoin network and build richer content has become a new challenge.

What is BitVM?

In December 2023, Robin Linus, head of the ZeroSync project, published a white paper titled "BitVM: Compute Anything On Bitcoin", which sparked everyone's thinking about improving Bitcoin's programmability.

The emergence of BitVM has brought Bitcoin the ability to perform complex calculations off-chain and verify results on-chain, greatly expanding its functionality. To put it more bluntly, BitVM is a solution that allows complex calculations and smart contracts to be performed on the Bitcoin network. This is a solution that can achieve Turing completeness without changing the consensus of the Bitcoin network. By becoming Turing complete, the Bitcoin blockchain can theoretically be used to expand Bitcoin's functionality far beyond the vision of a "peer-to-peer electronic cash system" first proposed in the Bitcoin White Paper. It allows users to create applications on top of Bitcoin - similar to what has been implemented on other platforms such as Ethereum, while maintaining the high security and decentralization that Bitcoin is known for.

In short, BitVM can enable the Bitcoin ecosystem to not only meet transaction needs, but also create more complex DApps on the BTC layer. At the same time, it retains the security and decentralization characteristics of Bitcoin.

However, complexity is often accompanied by risks, and how to ensure the security of these complex calculations has become an urgent problem to be solved.

Currently, there are many teams dedicated to the research and development of BitVM, including: ZeroSync founded by Robin, the founder of BitVM, Nubit, the Bitcoin native project founded by Prof. Yu Feng of the University of California, Santa Barbara, Alpen Labs dedicated to ZK expansion of Bitcoin, Chainway Labs and Citrea focusing on Bitcoin ZK Rollup, and Layer 1 Foundation where Domo, the founder of BRC20, is located.

Currently, Nubit, together with ZeroSync, Alpen Labs, Chainway Labs and the Layer 1 Foundation led by Domo, published a paper "Push-Button Verification for BitVM Implementations" on October 31, completing and launching the BitVM formal verification tool. In the paper, Nubit provides further security for BitVM applications through formal verification automated mathematical proofs, allowing developers and users to build and use applications with confidence.

What is formal verification? How can it help ensure the security of BitVM?

In Robin's paper, BitVM introduced a system that enables any computation to be verified on Bitcoin's blockchain in a way that does not affect its security or change the network. However, system development and the construction of applications based on it often require experts to manually review the code. In an ecosystem like Bitcoin that requires extremely high security, manual review is time-consuming and error-prone. Formal Verification can automatically verify whether the program logic meets expectations through pure mathematical operations, providing security for the BitVM overall system.

Imagine that you are deploying a smart contract on Bitcoin involving multi-party transactions. In order to ensure that the contract can be executed correctly in various situations, traditional methods may require repeated testing of every possibility. But with the Formal Verification tool, mathematical proofs will automatically check the correctness of the contract, greatly improving the security properties of the system operation.

BitVM’s special challenges: smart contract complexity and limitations of Bitcoin script

Unlike Turing-complete blockchains such as Ethereum, the Bitcoin script language is limited by security considerations and cannot directly run complex calculations. BitVM implements the basic functions of Bitcoin smart contracts through a mode of off-chain execution and on-chain verification. In other words, all complex calculations are completed off-chain, and only the results are verified on-chain, which greatly reduces the load on the Bitcoin chain. However, this innovation brings significant implementation difficulties.

First, the design of BitVM includes a large number of stack operations and register calculations, which need to be efficiently implemented and verified in Bitcoin’s non-Turing-complete scripts. For example, to ensure that the positive and negative values can be correctly judged when the contract is executed, a commonly used function is is_positive, which judges the positive and negative by checking the highest bit of the value. However, in an early version, the is_positive function mistakenly judged 0 as a positive number due to calculation deviation. This subtle error may lead to serious deviation in contract execution and even cause potential economic losses.

Image source: Push-Button Verification for BitVM Implementations

Through formal verification, Nubit's tools can automatically check similar calculation logic before code deployment to ensure that all execution paths are as expected. Here, the Nubit team designed a register-based DSL (domain-specific language) to transform the complex stack operations of Bitcoin scripts into register operations that are easier to verify, thereby simplifying the development and verification process. In addition, for repeated cyclic calculations, the DSL introduces "loop invariants" to effectively reduce repeated calculations in the code and reduce the difficulty of verification.

Image source: Push-Button Verification for BitVM Implementations

Verification effect: Efficiency of automated formal verification

According to the paper, Nubit's formal verification tool has been extensively tested on 98 BitVM SNARK verifier benchmarks, with a verification success rate of up to 94%, and most verification tasks can be completed within seconds. Compared with traditional manual review, this tool not only improves the verification speed, but also avoids the possibility of manual errors, providing a guarantee for the reliable execution of BitVM smart contracts on Bitcoin.

This result proves that formal verification does have extremely high practical value in complex Bitcoin applications, especially in BTCFi applications with extremely high security requirements, which can effectively reduce risks.

BitVM and Bitcoin Ecosystem: Expanding the Potential of Bitcoin Smart Contracts

Through formal verification, the security of BitVM has been significantly improved. While helping developers build more complex contracts and applications on Bitcoin, it allows users to enjoy the high security of the Bitcoin ecosystem in decentralized finance and cross-chain applications. As an innovative tool for the Bitcoin ecosystem, BitVM has laid the foundation for the expansion of Bitcoin in complex applications.

Bitcoin was never designed as a complex computing platform, but rather focused on the reliability of value storage and transfer. However, with the launch of BitVM, the Bitcoin ecosystem is moving towards smart contracts and DeFi applications. For the development of decentralized applications, completing the formal verification of BitVM is not only a technological advancement, but also represents an important milestone for Bitcoin in decentralized finance and smart contracts.

BitVM opens up the future ecosystem of Bitcoin

During the development of BitVM, Nubit worked closely with teams such as ZeroSync, Alpen Labs, Chainway Labs and Layer 1 Foundaton. Its formal verification BitVM has brought new security and technical standards to the Bitcoin ecosystem. At the same time, Nubit will continue to promote the development of secure and verifiable Bitcoin native computing with the funding of Starkware and Fractal Bitcoin.

Everything is difficult at the beginning. The Bitcoin ecosystem brought by BitVM is still in its infancy, but the deep collaboration and innovation between early projects will not only provide strong guarantees for the security of complex computing, but also open up unlimited possibilities for the future of Bitcoin. A new era of Bitcoin that everyone can trust and everyone can participate in is coming.