Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2605.00487

Zero-Knowledge Model Checking

Pascal Berrang·Mirco Giacobbe·Jacob Swales·Xiao Yang
View original source ↗Read source document ↗Export metadata ↓

Abstract

We introduce a technology to formally verify that a software system satisfies a temporal specification of functional correctness, without revealing the system itself. Our method combines a deductive approach to model checking to obtain a formal certificate of correctness for the system, with zero-knowledge proofs to convince an external verifier that the system -- kept secret -- complies with its specification of correctness -- made public. We consider proof certificates represented as ranking functions, and introduce both an explicit-state and a symbolic scheme for model checking in zero knowledge. Our explicit-state scheme assumes systems represented as transition graphs. We use polynomial commitments to convince the verifier that the public proof certificates correspond to the secret transition relation. Our symbolic scheme assumes systems specified as linear guarded commands. We apply Farkas' lemma to obtain a witness for the validity of the ranking function and employ sigma protocols with folding to efficiently convince the verifier of the witness's existence. We built a prototype to demonstrate the practical efficacy of our two schemes on linear temporal logic verification examples. Our technology enables formal verification in domains where both the safety and the confidentiality of the system under analysis are critical.

Explore related subjects

cs.CRcs.LO

Keep this discovery

BibTeXRIS

Pascal Berrang, Mirco Giacobbe, Jacob Swales, Xiao Yang. 2026-09-08. Zero-Knowledge Model Checking. https://arxiv.org/abs/2605.00487

Cite the original work for its findings. Save a collection to share your selection of sources.

Discover connections

cs.CR subjectcs.LO subject

Connections use source metadata and explicit phrase matches, not verified experimental comparisons.

KEEP EXPLORING

Related papers

arXiv2025

Security Science (SecSci), Basic Concepts and Mathematical Foundations

This textbook compiles the lecture notes from security courses taught at Oxford in the 2000s, at Royal Holloway in the 2010s, and currently in Hawaii. The early chapters are suitable for a first course in security. The middle chapters have been used in advanced courses. Towards the end there are also some research problems.

cs.CR↗
arXiv2026

A Non-Formulable Theorem: A Fundamental Limit of Finite Syntactic Systems and Its Consequences for Security and AI

For every coherent and sufficiently expressive finite syntactic system S, we prove the existence of at least one theorem that S cannot produce autonomously. The result is a metatheorem: it proves the existence of a theorem, and applies to every finite syntactic system - security mechanisms, AI systems, formal verifiers, legal systems, economic models, and the formal system in which it is itself proved.

cs.CR↗
arXiv2026

Proof verification by polynomial Fingerprinting

To cater to the needs of fast verification for mathematical proofs, we describe a method to encode formal sentences in $2 \times 2$ - matrices over multivariate polynomials with integer coefficients. This correspondence is homomorphic: usual proof-steps like modus-ponens or variable substitution in terms and formulae become operations with matrices. By evaluating the polynomial variables in random elements of a suitably chosen finite field, the proof is replaced by a numeric sequence. Only the values corresponding to axioms and tautologies have to be computed from scratch. The values corresponding to derived formulas are computed from the values corresponding to their ancestors by applying the homomorphic properties. The polynomial matrix corresponding to the conclusion of the proof is also evaluated in the chosen random values. If the last term of the numeric sequence equals the evaluation of the conclusion, by the Schwartz-Zippel Lemma, the proof is with high probability correct.

math.LO↗