pith. machine review for the scientific record. sign in

arxiv: 2605.00487 · v1 · submitted 2026-05-01 · 💻 cs.CR · cs.LO

Recognition: unknown

Zero-Knowledge Model Checking

Jacob Swales, Mirco Giacobbe, Pascal Berrang, Xiao Yang

Authors on Pith no claims yet

Pith reviewed 2026-05-09 19:34 UTC · model grok-4.3

classification 💻 cs.CR cs.LO
keywords zero-knowledge proofsmodel checkingranking functionsformal verificationtemporal logicguarded commandspolynomial commitmentsFarkas lemma
0
0 comments X

The pith

Zero-knowledge proofs on ranking functions let verifiers confirm a secret system's correctness against a public temporal specification.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a technique that formally verifies whether a software system satisfies a temporal correctness property without ever revealing the system itself. It obtains a ranking-function certificate through deductive model checking and then uses zero-knowledge proofs to show the verifier that this certificate is valid for the hidden system. Two concrete schemes are presented: an explicit-state version for transition graphs that relies on polynomial commitments, and a symbolic version for linear guarded commands that applies Farkas' lemma together with sigma protocols. A working prototype shows the approach can handle linear temporal logic examples. The result matters wherever both safety guarantees and confidentiality are required, such as in proprietary or security-sensitive software.

Core claim

We introduce both an explicit-state and a symbolic scheme for model checking in zero knowledge. The explicit-state scheme assumes systems represented as transition graphs and uses polynomial commitments to convince the verifier that the public proof certificates correspond to the secret transition relation. The symbolic scheme assumes systems specified as linear guarded commands and uses piecewise-linear ranking functions; Farkas' lemma produces a witness for the validity of the ranking function with public and secret components, and sigma protocols for matrix multiplication and range proofs convince the verifier of the witness's existence.

What carries the argument

Ranking functions serving as formal certificates of correctness, paired with zero-knowledge proof machinery (polynomial commitments for graphs and Farkas witnesses plus sigma protocols for guarded commands) to hide the underlying system while exposing only the validity of the certificate.

If this is right

  • Linear temporal logic properties can be verified on systems whose transition relation or commands remain hidden.
  • Explicit-state model checking becomes possible in zero knowledge when systems are given as transition graphs.
  • Symbolic model checking becomes possible in zero knowledge when systems are given as linear guarded commands.
  • A prototype implementation demonstrates that the two schemes are feasible on standard verification benchmarks.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same certificate-plus-zero-knowledge pattern could be applied to other deductive verification methods that produce algebraic witnesses.
  • If the overhead remains low, the approach would allow independent auditors to check safety properties of proprietary hardware or machine-learning models without access to their internals.
  • Combining the schemes with existing succinct proof systems could further reduce communication cost for large state spaces.

Load-bearing premise

Efficient zero-knowledge proofs exist for the algebraic statements that arise from ranking-function certificates and can be instantiated without prohibitive overhead on realistic systems.

What would settle it

A small, known-correct transition system or guarded-command program for which no zero-knowledge proof can be produced for its ranking-function certificate, or for which the resulting proof size and verification time exceed practical limits.

Figures

Figures reproduced from arXiv: 2605.00487 by Jacob Swales, Mirco Giacobbe, Pascal Berrang, Xiao Yang.

