The paper, Ziren: Succinct Arguments for MIPS32 Execution, is entry 2026/2330 on the IACR Cryptology ePrint Archive, and its full text is also available as the Ziren whitepaper on zkm.io. It is a complete design reference for a production zkVM: the architecture, the proof system, the formal verification of the machine itself, the security analysis and the production results, in one document.
Papers in this field usually present a single component, such as a commitment scheme or a sumcheck variant, while the full design of a production zkVM is spread across documentation and code. This paper puts Ziren's full design in one place.
Ziren is a CPU-less chip architecture. There is no central processor table: every executed instruction is one row in the chip for its opcode, and every relation between chips crosses a named bus. Because each chip carries its own constraints, the paper can state and prove determinism chip by chip.
Each shard of execution is proved with one lookup argument covering all of its buses and one zerocheck covering all of its constraints. The claims on its tens of thousands of columns of differing heights are then reduced by a jagged sumcheck to a single evaluation, opened with one batched WHIR proof. A recursion tree composes the shard proofs, and each node admits only verifying keys from an allowlist enumerated from the machine's declared shard shapes. The result is a compressed proof of 274 KiB that a native verifier checks in about 73 ms.
The paper describes those two applications without measuring them. One wraps the compressed proof in a pairing-based SNARK over BN254 for on-chain verifiers. The other re-proves it over a binary field with Blake3 for a garbled verifier, the kind of verifier used by protocols that check a computation on Bitcoin only when it is disputed.
The paper compares Ziren's design choices with four other zkVMs, at the releases it cites.
A well-known class of zkVM soundness bug is the under-constrained circuit: a constraint system that admits more than one witness, which lets a dishonest prover prove something false. The usual defence is review of the constraints, by auditors and by automated tools. Ziren adds determinism theorems: proofs that any two rows of a chip that satisfy its constraints and agree on their inputs also agree on their outputs.
The paper presents 104 of them, all proved in Lean 4, covering the determinism of 57 of the core machine's 62 chips: all but three preprocessed tables and two SHA-256 control chips. The theorems are extracted mechanically from the same constraint description the prover evaluates, so there is no separate hand-written model of the circuits that could drift from the code. All 104 are closed, with no axiom beyond Lean 4's standard three, and the proofs, gadget library and check scripts are archived alongside the paper.
Earlier determinism checks on Ziren's arithmetic core, made with @VeridiseInc in October 2025, are described in Verifying Determinism in Ziren's Arithmetic Core.
Every proof stage of the analysed schedule has more than 100 bits of interactive soundness, and the composite security over a block's tree of about 150 proofs is 93.5 bits. The composite figure sums the errors of every node in the tree, so it falls with the logarithm of the number of proofs. Both figures bound the interactive protocol; the paper also gives the bound after Fiat-Shamir compilation.
The end-to-end statement is conditional, and the paper lists what it assumes: round-by-round knowledge soundness of every node, compatibility of the composed extractors, that the recursion programs enforce the compose relation, and a property of the cross-shard digest to which the paper assigns no value. Identifying the trace with an execution also needs determinism of the two SHA-256 control chips and real-row exhaustiveness.
Ziren proves 77 user-mode integer instructions of MIPS32r2 and has proved Ethereum mainnet blocks end to end in production. On the configuration measured in the paper, proving throughput reaches up to 7.3 MHz on a single NVIDIA RTX 5090 and 24 MHz across four GPUs. The paper notes that this configuration precedes four later changes.
Veridise audited Ziren in October and November 2025, with manual review of the verifier logic, tool-assisted determinism validation of the circuits using Picus, and fuzzing of witness generation. All high- and critical-severity findings were fixed and re-verified, as described in Ziren Post-Audit: Execution Integrity Confirmed, and the audit report is public.
In December 2025, @ConsensysAudits (Consensys Diligence) and researchers at @TU_Wien, who had pointed their fuzzing infrastructure at Ziren, reached us through the @EthereumFndn. Seven months of responsible disclosure followed: five bugs found by fuzzing, each reproduced, fixed and independently re-verified, one fix landed upstream in LLVM, and two hardened releases, v1.2.5 and v1.2.6. The full record is in Inside Ziren's security collaboration with Consensys Diligence.
In September 2025, @TheProofLab published an independent evaluation of Ziren v1.1.4 covering the core VM, the distributed prover and the WASM verifier: An Independent Evaluation of Ziren v1.1.4.
One component of Ziren is not hash-based: the elliptic-curve multiset hash that carries memory consistency across shards. The paper states that the assumption behind it, unlike the rest of the argument, does not survive a quantum adversary. We have tracked it publicly as Ziren issue #276 since August 2025, and our September post, Hash-based is not the same as post-quantum, described two routes to replace it: a lattice multiset hash and a LogUp-GKR argument with a global challenge.
The paper adds a third route, Merkle roots over touched memory, and measures it and the global challenge against the elliptic-curve hash on the same GPUs. Merkle roots, whose soundness rests only on the collision resistance of the hash, proved 16.6% faster on one GPU and 3.4% slower on four, with 47% fewer shards and about 20 GB more memory per worker. The global challenge was 29% slower on one GPU and 42% slower on four. The lattice hash was costed rather than built, at 19.6 times today's committed area or more. The paper's measurements and soundness accounting are stated for the elliptic-curve hash, and the replacement has not been chosen.
Our thanks to the Plonky3 contributors and the SP1 team (@SuccinctLabs), whose work Ziren builds on, and to the Ethereum Foundation, Consensys Diligence, TU Wien and Veridise for working with us so closely on Ziren's security.
The paper, Ziren: Succinct Arguments for MIPS32 Execution, is entry 2026/2330 on the IACR Cryptology ePrint Archive, and its full text is also available as the Ziren whitepaper on zkm.io. It is a complete design reference for a production zkVM: the architecture, the proof system, the formal verification of the machine itself, the security analysis and the production results, in one document.
Papers in this field usually present a single component, such as a commitment scheme or a sumcheck variant, while the full design of a production zkVM is spread across documentation and code. This paper puts Ziren's full design in one place.
Ziren is a CPU-less chip architecture. There is no central processor table: every executed instruction is one row in the chip for its opcode, and every relation between chips crosses a named bus. Because each chip carries its own constraints, the paper can state and prove determinism chip by chip.
Each shard of execution is proved with one lookup argument covering all of its buses and one zerocheck covering all of its constraints. The claims on its tens of thousands of columns of differing heights are then reduced by a jagged sumcheck to a single evaluation, opened with one batched WHIR proof. A recursion tree composes the shard proofs, and each node admits only verifying keys from an allowlist enumerated from the machine's declared shard shapes. The result is a compressed proof of 274 KiB that a native verifier checks in about 73 ms.
The paper describes those two applications without measuring them. One wraps the compressed proof in a pairing-based SNARK over BN254 for on-chain verifiers. The other re-proves it over a binary field with Blake3 for a garbled verifier, the kind of verifier used by protocols that check a computation on Bitcoin only when it is disputed.
The paper compares Ziren's design choices with four other zkVMs, at the releases it cites.
A well-known class of zkVM soundness bug is the under-constrained circuit: a constraint system that admits more than one witness, which lets a dishonest prover prove something false. The usual defence is review of the constraints, by auditors and by automated tools. Ziren adds determinism theorems: proofs that any two rows of a chip that satisfy its constraints and agree on their inputs also agree on their outputs.
The paper presents 104 of them, all proved in Lean 4, covering the determinism of 57 of the core machine's 62 chips: all but three preprocessed tables and two SHA-256 control chips. The theorems are extracted mechanically from the same constraint description the prover evaluates, so there is no separate hand-written model of the circuits that could drift from the code. All 104 are closed, with no axiom beyond Lean 4's standard three, and the proofs, gadget library and check scripts are archived alongside the paper.
Earlier determinism checks on Ziren's arithmetic core, made with @VeridiseInc in October 2025, are described in Verifying Determinism in Ziren's Arithmetic Core.
Every proof stage of the analysed schedule has more than 100 bits of interactive soundness, and the composite security over a block's tree of about 150 proofs is 93.5 bits. The composite figure sums the errors of every node in the tree, so it falls with the logarithm of the number of proofs. Both figures bound the interactive protocol; the paper also gives the bound after Fiat-Shamir compilation.
The end-to-end statement is conditional, and the paper lists what it assumes: round-by-round knowledge soundness of every node, compatibility of the composed extractors, that the recursion programs enforce the compose relation, and a property of the cross-shard digest to which the paper assigns no value. Identifying the trace with an execution also needs determinism of the two SHA-256 control chips and real-row exhaustiveness.
Ziren proves 77 user-mode integer instructions of MIPS32r2 and has proved Ethereum mainnet blocks end to end in production. On the configuration measured in the paper, proving throughput reaches up to 7.3 MHz on a single NVIDIA RTX 5090 and 24 MHz across four GPUs. The paper notes that this configuration precedes four later changes.
Veridise audited Ziren in October and November 2025, with manual review of the verifier logic, tool-assisted determinism validation of the circuits using Picus, and fuzzing of witness generation. All high- and critical-severity findings were fixed and re-verified, as described in Ziren Post-Audit: Execution Integrity Confirmed, and the audit report is public.
In December 2025, @ConsensysAudits (Consensys Diligence) and researchers at @TU_Wien, who had pointed their fuzzing infrastructure at Ziren, reached us through the @EthereumFndn. Seven months of responsible disclosure followed: five bugs found by fuzzing, each reproduced, fixed and independently re-verified, one fix landed upstream in LLVM, and two hardened releases, v1.2.5 and v1.2.6. The full record is in Inside Ziren's security collaboration with Consensys Diligence.
In September 2025, @TheProofLab published an independent evaluation of Ziren v1.1.4 covering the core VM, the distributed prover and the WASM verifier: An Independent Evaluation of Ziren v1.1.4.
One component of Ziren is not hash-based: the elliptic-curve multiset hash that carries memory consistency across shards. The paper states that the assumption behind it, unlike the rest of the argument, does not survive a quantum adversary. We have tracked it publicly as Ziren issue #276 since August 2025, and our September post, Hash-based is not the same as post-quantum, described two routes to replace it: a lattice multiset hash and a LogUp-GKR argument with a global challenge.
The paper adds a third route, Merkle roots over touched memory, and measures it and the global challenge against the elliptic-curve hash on the same GPUs. Merkle roots, whose soundness rests only on the collision resistance of the hash, proved 16.6% faster on one GPU and 3.4% slower on four, with 47% fewer shards and about 20 GB more memory per worker. The global challenge was 29% slower on one GPU and 42% slower on four. The lattice hash was costed rather than built, at 19.6 times today's committed area or more. The paper's measurements and soundness accounting are stated for the elliptic-curve hash, and the replacement has not been chosen.
Our thanks to the Plonky3 contributors and the SP1 team (@SuccinctLabs), whose work Ziren builds on, and to the Ethereum Foundation, Consensys Diligence, TU Wien and Veridise for working with us so closely on Ziren's security.
