A Sonic Labs, o braço de pesquisa por trás da blockchain de alto desempenho layer-1 Sonic, hoje revelou uma biblioteca de verificação formal de código aberto projetada especificamente para protocolos de consenso de Grafo Acíclico Direcionado (DAG). Liderada pelo Diretor de Pesquisa Dr. Bernhard Scholz, a nova caixa de ferramentas foi anos em desenvolvimento e promete trazer certeza matemática a uma classe de designs de blockchain há muito valorizados por sua capacidade, mas frequentemente criticados por garantias de segurança não verificadas.

Apresentada pela primeira vez esta semana na NASA Formal Methods 2025 em Williamsburg, Virginia, a biblioteca utiliza o assistente de provas TLA+ — o mesmo rigoroso framework utilizado para validar algoritmos críticos de aeroespacial e sistemas distribuídos — para oferecer aos designers de protocolos componentes reutilizáveis e modulares para construir e verificar consenso baseado em DAG sob todas as condições de rede possíveis.

Scholz disse: “Na blockchain, falhas de segurança muitas vezes decorrem de suposições que não são testadas até que seja tarde demais. Com esta biblioteca, estamos mudando de esperança para prova, oferecendo as ferramentas para verificar, com certeza matemática, que um protocolo se comportará de forma segura sob todas as condições. Nosso objetivo é tornar a verificação formal acessível a todos os desenvolvedores de protocolos.”

Colaboração com Lógicos de Destaque

A Sonic Labs desenvolveu a biblioteca em estreita parceria com lógicos da Universidade de Sydney e do instituto de pesquisa INRIA da França. Nos últimos dois anos, a equipe conjunta codificou as propriedades de segurança essenciais de cinco protocolos DAG proeminentes — DAG-Rider, Cordial Miner, Bullshark, Hashgraph e Aleph — e então demonstrou como as próprias regras de consenso da Sonic se encaixam naturalmente como um modelo derivado.

Construindo sobre essas fundações, os desenvolvedores agora podem misturar e combinar módulos verificados — digamos, um componente de eleição de líder ou um gadget de finalização — em vez de elaborar cada prova do zero. O resultado: o que antes levava meses de provas teóricas exaustivas agora pode ser montado em dias, reduzindo drasticamente a barreira para pesquisas de blockchain formalmente verificadas.

Por que a Verificação Formal é Importante

As blockchains hoje protegem trilhões de dólares em ativos digitais, no entanto, a defesa tradicional de auditorias e testnets não pode garantir a ausência de sutis bugs de consenso que possam permitir que um atacante gaste fundos duas vezes ou bifurque o livro razão. A verificação formal trata a especificação do protocolo como um teorema matemático: se a prova é válida, a garantia de segurança também é.

Imagine enviar um foguete ao espaço sem verificar seu sistema de orientação. As blockchains não são menos críticas. A Sonic Labs está dando aos desenvolvedores a bússola para traçar um caminho de voo livre de quedas ocultas. A Sonic Labs já aplicou sua biblioteca à própria rede compatível com EVM da Sonic, provando que cenários perigosos — como dois blocos conflitantes alcançando a finalização — não podem ocorrer. A equipe planeja continuar implementando verificações formais nas atualizações de protocolo e extensões de terceiros que estão por vir.

Capacitando o Ecossistema Web3

Ao tornar a biblioteca de código aberto no GitHub, a Sonic Labs espera provocar uma onda de colaboração entre equipes de blockchain em todo o mundo. Desenvolvedores que experimentam designs DAG novos — ou ajustam protocolos existentes — agora podem contar com módulos de verificação testados em batalha, reduzindo tanto o tempo quanto o custo para pesquisas acadêmicas e implementações de produção.

Este anúncio chega em meio a um crescimento rápido para a própria rede Sonic. Com finalização em sub-segundos e uma capacidade de até 400.000 transações por segundo, a Sonic reivindicou seu lugar como a blockchain EVM mais rápida do mercado. Um novo modelo de “Monetização de Taxas” paga aos desenvolvedores 90% das taxas de rede geradas por seus aplicativos descentralizados — uma estrutura de incentivo emprestada da divisão de receita de anúncios da Web 2 que já atraiu vários projetos DeFi em busca de infraestrutura previsível e de alto desempenho.

Com a verificação formal agora parte de sua caixa de ferramentas, a Sonic Labs visa consolidar ainda mais a reputação da Sonic como uma plataforma de pesquisa de ponta e uma cadeia de produção sólida. Para designers de protocolos e arquitetos de blockchain, a nova biblioteca pode muito bem definir o padrão de como a segurança é incorporada nos sistemas descentralizados de amanhã.