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