Formální ověření? Co to je? Víc se uč 🧵
V blockchainech leží biliony dolarů. Jedna konsensuální chyba = okamžité vyčerpání. Testování může najít chyby, ale nemůže prokázat, že jsou nemožné. Formální verifikace protokolů založených na DAG tuto hru mění.
Formální verifikace modeluje protokol jako stavový automat a umožňuje dokazovateli vyčerpávajícím způsobem kontrolovat každý přechod – nejen testovací vzorek.
A co je na tom nejtěžší? Nátisky se píší pomalu. Sonicův postřeh: rozdělte protokoly na opakovaně použitelné stavební bloky místo toho, abyste pokaždé znovu vynalézali důkazy.
Společnost Sonic Labs právě otevřela knihovnu TLA+, která matematicky dokazuje bezpečnost pro DAG-Rider, Hashgraph, Bullshark, Aleph a další – žádný paywall, žádné NDA.
Dijkstra: "Testování programu může ukázat přítomnost chyb, ale nikdy ne jejich nepřítomnost." Důkazy vám poskytnou část nepřítomnosti.
Knihovna rozděluje věci na dvě části:
• Konstrukce 🌳 DAG
• Objednávka / volba 🗳️ lídra
Každý blok má svou vlastní specifikaci + strojově kontrolovaný důkaz.
Trvalo ~14 člověkoměsíců u 5 výzkumníků, než bylo vytvořeno 5 protokolů. Přidání 6. nyní trvá dny, ne měsíce.
Práce debutovala na NASA Formal Methods 2025. Pokud je dostatečně robustní pro rakety, je pravděpodobně dobrý pro Sonica!
Upozornění: tyto důkazy pokrývají bezpečnost (žádné vidličky, žádné dvojité výdaje). Neopravují živost ani ekonomické útoky – ale vymazání celých tříd bezpečnostních chyb je stále obrovskou výhrou.
TL; DR — Kontrolní seznamy auditu jsou 2020. Skládatelné, open-source důkazy jsou 2025. Udělejme "prokazatelně bezpečné" výchozím nastavením v kryptoměnách.
Blog →
Kód →
5,13 tis.
39
Obsah na této stránce poskytují třetí strany. Není-li uvedeno jinak, společnost OKX není autorem těchto informací a nenárokuje si u těchto materiálů žádná autorská práva. Obsah je poskytován pouze pro informativní účely a nevyjadřuje názory společnosti OKX. Nejedná se o doporučení jakéhokoli druhu a nemělo by být považováno za investiční poradenství ani nabádání k nákupu nebo prodeji digitálních aktiv. Tam, kde se k poskytování souhrnů a dalších informací používá generativní AI, může být vygenerovaný obsah nepřesný nebo nekonzistentní. Další podrobnosti a informace naleznete v připojeném článku. Společnost OKX neodpovídá za obsah, jehož hostitelem jsou externí weby. Držená digitální aktiva, včetně stablecoinů a tokenů NFT, zahrnují vysokou míru rizika a mohou značně kolísat. Měli byste pečlivě zvážit, zde je pro vás obchodování s digitálními aktivy nebo jejich držení vhodné z hlediska vaší finanční situace.