形式化驗證？這是什麼？瞭解更多資訊 🧵
數萬億美元位於區塊鏈中。一個共識錯誤 = 立即耗盡。測試可以發現 bug，但不能證明它們是不可能的。基於 DAG 的協定的形式化驗證改變了這種局面。
形式化驗證將協定建模為狀態機，並允許證明者詳盡地檢查每個轉換，而不僅僅是測試樣本。
難點是什麼？證明寫得很慢。Sonic 的見解：將協定分解為可重用的構建塊，而不是每次都重新發明證明。
索尼克實驗室剛剛開源了一個TLA+庫，該庫在數學上證明瞭DAG-Rider、Hashgraph、Bullshark、Aleph等的安全性——沒有付費牆，沒有保密協定。
Dijkstra： “程序測試可以顯示 bug 的存在，但永遠不會顯示 bug 的缺失。”證明給你缺席的部分。
該庫將內容一分為二：
• DAG 結構 🌳
• 排序/領導選舉 🗳️
每個塊都有自己的規格 + 機器檢查的證明。
5 名研究人員花了 ~14 個人月來類比 5 個方案。現在添加第 6 個應用程式需要幾天，而不是幾個月。
這項工作在 NASA Formal Methods 2025 上首次亮相。如果它足夠堅固，可以發射火箭，那可能對索尼克有好處！
警告：這些證明涵蓋安全性（沒有分叉，沒有雙花）。它們不修復活體攻擊或經濟攻擊，但消除所有類別的安全漏洞仍然是一個巨大的勝利。
TL;DR — 審計清單是 2020 年。可組合的開源證明是 2025 年。讓我們將 「provably safe」 作為 crypto 的預設設置。
博客 →
代碼 →
4,812
35
本頁面內容由第三方提供。除非另有說明，OKX 不是所引用文章的作者，也不對此類材料主張任何版權。該內容僅供參考，並不代表 OKX 觀點，不作為任何形式的認可，也不應被視為投資建議或購買或出售數字資產的招攬。在使用生成式人工智能提供摘要或其他信息的情況下，此類人工智能生成的內容可能不準確或不一致。請閱讀鏈接文章，瞭解更多詳情和信息。OKX 不對第三方網站上的內容負責。包含穩定幣、NFTs 等在內的數字資產涉及較高程度的風險，其價值可能會產生較大波動。請根據自身財務狀況，仔細考慮交易或持有數字資產是否適合您。