运行时：giskard共识以高安全性和稳定性保护平台

最近，运行时验证宣布了giskard共识协议验证项目与平台网络的成功完成。本次合作的目的是通过CoQ认证辅助验证方法验证平台giskard共识协议的安全性。根据运行时验证发布的技术报告，GISKARD一致性协议在验证过程中具有较高的安全性和稳定性，为平台系统的良好运行奠定了坚实的基础。

根据有关运行确认的负责人，在项目实施过程中，双方坚持了高效、严谨、极细粒度的地位和要求，对GISKARD共识进行了“高压”验证，GISKARD共识是平台的基础和核心。实现全球隐私计算网络和分布式经济基础设施，是平台区块链生态分布式网络基础设施的中心，用于验证平台网络中的交易和操作。

由于分布式系统中复杂多变的环境和网络节点存在的不良可能性，传统的仅通过单一的测试方法来保证一致性协议的安全性已不能满足当前的需要。运行时验证在CoQ中建立giskard模，对协议的几个关键安全属性进行编码和形式化验证。

从结果来看，运行时验证通过形式化验证得到的机器验证证据有力地证明了即使存在坏节点，giskard共识协议的关键安全属性也能为整个平台协议的实现保驾护航。本项目合作的验证结果为giskard共识协议作为平台网络基础设施的核心组成部分的可靠性提供了重要依据，明确了giskard共识的基本假设。

这次合作意义重大。它不仅验证了作为私有计算网络和分布式经济基础设施核心组件的平台的可靠性（该组件很难通过单一测试和其他类似方法进行分析），同时也使运行时验证能够详细说明Giscard共识协议的技术参数和假设。更新后的技术参数为以后落实和核查吉斯卡尔共识协议提供了指导，双方对此次合作给予了高度评价。

Gregory Russell是伊利诺伊大学香槟分校运行时验证的首席执行官和计算机科学教授，他说：“我们很荣幸与平台团队合作，通过CoQ对giskard协议进行建模和形式化。现在我们对协议的稳定运行和实现充满信心，也证明了协议的安全性达到了预期的标准。在与平台团队的密切沟通中，我们采用了最严格的形式化验证方法，充分证明了协议具有极高的安全性能。我们的giskard模也为将来协议的实现和变更提供了可靠而严格的参考。我们非常期待与平台深化合作，构建技术生态。”

对于此次合作，平台首席技术官曲俊杰表示：“很荣幸与运行时验证的工程师和研究人员合作，在此期间的交流也非常愉快。运行时验证团队处理多个并行复杂问题和边缘情况的能力给我们留下了深刻印象。我很高兴运行时验证可以成为平台的合作伙伴，一起工作。此后，我们将继续在协议建模和智能合约正式验证等领域保持深入合作。”

关于运行时验证

Runtime verification是一家位于美国伊利诺伊州乌尔巴纳的技术公司，专注于为区块链领域提供软件测试和验证服务和产品。

关于平台

平台由晓峰万象博士创立，致力于成为新一代全球隐私计算和分布式经济基础设施，也是全球隐私计算领域的先驱和领导者。高性能分布式计算网络长期以来专注于可扩展性和隐私保护，为全球人工智能、分布式应用开发者、数据提供商和各种社区提供开源，有计算需求的机构和个人通过下一代计算体系结构组成的可验证计算、安全多方计算、零知识证明、同态加密等密码算法公共基础设施框架下。其元网络Alaya于2020年10月24日正式上线。