Figure 1
Figure 1. Figure 1: Non-Interactive ZKMC Scheme As illustrated in view at source ↗
Figure 2
Figure 2. Figure 2: (a) 3-Way Handshake with Exponential Backoff and (b) Nondeterministic Büchi Automaton for view at source ↗
Figure 3
Figure 3. Figure 3: Construction of our Explicit-State ZKMC Protocol view at source ↗
Figure 4
Figure 4. Figure 4: Primitives of our Symbolic ZKMC Protocol view at source ↗
Figure 5
Figure 5. Figure 5: Construction of our Symbolic ZKMC Protocol view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper introduces a technology for formally verifying that a secret software system satisfies a public temporal specification of functional correctness. It combines deductive model checking via ranking-function certificates with zero-knowledge proofs, presenting an explicit-state scheme (using polynomial commitments over secret transition graphs) and a symbolic scheme (using Farkas' lemma on linear guarded commands together with sigma protocols for matrix multiplication and range proofs). A prototype implementation is evaluated on LTL verification examples.

Significance. If the ZK instantiations prove efficient at scale, the work would enable formal verification in safety-critical domains where the system itself must remain confidential. The explicit composition of ranking functions with polynomial commitments and sigma protocols is a novel contribution, and the existence of a working prototype is a positive indicator of feasibility for small instances. The approach bridges formal methods and cryptography in a way that could support new applications in proprietary or regulated software.

major comments (2)
  1. [Prototype and evaluation section] The central practicality claim rests on the ZK proofs for ranking-function certificates (polynomial commitments in the explicit-state case and Farkas witnesses in the symbolic case) remaining efficient as the number of states, transitions, or variables grows. The prototype evaluation only reports results on small LTL examples; no scaling curves, asymptotic analysis, or comparison against standard model checkers is supplied to substantiate that overhead stays acceptable for realistic systems.
  2. [Symbolic scheme description] In the symbolic scheme, the reduction via Farkas' lemma produces a witness containing both public and secret components; the security argument that the sigma protocols for matrix multiplication and range proofs leak nothing about the secret system components needs an explicit hybrid argument or simulation proof, which is not provided.
minor comments (2)
  1. [Preliminaries] Notation for the piecewise-linear ranking functions and the guarded-command syntax should be introduced with a small running example before the general construction.
  2. [Introduction] The abstract states that both schemes support LTL verification, but the body should clarify which fragment of LTL is handled and how the ranking functions are derived for liveness properties.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their constructive feedback and positive assessment of the novelty and potential applications of our work. We address each major comment below and outline the revisions we will make to the manuscript.

read point-by-point responses

  1. Referee: [Prototype and evaluation section] The central practicality claim rests on the ZK proofs for ranking-function certificates (polynomial commitments in the explicit-state case and Farkas witnesses in the symbolic case) remaining efficient as the number of states, transitions, or variables grows. The prototype evaluation only reports results on small LTL examples; no scaling curves, asymptotic analysis, or comparison against standard model checkers is supplied to substantiate that overhead stays acceptable for realistic systems.

    Authors: We acknowledge that the current prototype evaluation demonstrates feasibility on small LTL instances but does not include scaling curves or direct comparisons. In the revised manuscript we will add a dedicated complexity analysis section deriving the asymptotic growth of proof size, prover time, and verifier time for both schemes in terms of the number of states (explicit case) and variables (symbolic case). We will also report additional experimental results on larger synthetic transition systems and guarded-command programs, together with a qualitative comparison to the overhead of standard explicit-state and symbolic model checkers, while clarifying that the cryptographic cost is the necessary price for confidentiality. revision: yes

  2. Referee: [Symbolic scheme description] In the symbolic scheme, the reduction via Farkas' lemma produces a witness containing both public and secret components; the security argument that the sigma protocols for matrix multiplication and range proofs leak nothing about the secret system components needs an explicit hybrid argument or simulation proof, which is not provided.

    Authors: We thank the referee for this observation. While the manuscript relies on the standard zero-knowledge properties of the matrix-multiplication and range-proof sigma protocols, we agree that an explicit composition argument is required. In the revised version we will insert a new security subsection that presents a hybrid argument: the first hybrid replaces the secret witness components with simulated values using the zero-knowledge simulator of the sigma protocols; the second hybrid replaces the polynomial commitments with hiding commitments. The argument shows that the verifier's view is computationally indistinguishable from a simulated view that uses only the public ranking-function certificate and the public specification. revision: yes

Circularity Check

0 steps flagged

No significant circularity; construction composes independent primitives

full rationale

The paper's derivation chain introduces explicit-state and symbolic ZK model-checking schemes by combining ranking-function certificates (from deductive model checking) with standard cryptographic tools (polynomial commitments, Farkas' lemma, sigma protocols for matrix multiplication and range proofs). No equation or claim reduces to a fitted parameter renamed as a prediction, no self-definition of the target result, and no load-bearing step justified solely by self-citation. The central feasibility claim rests on the existence and efficiency of ZK instantiations for the resulting algebraic statements, which is an external assumption rather than a circular reduction. The prototype serves as empirical support without forcing the outcome by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The approach rests on standard cryptographic assumptions for zero-knowledge proofs and on the existence of ranking functions from classical model-checking theory; no new free parameters or invented entities are introduced in the abstract.

