Formale Verifikation? Was ist das? Erfahren Sie mehr 🧵
Billionen von Dollar liegen in Blockchains. Ein Konsensfehler = sofortiger Abfluss. Tests können Fehler finden, können aber nicht beweisen, dass sie unmöglich sind. Die formale Verifikation für DAG-basierte Protokolle verändert dieses Spiel.
Die formale Verifikation modelliert ein Protokoll als Zustandsmaschine und ermöglicht es einem Beweiser, jeden Übergang erschöpfend zu überprüfen – nicht nur eine Testprobe.
Der schwierige Teil? Beweise sind langsam zu schreiben. Sonics Einsicht: Teile Protokolle in wiederverwendbare Bausteine auf, anstatt jedes Mal Beweise neu zu erfinden.
Sonic Labs hat gerade eine TLA+-Bibliothek als Open Source veröffentlicht, die mathematisch die Sicherheit für DAG-Rider, Hashgraph, Bullshark, Aleph und mehr beweist – keine Bezahlschranke, keine NDAs.
Dijkstra: „Programmtests können das Vorhandensein von Fehlern zeigen, aber niemals deren Abwesenheit.“ Beweise geben dir den Abwesenheitsteil.
Die Bibliothek teilt die Dinge in zwei:
• DAG-Konstruktion 🌳
• Reihenfolge / Wahl des Leiters 🗳️
Jeder Block hat seine eigene Spezifikation + maschinengeprüfter Nachweis.
Es dauerte etwa 14 Personenmonate, um 5 Protokolle mit 5 Forschern zu modellieren. Das Hinzufügen eines 6. Protokolls dauert jetzt Tage, nicht Monate.
Die Arbeit debütierte bei den NASA Formal Methods 2025. Wenn es robust genug für Raketen ist, ist es wahrscheinlich auch gut für Sonic!
Vorbehalt: Diese Nachweise decken die Sicherheit ab (keine Forks, keine Doppel-Ausgaben). Sie beheben jedoch nicht die Liveness- oder wirtschaftlichen Angriffe – aber das Ausmerzen ganzer Klassen von Sicherheitsfehlern ist dennoch ein großer Gewinn.
TL;DR — Prüfungschecklisten sind 2020. Komponierbare, Open-Source-Beweise sind 2025. Lassen Sie uns "nachweislich sicher" zum Standard in der Krypto machen.
Blog →
Code →
5.127
39
Der Inhalt dieser Seite wird von Dritten bereitgestellt. Sofern nicht anders angegeben, ist OKX nicht der Autor der zitierten Artikel und erhebt keinen Anspruch auf das Urheberrecht an den Materialien. Der Inhalt wird ausschließlich zu Informationszwecken bereitgestellt und gibt nicht die Ansichten von OKX wieder. Er stellt keine wie auch immer geartete Befürwortung dar und sollte nicht als Anlageberatung oder Aufforderung zum Kauf oder Verkauf digitaler Vermögenswerte betrachtet werden. Soweit generative KI zur Bereitstellung von Zusammenfassungen oder anderen Informationen verwendet wird, können solche KI-generierten Inhalte ungenau oder inkonsistent sein. Bitte lesen Sie den verlinkten Artikel für weitere Details und Informationen. OKX ist nicht verantwortlich für Inhalte, die auf Websites Dritter gehostet werden. Der Besitz digitaler Vermögenswerte, einschließlich Stablecoins und NFTs, ist mit einem hohen Risiko verbunden und kann starken Schwankungen unterliegen. Sie sollten sorgfältig abwägen, ob der Handel mit oder der Besitz von digitalen Vermögenswerten angesichts Ihrer finanziellen Situation für Sie geeignet ist.