Verificação formal? O que é? Saiba Mais 🧵
Trilhões de dólares estão em blockchains. Um bug de consenso = drenagem instantânea. Os testes podem encontrar bugs, mas não podem 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 estado e permite que um provador verifique exaustivamente cada transição - não apenas uma amostra de teste.
A parte difícil? As provas demoram a ser escritas. O insight do Sonic: quebrar os protocolos em blocos de construção reutilizáveis em vez de reinventar as provas a cada vez.
A Sonic Labs acaba de abrir o código de uma biblioteca TLA+ que prova matematicamente a segurança para DAG-Rider, Hashgraph, Bullshark, Aleph e muito mais - sem paywall, sem NDAs.
Dijkstra: "Os testes do programa podem mostrar a presença de bugs, mas nunca sua ausência." As provas fornecem a parte da ausência.
A biblioteca divide as coisas em duas:
• Construção 🌳 DAG
• Ordenação / eleição 🗳️ de líder
Cada bloco tem sua própria especificação + prova verificada por máquina.
Demorou ~ 14 pessoas-mês em 5 pesquisadores para modelar 5 protocolos. Adicionar um 6º agora leva dias, não meses.
O trabalho estreou no NASA Formal Methods 2025. Se for robusto o suficiente para foguetes, provavelmente é bom para o Sonic!
Advertência: essas provas cobrem a segurança (sem garfos, sem gastos duplos). Eles não consertam ataques econômicos ou de vivacidade - mas eliminar classes inteiras de bugs de segurança ainda é uma grande vitória.
TL; DR — As listas de verificação de auditoria são 2020. As provas de código aberto combináveis são 2025. Vamos tornar "comprovadamente seguro" o padrão em criptomoedas.
Blog →
Código →
4,83 mil
35
O conteúdo desta página é fornecido por terceiros. A menos que especificado de outra forma, a OKX não é a autora dos artigos mencionados e não reivindica direitos autorais sobre os materiais apresentados. O conteúdo tem um propósito meramente informativo e não representa as opiniões da OKX. Ele não deve ser interpretado como um endosso ou aconselhamento de investimento de qualquer tipo, nem como uma recomendação para compra ou venda de ativos digitais. Quando a IA generativa é utilizada para criar resumos ou outras informações, o conteúdo gerado pode apresentar imprecisões ou incoerências. Leia o artigo vinculado para mais detalhes e informações. A OKX não se responsabiliza pelo conteúdo hospedado em sites de terceiros. Possuir ativos digitais, como stablecoins e NFTs, envolve um risco elevado e pode apresentar flutuações significativas. Você deve ponderar com cuidado se negociar ou manter ativos digitais é adequado para sua condição financeira.