O white paper do Bitcoin foi lançado em 31 de outubro de 2008, quando Satoshi Nakamoto publicou o white paper do Bitcoin (Bitcoin: um sistema de dinheiro eletrônico ponto a ponto) no site da P2P foundation, hoje celebrando seu 16º aniversário.
O preço inicial de transação do Bitcoin era de 0,0008 dólares, e agora valorizou mais de 90 milhões de vezes.
É amplamente conhecido que o Bitcoin redefiniu a maneira como as pessoas confiam na transferência de valor. Em uma rede descentralizada, a confiança é substituída pela tecnologia, e cada transação é verificada pela própria rede. No entanto, com o surgimento das finanças descentralizadas (DeFi) e contratos inteligentes, a introdução segura de cálculos mais complexos na rede Bitcoin para construir conteúdos mais ricos tornou-se um novo desafio.
O que é BitVM?
Em dezembro de 2023, Robin Linus, responsável pelo projeto ZeroSync, publicou um white paper intitulado (BitVM: Compute Anything On Bitcoin), provocando reflexões sobre como aumentar a programabilidade do Bitcoin.
A introdução do BitVM trouxe a capacidade de executar cálculos complexos fora da cadeia e verificar resultados na cadeia, expandindo enormemente suas funcionalidades. De forma mais direta, o BitVM é uma solução que permite a execução de cálculos complexos e contratos inteligentes na rede Bitcoin. É uma solução que pode implementar complete Turing sem alterar o consenso da rede Bitcoin. Ao se tornar Turing-completo, a blockchain do Bitcoin pode teoricamente ser usada para expandir as funcionalidades do Bitcoin, muito além da visão do "sistema de dinheiro eletrônico ponto a ponto" apresentada pela primeira vez no white paper do Bitcoin. Ele permite que os usuários criem aplicativos em cima do Bitcoin — de forma semelhante às funcionalidades já implementadas em outras plataformas como Ethereum — ao mesmo tempo que mantém a alta segurança e descentralização que o Bitcoin é conhecido.
Em resumo, o BitVM pode permitir que o ecossistema Bitcoin não apenas atenda às necessidades de transação, mas também crie DApps mais complexos na camada BTC. Ao mesmo tempo, preserva a segurança e a descentralização do Bitcoin.
No entanto, a complexidade geralmente vem acompanhada de riscos; como garantir a segurança desses cálculos complexos tornou-se um problema urgente a ser resolvido.
Atualmente, há muitas equipes dedicadas à pesquisa e desenvolvimento do BitVM, incluindo ZeroSync, fundada pelo criador do BitVM, Robin, o projeto nativo de Bitcoin Nubit criado pelo Prof. Yu Feng da Universidade da Califórnia, Santa Bárbara, Alpen Labs, que se dedica à expansão ZK do Bitcoin, Chainway Labs, focada em ZK Rollup do Bitcoin, Citrea, e Fiamma, além da Layer 1 Foundation, onde está o fundador do BRC20, Domo.
Atualmente, a Nubit, em conjunto com ZeroSync, Alpen Labs, Chainway Labs e a Layer 1 Foundation liderada pela Domo, publicou um artigo em 31 de outubro (Push-Button Verification for BitVM Implementations), completando e lançando a ferramenta de verificação formal do BitVM. No artigo, a Nubit fornece uma garantia adicional de segurança para as aplicações do BitVM através de provas matemáticas automatizadas, permitindo que desenvolvedores e usuários construam e utilizem aplicações com confiança.
O que é verificação formal? Como ela ajuda a garantir a segurança do BitVM?
No artigo de Robin, o BitVM introduziu um sistema que permite que qualquer cálculo seja verificado na blockchain do Bitcoin, sem afetar sua segurança ou alterar a rede. No entanto, o desenvolvimento do sistema e a construção de aplicações baseadas nele muitas vezes requerem revisão de código por especialistas. Em um ecossistema como o Bitcoin, que exige alta segurança, a revisão manual é tanto demorada quanto suscetível a erros. A verificação formal (Formal Verification), através de operações matemáticas puras, pode validar automaticamente se a lógica do programa atende às expectativas, proporcionando segurança ao sistema global do BitVM.
Imagine que você está implantando um contrato inteligente no Bitcoin que envolve transações entre várias partes. Para garantir que o contrato seja executado corretamente em várias circunstâncias, métodos tradicionais podem exigir testes repetidos de cada possibilidade. Mas com a ferramenta de verificação formal (Formal Verification), provas matemáticas automaticamente verificarão a correção do contrato, aumentando significativamente a segurança do funcionamento do sistema.
Os desafios especiais do BitVM: a complexidade dos contratos inteligentes e as limitações dos scripts do Bitcoin
Diferente de blockchains como Ethereum, que possuem completude Turing (Turing-complete), a linguagem de script do Bitcoin é limitada por considerações de segurança e não pode executar cálculos complexos diretamente. O BitVM implementou as funcionalidades básicas dos contratos inteligentes do Bitcoin através da execução fora da cadeia e verificação em cima da cadeia. Em outras palavras, todos os cálculos complexos são realizados fora da cadeia, e apenas os resultados são verificados na cadeia, aliviando significativamente a carga da cadeia do Bitcoin. No entanto, essa inovação trouxe uma dificuldade de implementação significativa.
Primeiro, o design do BitVM inclui uma grande quantidade de operações de pilha e cálculos de registradores, que precisam ser implementados e verificados de forma eficiente nos scripts não Turing-completos do Bitcoin. Por exemplo, para garantir que a execução do contrato possa julgar corretamente se um valor é positivo ou negativo, uma função comum é is_positive, que verifica o bit mais significativo para determinar o sinal. No entanto, em uma versão anterior, a função is_positive erroneamente classificou 0 como um número positivo devido a um desvio no cálculo, esse pequeno erro pode levar a uma grave discrepância na execução do contrato e até mesmo resultar em perdas econômicas potenciais.
Fonte da imagem: (Push-Button Verification for BitVM Implementations)
Através da verificação formal (Formal Verification), a ferramenta da Nubit pode automaticamente verificar lógicas de cálculo semelhantes antes da implantação do código, garantindo que todos os caminhos de execução atendam às expectativas. Aqui, a equipe da Nubit projetou uma DSL (linguagem específica de domínio) baseada em registradores, que transforma as complexas operações de pilha dos scripts do Bitcoin em operações de registrador mais fáceis de verificar, simplificando assim o processo de desenvolvimento e verificação. Além disso, para cálculos repetitivos em loop, essa DSL introduziu 'invariantes de loop' para efetivamente reduzir cálculos repetidos no código e diminuir a dificuldade de verificação.
Fonte da imagem: (Push-Button Verification for BitVM Implementations)
Efeito de verificação: eficiência da verificação formal automatizada
De acordo com o artigo, a ferramenta de verificação formal (Formal Verification) da Nubit foi amplamente testada em 98 benchmarks de verificadores SNARK do BitVM, com uma taxa de sucesso de verificação de 94%, e a maioria das tarefas de verificação pode ser concluída em segundos. Em comparação com a revisão manual tradicional, essa ferramenta não apenas aumenta a velocidade de verificação, mas também evita a possibilidade de erros humanos, proporcionando garantias para a execução confiável dos contratos inteligentes do BitVM no Bitcoin.
Esse resultado demonstra que a verificação formal (Formal Verification) possui um alto valor prático nas aplicações complexas do Bitcoin, especialmente em aplicações BTCFi que exigem alta segurança, podendo efetivamente reduzir riscos.
BitVM e o ecossistema Bitcoin: expandindo o potencial dos contratos inteligentes do Bitcoin
Através da verificação formal (Formal Verification), a segurança do BitVM foi significativamente aprimorada, ajudando desenvolvedores a construir contratos e aplicações mais complexas no Bitcoin, enquanto permite que usuários desfrutem da alta segurança do ecossistema Bitcoin em aplicações de finanças descentralizadas e cross-chain. Como uma ferramenta inovadora do ecossistema Bitcoin, o BitVM estabelece uma base para a expansão do Bitcoin em aplicações complexas.
O Bitcoin nunca foi projetado como uma plataforma de cálculos complexos, mas sim focado na confiabilidade do armazenamento e transferência de valor. No entanto, com o lançamento do BitVM, o ecossistema Bitcoin está avançando em direção a contratos inteligentes e aplicações DeFi. Para o desenvolvimento de aplicações descentralizadas, a conclusão da verificação formal do BitVM não é apenas um avanço tecnológico, mas também representa um marco importante para o Bitcoin nas finanças descentralizadas e contratos inteligentes.
BitVM abre o futuro do ecossistema Bitcoin
Durante o desenvolvimento do BitVM, a Nubit trabalhou em estreita colaboração com equipes como ZeroSync, Alpen Labs, Chainway Labs e Layer 1 Foundaton, trazendo novos padrões de segurança e tecnologia para o ecossistema Bitcoin com a verificação formal do BitVM. Além disso, a Nubit continuará a promover o desenvolvimento de cálculos nativos do Bitcoin seguros e verificáveis, com o apoio da Starkware e Fractal Bitcoin.
Todo começo é difícil, o ecossistema Bitcoin trazido pelo BitVM ainda está em sua infância, mas a colaboração e inovação profundas entre projetos iniciais não só fornecerão uma forte garantia para a segurança do cálculo complexo, mas também abrirão possibilidades infinitas para o futuro do Bitcoin. Uma nova era do Bitcoin, onde todos podem confiar e participar, está chegando.
Este artigo é uma contribuição e não representa a opinião da BlockBeats.
