Sonic Labs revela biblioteca de verificação formal para protocolos de consenso DAG

Equipe por trás do blockchain de alto desempenho da Camada 1 Sonic, Laboratórios Sônicos 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 visa fornecer prova matemática de segurança para blockchains de Grafos Acíclicos Direcionados (DAG), incluindo a própria rede compatível com EVM da Sonic.

Desenvolvida em parceria com pesquisadores da Universidade de Sydney e do INRIA, a biblioteca de código aberto utiliza o assistente de prova TLA+. Ela oferece uma estrutura 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 diversos protocolos baseados em DAG existentes, como DAG-Rider, Cordial Miner, Bullshark, Hashgraph e Aleph. O protocolo proprietário da Sonic também foi verificado como um derivado dentro desta estrutura. 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.

“Em blockchain, falhas de segurança frequentemente decorrem de suposições que não são testadas até que seja tarde demais”, afirmou o Dr. Bernhard Scholz, Diretor de Pesquisa da Sonic Labs, em uma declaração por escrito. “Com esta biblioteca, estamos passando da esperança para a comprovação, oferecendo as ferramentas para verificar com certeza matemática que um protocolo se comportará com segurança em todas as condições. Nosso objetivo é tornar a verificação formal acessível a todos os desenvolvedores de protocolos”, acrescentou.

Com o aumento do valor do blockchain, a Sonic Labs lança uma estrutura de verificação formal para garantir a segurança e a 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 gastos duplicados e estados inconsistentes do livro-razão. 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 por Laboratórios Sônicos , utilizando provas matemáticas para confirmar a segurança do protocolo em todas as condições possíveis.

Essa abordagem não apenas valida os protocolos de consenso existentes, mas também auxilia desenvolvedores que estão projetando novos modelos baseados em Grafos Acíclicos Direcionados ou adaptando os atuais. O método está sendo implementado para verificar formalmente se a blockchain Sonic não pode apresentar comportamento inseguro, estabelecendo a confiabilidade do protocolo por meio de validação matemática.

Ao disponibilizar a biblioteca de verificação abertamente, 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 a demanda por recursos normalmente associada à verificação do protocolo de consenso.