Zero-Knowledge Model Checking

• URL: http://arxiv.org/abs/2605.00487v1
• Date: Fri, 01 May 2026 07:53:51 GMT
• Title: Zero-Knowledge Model Checking
• Abstract summary: We introduce a technology to formally verify that a software system satisfies a temporal specification of functional correctness, without revealing the system itself.<n>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.
• Score: 8.04509170587377
• License: http://creativecommons.org/licenses/by/4.0/
• 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 and uses piecewise-linear ranking functions. We apply Farkas' lemma to obtain a witness for the validity of the ranking function with public and secret components, and employ sigma protocols for matrix multiplication and range proofs to 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.

Related papers

• Cryptographic certificates of validity for trustworthy AI [0.0]
  We propose cryptographic certificates of validity for agentic AI systems.<n>An agent's action can be accompanied by an independently checkable proof that it satisfies an agreed formal policy.
  arXiv  Detail & Related papers  (2026-06-22T16:42:25Z)
• Phantoms and Disclosures: a Causal Framework for Auditing Synthetic Data [56.86147283213652]
  We present a customizable empirical auditing framework designed to detect and explain data disclosures.<n>Our framework introduces a mechanism to distinguish between "true disclosures"-where the system directly reproduces a user's information-and "phantom disclosures"-where the system incidentally generates a user's data.
  arXiv  Detail & Related papers  (2026-06-15T16:54:02Z)
• Bridging Theory and Practice: An Executable Taxonomy of Security Properties for ProVerif and Tamarin [0.9339654135645749]
  Security is critical for everything relying on modern digital systems.<n>Tools such as ProVerif and Tamarin are widely employed to perform automated verification.<n>This work advances the state of the art by bridging the gap between theoretical security property definitions and their practical, executable verification models.
  arXiv  Detail & Related papers  (2026-05-28T06:57:08Z)
• Formal Evidence Generation for Assurance Cases for Robotic Software Models [1.8145248907978841]
  Assurance Cases provide structured arguments supported by evidence.<n> generating and maintaining this evidence is labour-intensive, error-prone, and difficult to keep consistent as systems evolve.<n>We present a model-based approach to systematically generating AC evidence by embedding formal verification into the assurance workflow.
  arXiv  Detail & Related papers  (2026-02-03T14:01:30Z)
• Neural Model Checking [10.376573742987917]
  We introduce a machine learning approach to model checking temporal logic, with application to formal hardware verification. Our new approach combines machine learning and symbolic reasoning by using neural networks as formal proof certificates for linear temporal logic. We experimentally demonstrate that our method outperforms the state-of-the-art academic and commercial model checkers on a set of standard hardware designs written in SystemVerilog.
  arXiv  Detail & Related papers  (2024-10-31T10:17:04Z)
• Bisimulation Learning [55.859538562698496]
  We compute finite bisimulations of state transition systems with large, possibly infinite state space. Our technique yields faster verification results than alternative state-of-the-art tools in practice.
  arXiv  Detail & Related papers  (2024-05-24T17:11:27Z)
• Formal Methods for Autonomous Systems [21.989467515686858]
  Formal methods have played a key role in establishing the correctness of safety-critical systems. Main building blocks of formal methods are models and specifications. We consider correct-by-construction synthesis under various formulations.
  arXiv  Detail & Related papers  (2023-11-02T14:18:43Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  We provide a framework to encode system specifications and define corresponding certificates. We present an automated approach to formally synthesise controllers and certificates. Our approach contributes to the broad field of safe learning for control, exploiting the flexibility of neural networks.
  arXiv  Detail & Related papers  (2023-09-12T09:37:26Z)
• Representing Timed Automata and Timing Anomalies of Cyber-Physical Production Systems in Knowledge Graphs [51.98400002538092]
  This paper aims to improve model-based anomaly detection in CPPS by combining the learned timed automaton with a formal knowledge graph about the system. Both the model and the detected anomalies are described in the knowledge graph in order to allow operators an easier interpretation of the model and the detected anomalies.
  arXiv  Detail & Related papers  (2023-08-25T15:25:57Z)
• Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
  We introduce the methodology of Faithfulness-through-Counterfactuals. It generates a counterfactual hypothesis based on the logical predicates expressed in the explanation. It then evaluates if the model's prediction on the counterfactual is consistent with that expressed logic.
  arXiv  Detail & Related papers  (2022-05-25T03:40:59Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  In model-based reinforcement learning for safety-critical control systems, it is important to formally certify system properties. We propose a framework that jointly conducts reinforcement learning and formal verification.
  arXiv  Detail & Related papers  (2022-01-28T16:53:56Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.