Proving UNSAT in Zero Knowledge

Program verification ensures software correctness through formal methods but incurs substantial computational overhead. It typically encodes program execution into formulas that are verified using a SAT solver and its extensions. However, this process exposes sensitive program details and requires redundant computations when multiple parties need to verify correctness. To overcome these limitations, zeroknowledge proofs (ZKPs) generate compact, reusable proofs with fast verification times, while provably hiding the program's internal logic. We propose a two-phase zero-knowledge protocol that hides program implementation details throughout verification. In Phase I, a zero-knowledge virtual machine (zkVM) is employed, which adopts HyperPlonk as the underlying protocol. This zkVM enables the encoding of programs into Boolean Satisfiability (SAT) formulas, while strictly avoiding the disclosure of the programs' semantic information. Phase II employs the encoding of resolution proofs for UNSAT instances and circuits for satisfying assignment verification for SAT instances through PLONKish circuits. Evaluation on the Boolector benchmark demonstrates that our method achieves verification time that is efficient and is independent of clause width for UNSAT instances and formula size for SAT instances. The resulting ZKPs enable efficient verification of program properties while providing strong end-to-end privacy guarantees.