RISC Zero 如何实现持续且可证明的零知识安全性？

该视频总结了 Risk Zero 和 Veridise 合作，使用 Veridise 的 PyKIS 工具对 Risk Zero 的 Ketchak 电路进行形式化验证，证明其确定性的过程和意义。

核心内容/主要观点：

• Risk Zero 和 Veridise 成功合作，使用 PyKIS 工具形式化验证了 Risk Zero 的 Ketchak 电路的确定性。
• 形式化验证对于确保零知识证明系统的安全性至关重要，可以有效防止“欠约束”漏洞。
• 此次合作不仅验证了特定电路，也为持续验证和优化 Risk Zero 的电路提供了自动化流程。

关键论据/关键信息：

• 确定性的重要性： 确定性是零知识电路的关键属性，确保电路的行为是可预测的，防止出现意外或恶意解。
• PyKIS 工具： Veridise 开发的 PyKIS 工具可以检查零知识电路的确定性，并能生成反例或进行形式化验证。
• 合作过程： Veridise 在初期审计时就发现了 Risk Zero 电路中的漏洞，促成了双方的合作。Risk Zero 积极配合，快速迭代，最终完成了验证。
• 形式化验证的文化： Risk Zero 非常重视形式化验证，将其视为确保系统安全性的重要手段。
• DSL 的作用： Risk Zero 使用的领域特定语言 (DSL) Zergen，其模块化设计和明确的语义使得电路更易于验证。
• 未来方向： 双方都计划在形式化验证方面进行更多探索，包括验证编译器、电路的功能正确性，以及开发更通用的验证工具。Veridise 正在开发LLCK，一个用于电路DSL的底层中间表示，旨在构建更广泛的安全工具。
• 形式化验证的假设： 视频中也提到了形式化验证依赖于一些假设，例如代码翻译的正确性，以及验证工具本身的正确性。未来需要进一步加强这些方面的保证。