今天，我们与Nethermind合作分享了 对 SP1正确性进行正式验证的进展，Nethermind 是形式化方法方面的专家，重点致力于增强零知识证明的安全性。
上周，我们宣布了使用形式化验证工具证明 SP1 确定性的工作。虽然确定性确保电路为每组输入产生单一、一致的输出，并且在很大程度上可以自动化，但证明正确性则是一个更加严格、手动且通常繁琐的过程。它需要形式化地指定预期行为，并证明电路完全遵循该行为。这正是 Nethermind 团队的优势所在：他们拥有深厚的专业知识，能够将这一流程扩展至像 SP1 这样不断发展的大型系统，使其可持续且实用。
作为此次合作的一部分，我们构建了基础架构，将 SP1 的约束提取到 Lean 中，使我们能够编写精确的正式规范，并验证我们的电路是否符合这些规范。我们成功地将该基础架构应用于AddSub芯片，并根据 32 位环绕加法的正式定义证明了其正确性。
我们将继续这项工作，扩展我们的验证框架，使其涵盖所有基础 ALU 电路。之后，我们将专注于更复杂的预编译，例如 Keccak256 和 Secp256k1，它们是 SP1 中最复杂的电路之一。为了支持这项工作，我们正在投入精力改进我们的验证工具和这些电路的模块化结构。我们的长期目标是根据 RISC-V 规范对 SP1 进行全面的正式验证，以确保我们的 zkVM 能够按预期实现架构，并提供严格的端到端保障。
我们与 Nethermind 的合作是我们更广泛的安全战略的重要组成部分，该战略包括审计、专家评审以及SP1-2FA等运行时安全措施。我们很高兴能够继续加强安全工作，并不断改进我们的战略，为开发者提供更强有力的 SP1 正确性和可靠性保障。
在他们的博客文章中了解有关我们与 Nethermind 合作的更多技术细节。