今天，我们很高兴地分享 SP1 形式化验证工作的进展情况，这项工作由我们与零知识安全审计领域的领先公司 Veridise合作开发。形式化验证在建立 SP1 行为的数学保证方面发挥着至关重要的作用。
这项工作是对我们对 SP1 安全性的多层方法的补充，包括上个月推出的SP1-2FA，它为开发人员提供了一种易于启用的运行时保护措施，以防范恶意证明者行为。除了全面的审计和外部审查外，我们还与 Veridise 合作，使用Picus进行确定性检查，这有助于确保 SP1 电路完全按照预期运行，为实现基于实践和理论的、经过形式化验证的 zkVM 铺平了道路。
许多电路错误，例如缺少范围检查或变量约束不足，很难通过人工审查发现，但通常可以通过非确定性发现。如果一个电路能够针对同一输入产生多个有效输出，则强烈表明存在约束不足的情况。通过正式检查确定性，我们可以及早发现这些问题，并排除一系列可能损害健全性的细微错误。对于 SP1 来说，这增加了一层重要的保障，确保每个电路都以可预测、安全和可验证的方式运行。
这是一项持续进行的合作，我们很高兴能在接下来的几周内继续与 Veridise 合作，将 Picus 扩展到整个 SP1 堆栈，目标是正式验证 SP1 中每个电路的确定性。除了确定性之外，我们还在进行一些激动人心的工作，重点是证明电路的形式正确性，使我们更接近端到端的数学保证。敬请期待更多更新。
了解更多关于 Veridise 如何利用其工具 Picus，通过将 SP1 基于 Plonky3 的约束转换为 Veridise 的中间表示 LLZK，正式验证关键 SP1 电路的确定性，包括 u32 加法、异或运算和范围检查。阅读其博客文章，了解完整的技术细节。