形式验证？这是什么？了解更多 🧵
数万亿美元存储在区块链中。一个共识漏洞 = 立即耗尽。测试可以发现漏洞，但无法证明它们是不可能的。基于DAG的协议的形式验证改变了这一游戏。
形式验证将协议建模为状态机，并允许证明者对每个转换进行全面检查，而不仅仅是测试样本。
难点是什么？证明的编写速度很慢。Sonic 的见解是：将协议分解为可重用的构建块，而不是每次都重新发明证明。
Sonic Labs刚刚开源了一个TLA+库，该库为DAG-Rider、Hashgraph、Bullshark、Aleph等提供数学安全证明——没有付费墙，没有保密协议。
Dijkstra：“程序测试可以显示出存在错误，但永远无法证明它们的不存在。” 证明给你提供了不存在的部分。
该库将事物分为两部分：
• DAG 构建 🌳
• 排序 / 领导者选举 🗳️
每个区块都有自己的规范 + 机器检查的证明。
建模5个协议花费了大约14人月，涉及5名研究人员。现在添加第6个只需几天，而不是几个月。
这项工作在2025年NASA正式方法会议上首次亮相。如果它足够稳健用于火箭，那么它可能也适用于Sonic！
警告：这些证明涵盖了安全性（没有分叉，没有双重支付）。它们并不能解决活跃性或经济攻击——但消除整个类别的安全漏洞仍然是一个巨大的胜利。
简而言之——审计清单是2020年的事。可组合的开源证明是2025年的事。让我们把“可证明安全”作为加密货币的默认标准。
博客 →
代码 →
4,821
35
本页面内容由第三方提供。除非另有说明，欧易不是所引用文章的作者，也不对此类材料主张任何版权。该内容仅供参考，并不代表欧易观点，不作为任何形式的认可，也不应被视为投资建议或购买或出售数字资产的招揽。在使用生成式人工智能提供摘要或其他信息的情况下，此类人工智能生成的内容可能不准确或不一致。请阅读链接文章，了解更多详情和信息。欧易不对第三方网站上的内容负责。包含稳定币、NFTs 等在内的数字资产涉及较高程度的风险，其价值可能会产生较大波动。请根据自身财务状况，仔细考虑交易或持有数字资产是否适合您。