axioms (2)
  • domain assumption Soundness and completeness of the underlying zero-knowledge proof systems (sigma protocols, polynomial commitments)
    Invoked when claiming that the verifier is convinced without learning the secret system.
  • domain assumption Existence of suitable ranking functions for the systems under consideration
    Taken from deductive model checking; required for the certificate to exist.

pith-pipeline@v0.9.0 · 5500 in / 1314 out tokens · 46031 ms · 2026-05-09T19:34:45.341646+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

78 extracted references · 8 canonical work pages · 1 internal anchor

  1. [1]

    Alessandro Abate, Daniele Ahmed, Mirco Giacobbe, and Andrea Peruffo. 2021. Formal Synthesis of Lyapunov Neural Networks.IEEE Control. Syst. Lett.5, 3 (2021), 773–778

    2021

  2. [2]

    Alessandro Abate, Alec Edwards, Mirco Giacobbe, Hashan Punchihewa, and Diptarko Roy. 2026. Quantitative Verification with Neural Networks.Log. Methods Comput. Sci.22, 2 (2026)

    2026

  3. [3]

    Alessandro Abate, Mirco Giacobbe, Sergey Ichtchenko, and Diptarko Roy. 2026. Complete Supermartingale Certificates for 𝜔-Regular Properties. InLICS. To appear

    2026

  4. [4]

    Alessandro Abate, Mirco Giacobbe, and Diptarko Roy. 2024. Stochastic Omega- Regular Verification and Control with Supermartingales. InCA V (3) (Lecture Notes in Computer Science). Springer, 395–419

    2024

  5. [5]

    Alessandro Abate, Mirco Giacobbe, and Diptarko Roy. 2025. Quantitative Super- martingale Certificates. InCA V (2) (Lecture Notes in Computer Science). Springer, 3–28

    2025

  6. [6]

    2015.Principles of cyber-physical systems

    Rajeev Alur. 2015.Principles of cyber-physical systems. MIT press

    2015

  7. [7]

    Henzinger

    Rajeev Alur and Thomas A. Henzinger. 1996. Reactive Modules. InLICS. IEEE Computer Society, 207–218

    1996

  8. [8]

    arkworks contributors. 2022. arkworks zkSNARK ecosystem. https://arkworks.rs

    2022

  9. [9]

    Edoardo Bacci, Mirco Giacobbe, and David Parker. 2021. Verifying Reinforcement Learning up to Infinity. InIJCAI. ijcai.org, 2154–2160

    2021

  10. [10]

    2008.Principles of model checking

    Christel Baier and Joost-Pieter Katoen. 2008.Principles of model checking. MIT Press

    2008

  11. [11]

    Barrett, Roberto Sebastiani, Sanjit A

    Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. 2009. Satisfiability Modulo Theories. InHandbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, Vol. 185. IOS Press, 825–885

    2009

  12. [12]

    Mihir Bellare and Oded Goldreich. 1992. On Defining Proofs of Knowledge. InAdvances in Cryptology - CRYPTO ’92, 12th Annual International Cryptol- ogy Conference, Santa Barbara, California, USA, August 16-20, 1992, Proceedings (Lecture Notes in Computer Science), Ernest F. Brickell (Ed.). Springer, 390–420. doi:10.1007/3-540-48071-4_28

    work page doi:10.1007/3-540-48071-4_28 1992

  13. [13]

    Dan Boneh, Ben Lynn, and Hovav Shacham. 2001. Short Signatures from the Weil Pairing. InAdvances in Cryptology - ASIACRYPT 2001, 7th International Conference on the Theory and Application of Cryptology and Information Security, Gold Coast, Australia, December 9-13, 2001, Proceedings (Lecture Notes in Computer Science), Colin Boyd (Ed.). Springer, 514–532....

    work page doi:10.1007/3-540-45682-1_30 2001

  14. [14]

    Benedikt Bünz, Jonathan Bootle, Dan Boneh, Andrew Poelstra, Pieter Wuille, and Greg Maxwell. 2018. Bulletproofs: Short proofs for confidential transactions and more. In2018 IEEE symposium on security and privacy (SP). IEEE, 315–334

    2018

  15. [15]

    Burch, Edmund M

    Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, and L. J. Hwang. 1990. Symbolic Model Checking:10 20 States and Beyond. InLICS. IEEE Computer Society, 428–439

    1990

  16. [16]

    Ya-Chien Chang, Nima Roohi, and Sicun Gao. 2019. Neural Lyapunov Control. InNeurIPS. 3240–3249

    2019

  17. [17]

    David Chaum and Torben Pryds Pedersen. 1992. Wallet Databases with Observers. InCRYPTO (Lecture Notes in Computer Science, Vol. 740). Springer, 89–105

    1992

  18. [18]

    Clarke, Orna Grumberg, Daniel Kroening, Doron A

    Edmund M. Clarke, Orna Grumberg, Daniel Kroening, Doron A. Peled, and Helmut Veith. 2018.Model checking, 2nd Edition. MIT Press

    2018

  19. [19]

    Michael Colón, Sriram Sankaranarayanan, and Henny Sipma. 2003. Linear Invariant Generation Using Non-linear Constraint Solving. InComputer Aided Verification, 15th International Conference, CA V 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings (Lecture Notes in Computer Science), Warren A. Hunt Jr. and Fabio Somenzi (Eds.). Springer, 420–432. doi:10.1...

    work page doi:10.1007/978-3-540-45069-6_39 2003

  20. [20]

    Michael Colón and Henny Sipma. 2001. Synthesis of Linear Ranking Functions. InTACAS (Lecture Notes in Computer Science, Vol. 2031). Springer, 67–81

    2001

  21. [21]

    Mingshu Cong, Tsz Hon Yuen, and Siu-Ming Yiu. 2024. zkMatrix: Batched Short Proof for Committed Matrix Multiplication. InAsiaCCS. ACM

    2024

  22. [22]

    Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, and Moshe Y. Vardi. 2007. Proving that programs eventually do something good. In POPL. ACM, 265–276

    2007

  23. [23]

    Byron Cook, Heidy Khlaaf, and Nir Piterman. 2015. Fairness for Infinite-State Systems. InTACAS (Lecture Notes in Computer Science). Springer, 384–398

    2015

  24. [24]

    Geoffroy Couteau, Michael Klooß, Huang Lin, and Michael Reichle. 2021. Efficient Range Proofs with Transparent Setup from Bounded Integer Commitments. In EUROCRYPT (3) (Lecture Notes in Computer Science, Vol. 12698). Springer, 247–277

    2021

  25. [25]

    Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 Theorem Prover and Programming Language. InCADE (Lecture Notes in Computer Science, Vol. 12699). Springer, 625–635

    2021

  26. [26]

    Leonardo Mendonça de Moura and Nikolaj S. Bjørner. 2008. Z3: An Efficient SMT Solver. InTACAS (Lecture Notes in Computer Science, Vol. 4963). Springer, 337–340

    2008

  27. [27]

    Leonardo Mendonça de Moura and Nikolaj S. Bjørner. 2011. Satisfiability modulo theories: introduction and applications.Commun. ACM54, 9 (2011), 69–77

    2011

  28. [28]

    Rayna Dimitrova, Luis María Ferrer Fioriti, Holger Hermanns, and Rupak Ma- jumdar. 2016. Probabilistic CTL*: The Deductive Way. InTACAS (Lecture Notes in Computer Science). Springer, 280–296

    2016

  29. [29]

    Ralph Droms. 1997. Dynamic Host Configuration Protocol. RFC 2131. doi:10. 17487/RFC2131

    1997

  30. [30]

    Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, An- toine Martin, Jérôme Dubois, Clément Gillard, and Henrich Lauko. 2022. From Spot 2.0 to Spot 2.10: What’s New?. InCA V (2) (Lecture Notes in Computer Science, Vol. 13372). Springer, 174–187

    2022

  31. [31]

    Julius Farkas. 1902. Theorie der einfachen Ungleichungen.Journal für die reine und angewandte Mathematik (Crelles Journal)1902, 124 (1902), 1–27

    1902

  32. [32]

    Amos Fiat and Adi Shamir. 1986. How to Prove Yourself: Practical Solutions to Identification and Signature Problems. InAdvances in Cryptology - CRYPTO ’86, Santa Barbara, California, USA, 1986, Proceedings (Lecture Notes in Computer Science), Andrew M. Odlyzko (Ed.). Springer, 186–194

    1986

  33. [33]

    Robert W. Floyd. 1993. Assigning Meanings to Programs. InProgram Verification. Springer Netherlands, 65–81

    1993

  34. [34]

    Williamson, and Oana Ciobotaru

    Ariel Gabizon, Zachary J. Williamson, and Oana Ciobotaru. 2019. PLONK: Permutations over Lagrange-bases for Oecumenical Noninteractive arguments of Knowledge.IACR Cryptol. ePrint Arch.2019 (2019), 953. https://eprint.iacr. org/2019/953

    2019

  35. [35]

    Schneider, B

    Steven D. Galbraith, Kenneth G. Paterson, and Nigel P. Smart. 2008. Pairings for cryptographers.Discret. Appl. Math.156, 16 (2008), 3113–3121. doi:10.1016/J. DAM.2007.12.010

    work page doi:10.1016/j 2008

  36. [37]

    InNeurIPS

    Neural Model Checking. InNeurIPS

  37. [38]

    Mirco Giacobbe, Daniel Kroening, Abhinandan Pal, and Michael Tautschnig

  38. [39]

    InNeurIPS

    Let a Neural Network be Your Invariant. InNeurIPS

  39. [40]

    Mirco Giacobbe, Daniel Kroening, and Julian Parsert. 2022. Neural termination analysis. InESEC/SIGSOFT FSE. ACM, 633–645

    2022

  40. [41]

    Jens Groth. 2016. On the Size of Pairing-Based Non-interactive Arguments. In Advances in Cryptology - EUROCRYPT 2016 - 35th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Vienna, Austria, May 8-12, 2016, Proceedings, Part II (Lecture Notes in Computer Science), Marc Fischlin and Jean-Sébastien Coron (Eds.). Spr...

    work page doi:10.1007/978-3-662-49896- 2016

  41. [42]

    Makowsky, and Willem P

    Orna Grumberg, Nissim Francez, Johann A. Makowsky, and Willem P. de Roever

  42. [43]

    Control.66, 1/2 (1985), 83–102

    A Proof Rule for Fair Termination of Guarded Commands.Inf. Control.66, 1/2 (1985), 83–102

    1985

  43. [44]

    Thomas Hader and Alex Ozdemir. 2024. An SMT-LIB Theory of Finite Fields. In Proceedings of the 22nd International Workshop on Satisfiability Modulo Theories (SMT 2024), Montreal, Canada, July, 22-23, 2024., Vol. 3725. CEUR Workshop Proceedings

    2024

  44. [45]

    Henzinger, Mahyar Karimi, and K

    Thomas A. Henzinger, Mahyar Karimi, and K. S. Thejaswini. 2025. Privacy- Preserving Runtime Verification. InCCS. ACM, 2774–2787

    2025

  45. [46]

    Henzinger, Kaushik Mallik, Pouya Sadeghi, and Dorde Zikelic

    Thomas A. Henzinger, Kaushik Mallik, Pouya Sadeghi, and Dorde Zikelic. 2025. Supermartingale Certificates for Quantitative Omega-Regular Verification and Control. InCA V (2) (Lecture Notes in Computer Science). Springer, 29–55

    2025

  46. [47]

    Holzmann

    Gerard J. Holzmann. 2018. Explicit-State Model Checking. InHandbook of Model Checking. Springer, 153–171

    2018

  47. [48]

    Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. 2017. Safety Verification of Deep Neural Networks. InCA V (1) (Lecture Notes in Computer Science). Springer, 3–29

    2017

  48. [49]

    Samuel Judson, Ning Luo, Timos Antonopoulos, and Ruzica Piskac. 2020. Pri- vacy Preserving CTL Model Checking through Oblivious Graph Algorithms. In WPES@CCS. ACM, 101–115

    2020

  49. [50]

    Zaverucha, and Ian Goldberg

    Aniket Kate, Gregory M. Zaverucha, and Ian Goldberg. 2010. Constant-Size Commitments to Polynomials and Their Applications. InASIACRYPT (Lecture Notes in Computer Science, Vol. 6477). Springer, 177–194

    2010

  50. [51]

    2014.Introduction to Modern Cryptography, Second Edition

    Jonathan Katz and Yehuda Lindell. 2014.Introduction to Modern Cryptography, Second Edition. CRC Press

    2014

  51. [52]

    2016.Decision Procedures - An Algorithmic Point of View, Second Edition

    Daniel Kroening and Ofer Strichman. 2016.Decision Procedures - An Algorithmic Point of View, Second Edition. Springer

    2016

  52. [53]

    Orna Kupferman and Moshe Y. Vardi. 2005. From complementation to certifica- tion.Theor. Comput. Sci.345, 1 (2005), 83–100

    2005

  53. [54]

    Satoshi Kura and Hiroshi Unno. 2025. A Hierarchy of Supermartingales for 𝜔-Regular Verification.CoRRabs/2512.00270 (2025)

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  54. [55]

    Leslie Lamport. 1983. Specifying Concurrent Program Modules.ACM Trans. Program. Lang. Syst.5, 2 (1983), 190–222

    1983

  55. [56]

    Evan Laufer, Alex Ozdemir, and Dan Boneh. 2024. zkPi: Proving Lean Theorems in Zero-Knowledge. InCCS. ACM, 4301–4315. Berrang et al

    2024

  56. [57]

    Hen- zinger

    Mathias Lechner, Dorde Zikelic, Krishnendu Chatterjee, and Thomas A. Hen- zinger. 2022. Stability Verification in Stochastic Control Systems via Neural Network Supermartingales. InAAAI. AAAI Press, 7326–7336

    2022

  57. [58]

    Kolesar, Timos Antonopoulos, William R

    Daniel Luick, John C. Kolesar, Timos Antonopoulos, William R. Harris, James Parker, Ruzica Piskac, Eran Tromer, Xiao Wang, and Ning Luo. 2024. ZKSMT: A VM for Proving SMT Theorems in Zero Knowledge. InUSENIX Security Sympo- sium. USENIX Association

    2024

  58. [59]

    Harris, Ruzica Piskac, Eran Tromer, and Xiao Wang

    Ning Luo, Timos Antonopoulos, William R. Harris, Ruzica Piskac, Eran Tromer, and Xiao Wang. 2022. Proving UNSAT in Zero Knowledge. InCCS. ACM, 2203– 2217

    2022

  59. [60]

    Zohar Manna and Amir Pnueli. 1990. A Hierarchy of Temporal Properties. In PODC. ACM, 377–410

    1990

  60. [61]

    Grigory Neustroev, Mirco Giacobbe, and Anna Lukina. 2025. Neural Continuous- Time Supermartingale Certificates. InAAAI. AAAI Press, 27538–27546

    2025

  61. [62]

    numerous contributors. 2022. bls_bulletproofs. https://github.com/maidsafe/ bls_bulletproofs

    2022

  62. [63]

    Pedersen

    Torben P. Pedersen. 1991. Non-Interactive and Information-Theoretic Secure Verifiable Secret Sharing. InAdvances in Cryptology - CRYPTO ’91, 11th Annual International Cryptology Conference, Santa Barbara, California, USA, August 11-15, 1991, Proceedings (Lecture Notes in Computer Science), Joan Feigenbaum (Ed.). Springer, 129–140. doi:10.1007/3-540-46766-1_9

    work page doi:10.1007/3-540-46766-1_9 1991

  63. [64]

    Amir Pnueli. 1977. The Temporal Logic of Programs. InFOCS. IEEE Computer Society, 46–57

    1977

  64. [65]

    Andreas Podelski and Andrey Rybalchenko. 2004. A Complete Method for the Synthesis of Linear Ranking Functions. InVMCAI (Lecture Notes in Computer Science, Vol. 2937). Springer, 239–251

    2004

  65. [66]

    Jon Postel. 1981. Transmission Control Protocol. RFC 793. doi:10.17487/RFC0793

    work page doi:10.17487/rfc0793 1981

  66. [67]

    Stephen Prajna and Ali Jadbabaie. 2004. Safety Verification of Hybrid Systems Using Barrier Certificates. InHSCC (Lecture Notes in Computer Science). Springer, 477–492

    2004

  67. [68]

    Stephen Prajna, Ali Jadbabaie, and George J. Pappas. 2004. Stochastic safety verification using barrier certificates. InCDC. IEEE, 929–934

    2004

  68. [69]

    Luca Pulina and Armando Tacchella. 2010. An Abstraction-Refinement Approach to Verification of Artificial Neural Networks. InCA V (Lecture Notes in Computer Science). Springer, 243–257

    2010

  69. [70]

    RISC Zero, Inc. 2024. RISC Zero: A General-Purpose Zero-Knowledge Computing Platform. https://www.risczero.com. Accessed 2025

    2024

  70. [71]

    Goodfellow, and Rob Fergus

    Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian J. Goodfellow, and Rob Fergus. 2014. Intriguing properties of neural networks. InICLR (Poster)

    2014

  71. [72]

    Johnson, and Xenofon D

    Hoang-Dung Tran, Feiyang Cai, Diego Manzanas Lopez, Patrick Musau, Taylor T. Johnson, and Xenofon D. Koutsoukos. 2019. Safety Verification of Cyber-Physical Systems with Reinforcement Learning Control.ACM Trans. Embed. Comput. Syst.18, 5s (2019), 105:1–105:22

    2019

  72. [73]

    Hoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak, and Taylor T. Johnson. 2020. NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems. InCA V (1) (Lecture Notes in Computer Science). Springer, 3–17

    2020

  73. [74]

    Caterina Urban, Arie Gurfinkel, and Temesghen Kahsai. 2016. Synthesizing Ranking Functions from Bits and Pieces. InTACAS (Lecture Notes in Computer Science, Vol. 9636). Springer, 54–70

    2016

  74. [75]

    Moshe Y. Vardi. 1991. Verification of Concurrent Programs: The Automata- Theoretic Framework.Ann. Pure Appl. Log.51, 1-2 (1991), 79–98

    1991

  75. [76]

    Vardi and Pierre Wolper

    Moshe Y. Vardi and Pierre Wolper. 1986. An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report). InLICS. IEEE Computer Society, 332–344

    1986

  76. [77]

    Zico Kolter

    Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J. Zico Kolter. 2021. Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Neural Network Robustness Verification. InNeurIPS. 29909– 29921

    2021

  77. [78]

    Henzinger, and Krishnendu Chatter- jee

    Dorde Zikelic, Mathias Lechner, Thomas A. Henzinger, and Krishnendu Chatter- jee. 2023. Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees. InAAAI. AAAI Press, 11926–11935

    2023

  78. [79]

    Henzinger

    Dorde Zikelic, Mathias Lechner, Abhinav Verma, Krishnendu Chatterjee, and Thomas A. Henzinger. 2023. Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees. InNeurIPS. A Open Science We provide three tools and prototypes, as well as a series of bench- mark data files, that enable the program committee to evaluate the paper’s co...

    2023