A equipe por trás da blockchain de alto desempenho Layer 1 Sonic, Sonic Labs, introduziu uma biblioteca de verificação formal projetada para aprimorar a segurança em protocolos de consenso baseados em DAG. Liderada pelo Diretor de Pesquisa Dr. Bernhard Scholz, a biblioteca tem como objetivo fornecer prova matemática de segurança para blockchains de Grafos Acíclicos Dirigidos (DAG), incluindo a própria rede compatível com EVM da Sonic.
Desenvolvida em parceria com pesquisadores da Universidade de Sydney e INRIA, a biblioteca de código aberto é construída usando o assistente de provas TLA+. Oferece um framework modular e reutilizável que simplifica o processo de modelagem e verificação de mecanismos de consenso baseados na arquitetura DAG.
A biblioteca de verificação apresenta provas formais para vários protocolos existentes baseados em DAG, como DAG-Rider, Cordial Miner, Bullshark, Hashgraph e Aleph. O protocolo proprietário da Sonic também foi verificado como um derivado dentro deste framework. A pesquisa foi apresentada pela primeira vez na conferência NASA Formal Methods 2025, realizada em Williamsburg, Virgínia, de 11 a 13 de junho, e representa um avanço notável nos padrões de verificação de blockchain.
“No blockchain, falhas de segurança muitas vezes decorrem de suposições que não são testadas até que seja tarde demais”, disse Dr. Bernhard Scholz, Diretor de Pesquisa da Sonic Labs, em uma declaração escrita. “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,” acrescentou.
À medida que o valor da blockchain aumenta, a Sonic Labs lança um Framework de Verificação Formal para garantir a segurança e confiabilidade do protocolo.
À medida que o valor garantido pelas redes blockchain continua a crescer, o impacto potencial das vulnerabilidades nos protocolos de consenso torna-se cada vez mais significativo, com riscos que incluem gasto duplo e estados de livro-razão inconsistentes. Testes convencionais e auditorias de código são limitados em sua capacidade de garantir sistemas livres de bugs. Em resposta, um método de verificação formal foi aplicado pela Sonic Labs, utilizando provas matemáticas para confirmar a segurança do protocolo em todas as condições possíveis.
Esta abordagem não apenas valida os protocolos de consenso existentes, mas também auxilia os desenvolvedores que estão projetando novos modelos baseados em Grafos Acíclicos Dirigidos ou adaptando os atuais. O método está sendo implementado atualmente para verificar formalmente que a blockchain Sonic não pode exibir comportamentos inseguros, estabelecendo a confiabilidade do protocolo por meio da validação matemática.
Ao tornar a biblioteca de verificação amplamente disponível, a iniciativa fornece aos desenvolvedores de blockchain recursos para construir sistemas comprovadamente seguros. Espera-se que isso melhore a resiliência geral dos ecossistemas descentralizados e reduza as demandas de recursos normalmente associadas à verificação de protocolos de consenso.
O post Sonic Labs Revela Biblioteca de Verificação Formal Para Protocolos de Consenso DAG apareceu primeiro no Metaverse Post.
