Verificação formal? O que é? Saiba mais 🧵
Trilhões de dólares estão em blockchains. Um bug de consenso = drenagem instantânea. Testes podem encontrar bugs, mas não conseguem provar que são impossíveis. A verificação formal para protocolos baseados em DAG muda esse jogo.
A verificação formal modela um protocolo como uma máquina de estados e permite que um provador verifique exaustivamente cada transição—não apenas uma amostra de teste.
A parte difícil? As provas são lentas de escrever. A visão do Sonic: dividir os protocolos em blocos de construção reutilizáveis em vez de reinventar as provas a cada vez.
A Sonic Labs acaba de tornar open-source uma biblioteca TLA+ que prova matematicamente a segurança para DAG-Rider, Hashgraph, Bullshark, Aleph e mais—sem paywall, sem NDAs.
Dijkstra: “Os testes de programa podem mostrar a presença de erros, mas nunca a sua ausência.” As provas dão-lhe a parte da ausência.
A biblioteca divide as coisas em duas:
• Construção de DAG 🌳
• Ordenação / eleição de líder 🗳️
Cada bloco tem sua própria especificação + prova verificada por máquina.
Levou cerca de 14 meses-pessoa entre 5 investigadores para modelar 5 protocolos. Adicionar um 6º agora leva dias, não meses.
O trabalho estreou na NASA Formal Methods 2025. Se é robusto o suficiente para foguetes, provavelmente é bom para o Sonic!
Aviso: estas provas cobrem a segurança (sem forks, sem gastos duplos). Elas não resolvem problemas de disponibilidade ou ataques econômicos—mas eliminar classes inteiras de bugs de segurança ainda é uma grande vitória.
Resumo — Listas de verificação de auditoria são de 2020. Provas composáveis e de código aberto são de 2025. Vamos fazer de "provavelmente seguro" o padrão no cripto.
Blog →
Código →
4,83 mil
35
O conteúdo apresentado nesta página é fornecido por terceiros. Salvo indicação em contrário, a OKX não é o autor dos artigos citados e não reivindica quaisquer direitos de autor nos materiais. O conteúdo é fornecido apenas para fins informativos e não representa a opinião da OKX. Não se destina a ser um endosso de qualquer tipo e não deve ser considerado conselho de investimento ou uma solicitação para comprar ou vender ativos digitais. Na medida em que a IA generativa é utilizada para fornecer resumos ou outras informações, esse mesmo conteúdo gerado por IA pode ser impreciso ou inconsistente. Leia o artigo associado para obter mais detalhes e informações. A OKX não é responsável pelo conteúdo apresentado nos sites de terceiros. As detenções de ativos digitais, incluindo criptomoedas estáveis e NFTs, envolvem um nível de risco elevado e podem sofrer grandes flutuações. Deve considerar cuidadosamente se o trading ou a detenção de ativos digitais é adequado para si à luz da sua condição financeira.