ZKP Frontier Tracker 🎯
零知识证明 前沿热点追踪 🎯
Mon 星期一
05.19
2025
Verifying SP1 circuit determinism with Picus: A collaboration between Veridise and Succinct https://medium.com/veridise/verifying-sp1-circuit-determinism-with-picus-a-collaboration-between-veridise-and-succinct-985c7a6dd9b5
Veridise shares the initial results of their collaboration with Succinct using the Picus tool to verify the determinism of SP1 circuits, including successful verification of multiple SP1 circuits and identification of improvement points, emphasizing the importance of determinism in ZK circuit security. Veridise分享了与Succinct合作使用Picus工具验证SP1电路确定性的初步成果，包括成功验证多个SP1电路及识别改进点，强调了确定性在ZK电路安全中的重要性。
Notes
- Veridise and Succinct collaborated to verify the determinism of SP1 circuits using the Picus tool
- Determinism verification can eliminate vulnerabilities in ZK circuits due to insufficient logical constraints
- Developed a tool to convert Plonky3 to LLZK, successfully verified 11 basic operations
- Current process has limitations such as modular constraints and input/output labeling
- Succinct plans to optimize the Plonky3 framework to support formal verification
- Targeting to extend formal verification to all SP1 circuits, becoming a regular development step