Sonic Labs加强区块链安全，推出新的形式化验证库 | Bitcoinist.com

![](http://img-cdn.gateio.im/social/moments-7626b41da48d2a715b0aa25c7df79122019283746574839201 受信任的编辑内容，由领先行业专家和经验丰富的编辑审核。广告披露 Sonic Labs 一直在践行其名称，在实验室中努力工作，撰写一篇新的研究论文。这不仅仅是一份理论文件：它在区块链共识领域产生了可实际应用的成果，Sonic Labs 开发的正式验证库现在已开源并可在 Github 上获取。

Sonic Labs团队当然最出名的是设计了Sonic Layer-1链，这个链是从Fantom的废墟中崛起的。Sonic使用DAG )有向无环图(作为其共识机制，而正是在这一领域，Labs团队可以理解地选择了集中他们的努力。尽管他们开发的后续验证库对Sonic的EVM网络有影响，但它同样适用于所有现有和未来的基于DAG的链，在这些链上，它有潜力通过防止错误的出现来显著增强安全性。

) Sonic Labs 对 DAG 进行了重新调整

区块链共识设计是需要大脑的东西，涉及到数学、密码学和博弈论等领域的研究者的专业知识。虽然Sonic Labs团队在这些领域受过良好的教育，但它还是请来了一些专家，帮助深入研究DAG，目标是使其可验证地安全。

与悉尼大学和INRIA的顶尖逻辑学家合作开发的这个库，利用TLA+证明助手提供模块化、可重用的组件。这些组件简化了开发人员的验证过程，使他们能够轻松地建模和确认基于DAG的协议的安全性。该库包含对主要协议的验证证明，如DAG-Rider、Cordial Miner、Bullshark、Hashgraph和Aleph，以及Sonic自己的共识协议被验证为衍生协议。

考虑到现在区块链生态系统中流通的价值，确保它们的安全对每个人来说都是有利的。然而，这说起来容易做起来难，因为标准审计程序绝不是万无一失的，漏洞悄然出现并最终被利用的情况并不鲜见，后果可能是灾难性的。

让区块链对每个人都更安全

Sonic Labs 的形式验证方法使用严格的数学证明来消除错误，确保协议在每种可想象的场景中都能可靠地执行。该库不仅验证现有协议，还使开发者能够设计新的基于 DAG 的系统或改进当前系统。Sonic Labs 已经应用其专有工具证明在 Sonic 区块链上不安全的行为在数学上是不可能的。

该库于2025年6月中旬在弗吉尼亚州威廉斯堡的NASA正式方法会议上首次展示，为区块链开发者的武器库增加了一种有价值的防御工具。随着模块化设计成为构建区块链的默认方式，安全风险潜入的风险上升。例如，许多区块链即服务提供商允许团队仅需几次点击即可创建和部署自定义网络。但如果他们在此过程中选择修改共识机制的参数，就有可能无意中引入安全漏洞。

这只是 Sonic Labs 的形式验证库具有明确应用的一个领域。但它在评估现有的基于 DAG 的链方面也有价值。漏洞常常在实际中潜藏多年，最好的情况是白帽子发现它并进行修补。最坏的情况是，它落入黑帽子的手中，黑帽子能够利用它。

正如Sonic Labs的首席研究官Bernhard Scholz博士总结的那样：“在区块链中，安全失败往往源于未经过测试的假设，直到为时已晚。借助这个库，我们正从希望转向证明，提供了以数学确定性验证协议在所有条件下安全行为的工具。”随着这个开源库现已向web3开发者开放，责任在于他们利用这个工具并充分发挥其作用。

![]###http://bitcoinist.com/wp-content/uploads/2025/02/safe.png( 编辑流程针对bitcoinist，旨在提供经过深入研究、准确且公正的内容。我们坚持严格的来源标准，每一页都经过我们顶级技术专家和经验丰富的编辑团队的认真审查。这个流程确保了我们内容的完整性、相关性和对读者的价值。