Ziren targets a deterministic execution model: identical inputs must yield identical outputs across all circuit paths. Determinism at the chip level (e.g. ALU primitives) is a prerequisite for soundness and proof reproducibility.
We partnered with ZK auditing company Veridise to check determinism of Ziren’s core arithmetic components using Picus, their formal verification framework. Ziren is built on Plonky3; Veridise constructed a pipeline that extracts Ziren’s Plonky3 constraints, translates them to LLZK (their IR for ZK languages), and packages them for analysis in AuditHub.
The extractor is presented at Ziren’s branch audit/picus.
Verification covered two ALU primitives - addition and subtraction - implemented together in Ziren’s AddSub chip. Picus confirmed both are deterministic, with checks completing in under two seconds.
What “deterministic” guarantees here:
For the same witness and public inputs, the chip enforces the same output assignment. This rules out multi-solution behavior that could undermine soundness or hinder proof reproducibility.
What’s next (collaboration roadmap):
Analysis ran through AuditHub, enabling both teams to inspect runs and outputs in a reproducible environment. As scope expands, we will continue to surface verification targets and statuses in our engineering notes and release materials.
Formal verification on arithmetic building blocks is a concrete step toward a verifiably correct zkVM. This collaboration helps ensure Ziren’s low-level semantics are pinned down formally, paving the way for broader coverage.
Start building with Ziren today: https://github.com/projectzkm/ziren
Ziren targets a deterministic execution model: identical inputs must yield identical outputs across all circuit paths. Determinism at the chip level (e.g. ALU primitives) is a prerequisite for soundness and proof reproducibility.
We partnered with ZK auditing company Veridise to check determinism of Ziren’s core arithmetic components using Picus, their formal verification framework. Ziren is built on Plonky3; Veridise constructed a pipeline that extracts Ziren’s Plonky3 constraints, translates them to LLZK (their IR for ZK languages), and packages them for analysis in AuditHub.
The extractor is presented at Ziren’s branch audit/picus.
Verification covered two ALU primitives - addition and subtraction - implemented together in Ziren’s AddSub chip. Picus confirmed both are deterministic, with checks completing in under two seconds.
What “deterministic” guarantees here:
For the same witness and public inputs, the chip enforces the same output assignment. This rules out multi-solution behavior that could undermine soundness or hinder proof reproducibility.
What’s next (collaboration roadmap):
Analysis ran through AuditHub, enabling both teams to inspect runs and outputs in a reproducible environment. As scope expands, we will continue to surface verification targets and statuses in our engineering notes and release materials.
Formal verification on arithmetic building blocks is a concrete step toward a verifiably correct zkVM. This collaboration helps ensure Ziren’s low-level semantics are pinned down formally, paving the way for broader coverage.
Start building with Ziren today: https://github.com/projectzkm/ziren
.png)
