Sonic Labs推出DAG共识协议形式化验证库

高性能Layer1区块链Sonic背后的开发团队Sonic Labs宣布了一项区块链安全领域的重大突破——在首席研究官Bernhard Scholz博士的带领下，他们发布了面向DAG共识协议的形式化验证库。这个开源库运用形式化验证方法，为包括Sonic自研EVM区块链在内的有向无环图区块链提供数学层面的安全性证明。

通过与悉尼大学和INRIA顶尖逻辑学家的合作，Sonic Labs验证库采用TLA+证明辅助工具构建。该库提供可复用的模块化组件，大幅简化了DAG共识协议的验证流程，开发者只需最小工作量即可完成协议建模与验证。

该验证库涵盖DAG-Rider、Cordial Miner、Bullshark、Hashgraph和Aleph等主流DAG协议的证明，Sonic自研共识协议作为衍生方案也通过了验证。这项成果于6月11-13日在弗吉尼亚州威廉斯堡举办的NASA Formal Methods 2025（NFM 2025）会议上首次发布，为区块链安全树立了新标杆。

"区块链领域的安全漏洞往往源于未经检验的假设，等到发现时为时已晚。通过这个验证库，我们将从依赖经验转向数学证明，提供工具确保协议在所有条件下都安全运行。我们的目标是让每个协议开发者都能运用形式化验证技术。"

——Sonic Labs首席研究官 Bernhard Scholz博士

鉴于区块链上锁定的数万亿美元资产，共识协议漏洞可能导致双花攻击或账本不一致等灾难性后果。传统测试和审计方法因无法保证完全消除漏洞而存在局限。Sonic Labs采用形式化验证这一严格的数学方法，证明协议在所有可能场景下的安全性，彻底杜绝错误发生。

除支持现有协议验证外，Sonic Labs的方案还能辅助开发者创建新型DAG协议或改良现有模型。为展示验证库效能，Sonic Labs已开始部署形式化验证，证明Sonic区块链上不可能出现数学层面的不安全行为。

通过开源验证库，Sonic Labs致力于赋能区块链开发者构建可验证的安全协议。这将大幅缩短DAG共识完整性的验证周期和成本，同时强化整个Web3生态系统的安全性。