Muodollinen vahvistus? Mikä se on? Opi lisää 🧵
Lohkoketjuissa on biljoonia dollareita. Yksi konsensusvirhe = välitön tyhjennys. Testaus voi löytää virheitä, mutta ei voi todistaa, että ne ovat mahdottomia. DAG-pohjaisten protokollien muodollinen vahvistus muuttaa tämän pelin.
Muodollinen verifiointi mallintaa protokollan tilakoneeksi ja antaa todistajan tarkistaa perusteellisesti jokaisen siirtymän – ei vain testinäytteen.
Vaikea osa? Todisteet ovat hitaita kirjoittaa. Sonicin oivallus: jaa protokollat uudelleenkäytettäviksi rakennuspalikoiksi sen sijaan, että keksisit todisteita joka kerta uudelleen.
Sonic Labs julkaisi juuri avoimen lähdekoodin TLA+-kirjaston, joka matemaattisesti todistaa turvallisuuden DAG-Riderille, Hashgraphille, Bullsharkille, Alephille ja muille – ei maksumuuria, ei salassapitosopimuksia.
Dijkstra: "Ohjelmatestaus voi osoittaa bugien olemassaolon, mutta ei koskaan niiden puuttumista." Todisteet antavat sinulle poissaolo-osan.
Kirjasto jakaa asiat kahteen osaan:
• DAG-rakentaminen 🌳
• Järjestys / johtajan valinta 🗳️
Jokaisella lohkolla on oma spesifikaatio + konetarkistettu todistus.
Kesti ~14 henkilökuukautta 5 tutkijalta mallintaa 5 protokollaa. Kuudennen lisääminen vie nyt päiviä, ei kuukausia.
Työ debytoi NASA Formal Methods 2025 -tapahtumassa. Jos se on tarpeeksi kestävä raketeille, se on luultavasti hyvä Sonicille!
Varoitus: nämä todisteet kattavat turvallisuuden (ei haarukoita, ei kaksinkertaisia kuluja). Ne eivät korjaa elävyyttä tai taloudellisia hyökkäyksiä – mutta kokonaisten turvallisuusvirheluokkien pyyhkiminen pois on silti valtava voitto.
TALLIUM; DR – Auditoinnin tarkistuslistat ovat 2020. Koottavat avoimen lähdekoodin todistukset ovat vuosi 2025. Tehdään "todistettavasti turvallisesta" oletusarvo kryptossa.
Blogin →
Koodi →
4,84 t.
35
Tällä sivulla näytettävä sisältö on kolmansien osapuolten tarjoamaa. Ellei toisin mainita, OKX ei ole lainatun artikkelin / lainattujen artikkelien kirjoittaja, eikä OKX väitä olevansa materiaalin tekijänoikeuksien haltija. Sisältö on tarkoitettu vain tiedoksi, eikä se edusta OKX:n näkemyksiä. Sitä ei ole tarkoitettu minkäänlaiseksi suositukseksi, eikä sitä tule pitää sijoitusneuvontana tai kehotuksena ostaa tai myydä digitaalisia varoja. Siltä osin kuin yhteenvetojen tai muiden tietojen tuottamiseen käytetään generatiivista tekoälyä, tällainen tekoälyn tuottama sisältö voi olla epätarkkaa tai epäjohdonmukaista. Lue aiheesta lisätietoa linkitetystä artikkelista. OKX ei ole vastuussa kolmansien osapuolten sivustojen sisällöstä. Digitaalisten varojen, kuten vakaakolikoiden ja NFT:iden, omistukseen liittyy suuri riski, ja niiden arvo voi vaihdella merkittävästi. Sinun tulee huolellisesti harkita, sopiiko digitaalisten varojen treidaus tai omistus sinulle taloudellisessa tilanteessasi.