ZKP Frontier Tracker 🎯零知识证明 前沿热点追踪 🎯ZKP 最前線追跡🎯
Mon星期一月曜日
05.19
2025
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电路安全中的重要性。Veridiseは、Picusツールを用いたSuccinctとの共同作業の初期結果を共有します。これには、複数のSP1サーキットの検証成功や改善点の特定が含まれ、ZK回路セキュリティにおける決定論（determinism）の重要性を強調しています。
NotesNotes要点
- 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