At Veridise we’ve taken another step toward our mission to bring formal verification to the zero-knowledge ecosystem. This time we partnered with ZKM—the team behind Ziren, a MIPS-based zkVM built on Plonky3—to verify the determinism of its core arithmetic components using Picus, our in-house verification framework. A key step in achieving this goal is to build a complete verification pipeline that connects a Plonky3-based constraint system to the Picus verification environment.
Building the Picus Verification Pipeline for Ziren
Ziren’s circuits are defined over the Plonky3 backend, whose constraints differ significantly from the intermediate representations that Picus operates on. To bridge this gap, we designed a custom extraction pipeline that:
- Parses Ziren’s constraint definitions within Plonky3.
- Translates them into Picus’s internal representation via LLZK our IR for ZK languages.
- Packages the translated circuits into a form consumable by AuditHub, Veridise’s verification platform.
Once the translation was complete, Ziren’s circuits could be analyzed by Picus just like any other Picus-native program — enabling automated checks for determinism.
Determinism Verification Results
As a first step, we focused on two arithmetic primitives in Ziren’s ALU: the addition and subtraction instructions which are expressed in a single AddSub chip. Using Picus, we verified that both instructions were deterministic — a core requirement for sound zkVM design — in under 2 seconds!.
Running Picus through AuditHub allows us to conduct these checks reproducibly and transparently, ensuring both teams could inspect results and artifacts directly through Veridise’s cloud platform.
Why Determinism Matters for zkVMs
Determinism is a cornerstone of verifiable computation. In zkVMs, each circuit represents a program execution trace; if any subcircuit can yield multiple outputs for the same input, it threatens both soundness and proof reproducibility.
By formally proving determinism of arithmetic chips, we ensure that the zkVM’s foundational building blocks behave in a well-defined, mathematical way — paving the way for future proofs of correctness and completeness.
Looking Ahead
This verification marks only the beginning of our collaboration with Ziren. Our next milestones include:
- Extending the verification to cover the full ALU (including multiplication, division, and bitwise ops).4
- Automating the translation process for larger composite chips within Ziren’s execution pipeline.
- Integrating determinism verification into continuous integration workflows, enabling automated checks on every new release.
By scaling this verification effort, we hope to make formal guarantees a standard part of zkVM development — not an afterthought.
About Picus and AuditHub
Picus is Veridise’s formal verification framework for ZK circuits. It automatically proves key security and correctness properties — such as determinism, range soundness, and constraint consistency — across multiple ZK ecosystems (Halo2, Circom, Plonky3, and more).
AuditHub provides a unified interface for running and visualizing verification tools like Picus, allowing protocol teams to integrate formal checks directly into their audit process.
