Paper 2025/1152

ZK-ProVer: Non-Interactive Zero-Knowledge Certification for SAT-Based Program Verification

Abstract

Program verification ensures software correctness through formal methods but often incurs substantial computational overhead. In SAT-based verification, the verification task is reduced to satisfiability checking, where satisfiable instances yield concrete counterexamples and unsatisfiable instances are certified by resolution proofs. While satisfying assignments and resolution proofs are useful for establishing correctness, they may expose defect-relevant details, including concrete inputs that trigger assertion violations, and can be costly for multiple parties to re-check independently. To address this problem, we propose a non-interactive two-phase zero-knowledge protocol for SAT-based program verification that certifies verification results while hiding the satisfying assignment in the SAT case and avoiding transmission of the full resolution proof in the UNSAT case. In Phase I, a zero-knowledge virtual machine (zkVM) performs translation validation for the deterministic frontend-to-CNF translation from the source program and assertions, and binds the resulting SAT formula through a commitment for subsequent verification. In Phase II, we design two specialized AIR constraint systems and implement them over a Plonky3-based STARK backend: one checks satisfying assignments for SAT instances, and the other checks resolution proofs for UNSAT instances, without requiring verifiers to replay the full UNSAT certificate. We evaluate the two phases separately. On supported SV-COMP-style benchmarks, Phase I validates reusable program-to-CNF translations for bounded verification-condition instances. For Phase II, comparison with ZKUNSAT on ten UNSAT instances yields an 11.1× geometric-mean verifier speedup and a 410.4× geometric-mean reduction in verifier-side communication. These component-level results provide evidence for the feasibility of zero-knowledge certification of program-verification results while limiting counterexample disclosure and reducing repeated UNSAT-certificate validation cost.