Ziren has completed an independent security review by Veridise, validating its execution model as a well-defined machine under adversarial conditions.
A zkVM can fail in a small number of ways: ambiguous state transitions, underconstrained memory or syscall semantics, malleable traces, or a runtime that collapses under malformed programs. These are machine-level failures that, if present, undermine the meaning of the proof itself.
The Veridise assessment focused precisely on these failure modes. The review combined manual circuit inspection, formal determinism checks using Veridise’s Picus tooling, and extensive fuzzing of the execution and trace-generation paths. The goal was to determine whether Ziren behaves like a single, well-defined machine under all admissible inputs.
Post-audit, Ziren is suitable for live deployment because the machine-level invariants are enforced by the constraint system rather than assumed by convention. It also saves applications being built on top of Ziren from having to undergo certain audit processes, reducing their audit cost.
The audit surfaced a number of issues - including several high- and critical-severity findings - all of which relate to the same underlying risk: parts of the system where the prover had more freedom than intended.
Crucially, these issues were identified, fixed, and re-verified during the audit process. With those fixes in place, the assessment establishes several core properties that matter for deployment.
First, execution determinism:
Ziren’s circuits now encode deterministic state transitions. Given the same inputs, there is exactly one valid execution trace that can satisfy the constraints. This removes ambiguity and prevents alternative executions from being proven as equivalent.
Second, sound memory and syscall semantics:
Memory accesses, register interactions, and syscalls are now fully constrained. A prover cannot fabricate reads, suppress writes, or inject host interactions while maintaining a valid proof.
Third, trace integrity under adversarial inputs:
Through fuzzing and stress testing, Ziren demonstrated stable behaviour even when executing malformed or malicious programs. Panics and unchecked arithmetic that could previously crash the VM have been removed or guarded.
Finally, alignment between execution and proof:
The audit confirms that the behaviour enforced by Ziren’s constraint system matches the intended semantics of the MIPS execution model. What is executed is exactly what is proven.
A production system depends on the assumption that proofs correspond to real computation - not “mostly correct” execution, and not behaviour that holds only under cooperative inputs. The audit establishes that Ziren meets this bar.
This is why Ziren can now be used as an execution layer in live systems, including rollup architectures that operate continuously and process untrusted inputs. The audit does not claim perfection; no audit can. But it confirms that the core execution invariants are enforced by the system itself, rather than by convention or assumption.
ZKM was formed to build core zero-knowledge execution infrastructure, with the zkVM as the central abstraction. Ziren was designed from the outset as a general-purpose execution environment: a stable, deterministic virtual machine capable of running arbitrary programs and producing proofs that faithfully represent that execution.
GOAT Network should be understood as a vertical extension of this work. It is the first concrete system that exercises Ziren under real-world conditions (though not the sole context in which Ziren is intended to operate). GOAT Network uses Ziren as its execution layer because a Bitcoin rollup requires precisely the properties Ziren was built to provide: deterministic execution reminders, tight control over memory and syscalls, and predictable behaviour under adversarial inputs.
By deploying Ziren inside a live system, ZKM is able to validate the VM not only in isolation, but as part of a complete execution and verification pipeline. The audit process sits between these two layers, ensuring that the machine-level semantics Ziren enforces are sound before they are relied upon by production systems.
At the same time, Ziren is available for use by other projects and is particularly well-suited to applications built on BitVM-style verification. As demonstrated by GOAT Network, BitVM2/3 shifts computation off-chain and relies on succinct verification on Bitcoin; this places strict requirements on the execution environment that produces the proofs. Ziren’s design - including its deterministic execution model and explicit constraint encoding - aligns well with these requirements (as confirmed by independent ZK research firm, Prooflab.
Post-audit, Ziren is:
This establishes Ziren as fully deployable infrastructure.
For readers interested in the technical details, the full Veridise report is available here: github.com/ProjectZKM/Ziren/tree/main/audits
Ziren has completed an independent security review by Veridise, validating its execution model as a well-defined machine under adversarial conditions.
A zkVM can fail in a small number of ways: ambiguous state transitions, underconstrained memory or syscall semantics, malleable traces, or a runtime that collapses under malformed programs. These are machine-level failures that, if present, undermine the meaning of the proof itself.
The Veridise assessment focused precisely on these failure modes. The review combined manual circuit inspection, formal determinism checks using Veridise’s Picus tooling, and extensive fuzzing of the execution and trace-generation paths. The goal was to determine whether Ziren behaves like a single, well-defined machine under all admissible inputs.
Post-audit, Ziren is suitable for live deployment because the machine-level invariants are enforced by the constraint system rather than assumed by convention. It also saves applications being built on top of Ziren from having to undergo certain audit processes, reducing their audit cost.
The audit surfaced a number of issues - including several high- and critical-severity findings - all of which relate to the same underlying risk: parts of the system where the prover had more freedom than intended.
Crucially, these issues were identified, fixed, and re-verified during the audit process. With those fixes in place, the assessment establishes several core properties that matter for deployment.
First, execution determinism:
Ziren’s circuits now encode deterministic state transitions. Given the same inputs, there is exactly one valid execution trace that can satisfy the constraints. This removes ambiguity and prevents alternative executions from being proven as equivalent.
Second, sound memory and syscall semantics:
Memory accesses, register interactions, and syscalls are now fully constrained. A prover cannot fabricate reads, suppress writes, or inject host interactions while maintaining a valid proof.
Third, trace integrity under adversarial inputs:
Through fuzzing and stress testing, Ziren demonstrated stable behaviour even when executing malformed or malicious programs. Panics and unchecked arithmetic that could previously crash the VM have been removed or guarded.
Finally, alignment between execution and proof:
The audit confirms that the behaviour enforced by Ziren’s constraint system matches the intended semantics of the MIPS execution model. What is executed is exactly what is proven.
A production system depends on the assumption that proofs correspond to real computation - not “mostly correct” execution, and not behaviour that holds only under cooperative inputs. The audit establishes that Ziren meets this bar.
This is why Ziren can now be used as an execution layer in live systems, including rollup architectures that operate continuously and process untrusted inputs. The audit does not claim perfection; no audit can. But it confirms that the core execution invariants are enforced by the system itself, rather than by convention or assumption.
ZKM was formed to build core zero-knowledge execution infrastructure, with the zkVM as the central abstraction. Ziren was designed from the outset as a general-purpose execution environment: a stable, deterministic virtual machine capable of running arbitrary programs and producing proofs that faithfully represent that execution.
GOAT Network should be understood as a vertical extension of this work. It is the first concrete system that exercises Ziren under real-world conditions (though not the sole context in which Ziren is intended to operate). GOAT Network uses Ziren as its execution layer because a Bitcoin rollup requires precisely the properties Ziren was built to provide: deterministic execution reminders, tight control over memory and syscalls, and predictable behaviour under adversarial inputs.
By deploying Ziren inside a live system, ZKM is able to validate the VM not only in isolation, but as part of a complete execution and verification pipeline. The audit process sits between these two layers, ensuring that the machine-level semantics Ziren enforces are sound before they are relied upon by production systems.
At the same time, Ziren is available for use by other projects and is particularly well-suited to applications built on BitVM-style verification. As demonstrated by GOAT Network, BitVM2/3 shifts computation off-chain and relies on succinct verification on Bitcoin; this places strict requirements on the execution environment that produces the proofs. Ziren’s design - including its deterministic execution model and explicit constraint encoding - aligns well with these requirements (as confirmed by independent ZK research firm, Prooflab.
Post-audit, Ziren is:
This establishes Ziren as fully deployable infrastructure.
For readers interested in the technical details, the full Veridise report is available here: github.com/ProjectZKM/Ziren/tree/main/audits
