Paper 2025/2204

Consistency Verification for Zero-Knowledge Virtual Machine on Circuit-Irrelevant Representation

Abstract

Zero-knowledge virtual machines (zkVMs) rely on tabular constraint systems whose verification semantics include gate, lookup, and permutation relations, making correctness auditing substantially more challenging than in arithmetic-circuit DSLs such as Circom. In practice, ensuring that witness-generation code is consistent with these constraints has become a major source of subtle and hard-to-detect bugs. To address this problem, we introduce a high-level semantic model for tabular constraint systems that provides a uniform, circuit-irrelevant interpretation of row-wise constraints and their logical interactions. This abstraction enables an inductive, row-indexed reasoning principle that checks consistency without expanding the full circuit, significantly improving scalability. We implement this methodology in ZIVER and show that it faithfully captures real zkVM designs and automatically validates the consistency of diverse SP1 chip components.