Verifica formale? Cos'è? Scopri di più 🧵
Trilioni di dollari sono bloccati nelle blockchain. Un bug di consenso = drenaggio istantaneo. I test possono trovare bug ma non possono dimostrare che siano impossibili. La verifica formale per i protocolli basati su DAG cambia le regole del gioco.
La verifica formale modella un protocollo come una macchina a stati e consente a un dimostratore di controllare esaustivamente ogni transizione, non solo un campione di test.
La parte difficile? Le prove sono lente da scrivere. L'intuizione di Sonic: suddividere i protocolli in blocchi di costruzione riutilizzabili invece di reinventare le prove ogni volta.
Sonic Labs ha appena reso open source una libreria TLA+ che dimostra matematicamente la sicurezza per DAG-Rider, Hashgraph, Bullshark, Aleph e altro—nessun paywall, nessun NDA.
Dijkstra: “Il testing dei programmi può mostrare la presenza di bug, ma mai la loro assenza.” Le dimostrazioni ti danno la parte dell'assenza.
La libreria divide le cose in due:
• Costruzione del DAG 🌳
• Ordinamento / elezione del leader 🗳️
Ogni blocco ha la propria specifica + prova verificata dalla macchina.
Ci sono voluti circa 14 mesi-uomo tra 5 ricercatori per modellare 5 protocolli. Aggiungere un sesto ora richiede giorni, non mesi.
Il lavoro è debuttato al NASA Formal Methods 2025. Se è abbastanza robusto per i razzi, probabilmente è buono anche per Sonic!
Avvertenza: queste prove coprono la sicurezza (niente fork, niente doppie spese). Non risolvono problemi di vivacità o attacchi economici, ma eliminare intere classi di bug di sicurezza è comunque un grande successo.
TL;DR — Le liste di controllo per le audit sono del 2020. Le prove composabili e open-source sono del 2025. Rendiamo "provabilmente sicuro" il default nel crypto.
Blog →
Codice →
4.042
32
Il contenuto di questa pagina è fornito da terze parti. Salvo diversa indicazione, OKX non è l'autore degli articoli citati e non rivendica alcun copyright sui materiali. Il contenuto è fornito solo a scopo informativo e non rappresenta le opinioni di OKX. Non intende essere un'approvazione di alcun tipo e non deve essere considerato un consiglio di investimento o una sollecitazione all'acquisto o alla vendita di asset digitali. Nella misura in cui l'IA generativa viene utilizzata per fornire riepiloghi o altre informazioni, tale contenuto generato dall'IA potrebbe essere impreciso o incoerente. Leggi l'articolo collegato per ulteriori dettagli e informazioni. OKX non è responsabile per i contenuti ospitati su siti di terze parti. Gli holding di asset digitali, tra cui stablecoin e NFT, comportano un elevato grado di rischio e possono fluttuare notevolmente. Dovresti valutare attentamente se effettuare il trading o detenere asset digitali è adatto a te alla luce della tua situazione finanziaria.