pith. sign in

arxiv: 2606.23768 · v1 · pith:F6WVCYQEnew · submitted 2026-06-22 · 💻 cs.CR · cs.AI· cs.LO

Cryptographic certificates of validity for trustworthy AI

Murdoch J. Gabbay This is my paper

Pith reviewed 2026-06-26 07:37 UTC · model grok-4.3

classification 💻 cs.CR cs.AIcs.LO
keywords cryptographic certificatesAI policy compliancesuccinct proofszero-knowledge proofsagentic AIproof-carrying codetrustworthy AIformal methods
0
0 comments X

The pith

An AI agent's action can carry a cryptographic proof that it satisfies an agreed formal policy without the verifier needing to trust the agent or re-execute the work.

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

The paper proposes compiling a policy or correctness condition into a logical predicate that reduces to a witness-checking problem over polynomial constraints. A succinct cryptographic proof system then produces a short, independently verifiable certificate that the condition holds for the agent's action. This sits between full formal verification of source code and ordinary cryptographic authentication of identity. A reader would care because it lets verifiers confirm compliance at low cost even when the agent is untrusted and the computation is expensive. The approach therefore offers a route to auditable agent behavior in settings where re-running everything is impractical.

Core claim

The paper claims that any relevant correctness or policy condition can be specified as a logical predicate, compiled to a witness-checking problem over polynomial constraints, and then certified by a succinct cryptographic proof system (optionally zero-knowledge) so that an agent's action is accompanied by an independently checkable proof that the policy holds.

What carries the argument

Succinct cryptographic proof systems applied to policy predicates compiled into polynomial constraint systems, which generate short certificates of validity.

If this is right

  • Verification reduces to checking the short proof rather than re-executing the agent's computation.
  • Zero-knowledge variants can certify compliance while keeping the agent's internal state private.
  • The method supplies a middle ground between source-code formal verification and simple cryptographic authentication.
  • Policy specification and auditing become the main deployment tasks once the proof system is in place.

Where Pith is reading between the lines

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

  • Proofs could be archived on public ledgers to create transparent records of AI decisions over time.
  • The same compilation pipeline might be reused across multiple agents or regulators sharing the same policy language.
  • Efficiency gains would be largest for policies whose predicates map cleanly to low-degree polynomial constraints.

Load-bearing premise

Any relevant policy or correctness condition can be expressed as a logical predicate that compiles to a witness-checking problem over polynomial constraints admitting efficient succinct proofs.

What would settle it

A concrete policy condition that cannot be compiled into such a polynomial constraint system without the resulting proofs becoming impractically large or slow to verify.

Figures

Figures reproduced from arXiv: 2606.23768 by Murdoch J. Gabbay.

Figure 1
Figure 1. Figure 1: Syntax of terms and predicates (Definition [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Polynomial semantics for terms and predicates (Defini [PITH_FULL_IMAGE:figures/full_fig_p002_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Table of semantic meaning (Remark 3.2) much as logic gates are compact and theoretical: by compos￾ing together simple components we attain great expressivity, and by suitable implementation we can accomplish remark￾able things. We give the reader a taste of how this works. Example 3.1. We can express truth as 0= 0 and false as 0= 1. The reader can check that [[0 = 0]]ς = 0 (thus ⊨ς 0 = 0) and [[0 = 1]]ς = … view at source ↗
Figure 4
Figure 4. Figure 4: Exponentiation a b (Definitions 3.3 and 3.6) Example 3.8. We illustrate some values for ς(pow) such that ⊨ς χpow, so that by Lemma 3.7 they encode a partial power function:   2 2 2 0 1 2 1 2 4 1 1 2     2 2 2 2 1 0 4 2 1 2 3 3     2 2 2 2 0 2 1 0 1 4 2 1 2 3 1 1     3 2 3 2 0 0 1 1 1 1 3 2 1 1 1 2   These all represent the derivation-tree from Remark 3.4: 1. The leftmost matrix enco… view at source ↗
read the original abstract

We propose cryptographic certificates of validity for agentic AI systems. The core idea is to formally specify a correctness or policy condition as a logical predicate, compile this predicate to a witness-checking problem over polynomial constraints, and use a succinct cryptographic proof system (and optionally zero-knowledge) to certify that the condition holds. This offers a middle ground between formal verification of source code, and cryptographic authentication. An agent's action can be accompanied by an independently checkable proof that it satisfies an agreed formal policy, without requiring the verifier to trust the agent or to re-execute computation. We outline the approach at a high level, give the core mathematical translation, relate the proposal to proof-carrying code, zkVMs, formal methods, and agent governance, and note the specification, auditing, and deployment questions that a full implementation must answer.

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 / 1 minor

Summary. The manuscript proposes cryptographic certificates of validity for agentic AI systems. It suggests formally specifying a correctness or policy condition as a logical predicate, compiling the predicate to a witness-checking problem over polynomial constraints (e.g., R1CS or AIR), and using a succinct cryptographic proof system (optionally with zero-knowledge) to certify that the condition holds for an agent's action. This provides an independently checkable proof without requiring the verifier to trust the agent or re-execute the computation. The paper outlines the approach at a high level, presents the core mathematical translation, relates the idea to proof-carrying code, zkVMs, formal methods, and agent governance, and identifies open questions around specification, auditing, and deployment for a full implementation.

Significance. If the central modeling assumption holds and relevant AI policies can be compiled to succinct-proof instances with practical costs, the approach would supply a useful middle ground between full formal verification of AI systems and simple cryptographic authentication, supporting verifiable compliance in agent governance. The manuscript appropriately credits connections to existing primitives such as proof-carrying code and zkVMs rather than claiming novel cryptographic constructions. The significance remains prospective, however, because the work is positioned as an outline rather than a demonstration with concrete reductions or examples.

major comments (2)
  1. [core mathematical translation section] Core mathematical translation section: the manuscript asserts that any agreed formal policy can be expressed as a logical predicate that compiles to a witness-checking problem over polynomial constraints admitting efficient succinct proofs, but supplies neither a worked example of a non-trivial policy (such as an output-safety or fairness constraint) nor any complexity bound showing that the resulting circuit size or prover time remains sub-linear in the underlying AI computation. This assumption is load-bearing for the practicality claim.
  2. [outline of the approach section] Outline of the approach section: no security reduction or composition argument is given for how the AI execution trace is incorporated into the witness or how the proof system interacts with the agent runtime; without this, it is unclear whether the succinctness property survives the full pipeline from policy to verified action.
minor comments (1)
  1. [abstract] The abstract and introduction could include a brief comparison table or paragraph distinguishing the proposal from prior zkML and proof-carrying-code literature to clarify the incremental contribution.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the detailed and constructive review. The manuscript is explicitly positioned as a high-level outline of an approach rather than a complete implementation or formal analysis, which informs our responses below. We address each major comment and indicate planned revisions.

read point-by-point responses

  1. Referee: [core mathematical translation section] Core mathematical translation section: the manuscript asserts that any agreed formal policy can be expressed as a logical predicate that compiles to a witness-checking problem over polynomial constraints admitting efficient succinct proofs, but supplies neither a worked example of a non-trivial policy (such as an output-safety or fairness constraint) nor any complexity bound showing that the resulting circuit size or prover time remains sub-linear in the underlying AI computation. This assumption is load-bearing for the practicality claim.

    Authors: We agree that the manuscript provides no concrete worked example of a non-trivial policy nor explicit complexity bounds. This follows from the paper's scope as an outline identifying the core translation and open questions rather than demonstrating a full system. In revision we will insert a short illustrative example (e.g., a simple output-safety predicate compiled to an R1CS instance) in the core mathematical translation section to make the claim more concrete. General complexity bounds that hold for arbitrary AI models and policies remain outside the present scope and would require case-by-case analysis of specific AI architectures; we will note this limitation explicitly. revision: partial

  2. Referee: [outline of the approach section] Outline of the approach section: no security reduction or composition argument is given for how the AI execution trace is incorporated into the witness or how the proof system interacts with the agent runtime; without this, it is unclear whether the succinctness property survives the full pipeline from policy to verified action.

    Authors: The manuscript does not supply a formal security reduction or detailed composition argument because it relies on the established properties of existing succinct proof systems (e.g., those used in zkVMs) once a policy has been compiled to a constraint system. The AI execution trace would enter the witness via standard techniques such as zkVM execution of the agent, preserving succinctness by construction. In revision we will add a clarifying paragraph in the outline of the approach section that sketches this incorporation at the level of the existing primitives, while acknowledging that a full end-to-end composition theorem is left for future work. revision: partial

Circularity Check

0 steps flagged

No significant circularity; proposal is self-contained outline of existing primitives

full rationale

The manuscript is a high-level proposal that specifies a policy as a logical predicate, compiles it to a witness-checking problem over polynomial constraints, and certifies it via succinct proofs. No equations appear, no parameters are fitted to data, and no self-citations are invoked as load-bearing uniqueness theorems. The approach rests on standard cryptographic primitives (R1CS, AIR, zk-SNARKs) whose properties are treated as external and independently established. The central claim is therefore not reduced to its own inputs by construction and receives the default non-circular finding.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The proposal assumes the existence of a compilation from logical predicates to polynomial witness problems that supports succinct proofs, without supplying evidence or bounds for that step.

axioms (1)
  • domain assumption Logical predicates expressing AI policies can be compiled to witness-checking problems over polynomial constraints that admit succinct cryptographic proofs
    This compilation step is stated as the core mathematical translation but is not demonstrated or bounded in the abstract.

pith-pipeline@v0.9.1-grok · 5660 in / 1171 out tokens · 21507 ms · 2026-06-26T07:37:10.937519+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

33 extracted references · 26 canonical work pages

  1. [1]

    Jolt: SNARKs for virtual machines via lookups

    Arasu Arun, Srinath Setty, and Justin Thaler. Jolt: SNARKs for virtual machines via lookups. In Advances in Cryptology -- EUROCRYPT 2024 , volume 14656 of Lecture Notes in Computer Science , pages 3--33. Springer, 2024. 10.1007/978-3-031-58751-1_1

    work page doi:10.1007/978-3-031-58751-1_1 2024

  2. [2]

    A verified algebraic representation of cairo program execution, 2021

    Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, and Alon Titelman. A verified algebraic representation of cairo program execution, 2021. 10.48550/arXiv.2109.14534

    work page doi:10.48550/arxiv.2109.14534 2021

  3. [3]

    SNARKs for C : Verifying program executions succinctly and in zero knowledge

    Eli Ben-Sasson, Alessandro Chiesa, Daniel Genkin, Eran Tromer, and Madars Virza. SNARKs for C : Verifying program executions succinctly and in zero knowledge. In Advances in Cryptology -- CRYPTO 2013 , volume 8043 of Lecture Notes in Computer Science , pages 90--108. Springer, 2013. 10.1007/978-3-642-40084-1_6

    work page doi:10.1007/978-3-642-40084-1_6 2013

  4. [4]

    Interactive oracle proofs

    Eli Ben-Sasson, Alessandro Chiesa, and Nicholas Spooner. Interactive oracle proofs. In Theory of Cryptography , volume 9986 of Lecture Notes in Computer Science , pages 31--60. Springer, 2016. 10.1007/978-3-662-53644-5_2

    work page doi:10.1007/978-3-662-53644-5_2 2016

  5. [5]

    Halo infinite: Proof-carrying data from additive polynomial commitments

    Dan Boneh, Justin Drake, Ben Fisch, and Ariel Gabizon. Halo infinite: Proof-carrying data from additive polynomial commitments. In Advances in Cryptology -- CRYPTO 2021 , volume 12825 of Lecture Notes in Computer Science , pages 649--680. Springer, 2021. 10.1007/978-3-030-84242-0_23

    work page doi:10.1007/978-3-030-84242-0_23 2021

  6. [6]

    Transparent SNARKs from DARK compilers

    Benedikt B \"u nz, Ben Fisch, and Alan Szepieniec. Transparent SNARKs from DARK compilers. In Advances in Cryptology -- EUROCRYPT 2020 , volume 12105 of Lecture Notes in Computer Science , pages 677--706. Springer, 2020. 10.1007/978-3-030-45721-1_24

    work page doi:10.1007/978-3-030-45721-1_24 2020

  7. [7]

    i’m not sure, but

    Alan Chan, Carson Ezell, Max Kaufmann, Kevin Wei, Lewis Hammond, Herbie Bradley, Emma Bluemke, Nitarshan Rajkumar, David Krueger, Noam Kolt, Lennart Heim, and Markus Anderljung. Visibility into AI agents. In Proceedings of the 2024 ACM Conference on Fairness, Accountability, and Transparency , FAccT '24, page 958–973, New York, NY, USA, 2024. Association ...

    work page doi:10.1145/3630106.3658948 2024

  8. [8]

    A core model for choreographic programming

    Lu \'i s Cruz-Filipe and Fabrizio Montesi. A core model for choreographic programming. In Formal Aspects of Component Software , volume 10231 of Lecture Notes in Computer Science , pages 17--35. Springer, 2017. 10.1007/978-3-319-57666-4_3

    work page doi:10.1007/978-3-319-57666-4_3 2017

  9. [9]

    Functional choreographic programming

    Lu \'i s Cruz-Filipe, Eva Graversen, Lovro Lugovi \'c , Fabrizio Montesi, and Marco Peressotti. Functional choreographic programming. In Theoretical Aspects of Computing -- ICTAC 2022 , Lecture Notes in Computer Science. Springer, 2022. 10.1007/978-3-031-17715-6_15

    work page doi:10.1007/978-3-031-17715-6_15 2022

  10. [10]

    A formal theory of choreographic programming

    Lu \'i s Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. A formal theory of choreographic programming. Journal of Automated Reasoning , 67, 2023. 10.1007/s10817-023-09665-3

    work page doi:10.1007/s10817-023-09665-3 2023

  11. [11]

    Halo2 : The Halo2 zero-knowledge proving system, 2026

    Electric Coin Company and Zcash Foundation . Halo2 : The Halo2 zero-knowledge proving system, 2026. Software repository; accessed 2 May 2026. https://github.com/zcash/halo2

    2026

  12. [12]

    Gabbay and Andrew Mendelsohn

    Murdoch J. Gabbay and Andrew Mendelsohn. SNARKs for First Order Logic . Talk presented by Mendelsohn at the Workshop on Cryptographic Tools for Blockchains https://www.ctb-workshop.org ( CTB 2026, permalink https://wayback-api.archive.org/web/20260608154418/https://www.ctb-workshop.org/), affiliated with Eurocrypt 2026, Rome, Italy, May 2026. Slides at ht...

    arXiv 2026

  13. [13]

    Murdoch J. Gabbay. Arithmetisation of computation via polynomial semantics for first-order logic. Cryptology ePrint Archive, Paper 2024/954, 2024. https://eprint.iacr.org/2024/954

    2024

  14. [14]

    Murdoch J. Gabbay. Arithmetising logic: polynomial semantics of FOL . Journal of Applied Logics , 12(6), October 2025. http://www.collegepublications.co.uk/downloads/ifcolog00074.pdf\#page=107

    2025

  15. [15]

    The ethics of advanced ai assistants, 2024

    Iason Gabriel, Arianna Manzini, Geoff Keeling, Lisa Anne Hendricks, Verena Rieser, Hasan Iqbal, Nenad Toma s ev, Ira Ktena, Zachary Kenton, Mikel Rodriguez, et al. The ethics of advanced ai assistants, 2024. 10.48550/arXiv.2404.16244

    work page doi:10.48550/arxiv.2404.16244 2024

  16. [16]

    Zinc: Succinct arguments with small arithmetization overheads from IOPs of proximity to the integers

    Albert Garreta, Hendrik Waldner, Ilia Vlasov, Katerina Hristova, Luca Dall'Ava, Marko C upi \'c , and Matthew Klein. Zinc: Succinct arguments with small arithmetization overheads from IOPs of proximity to the integers. In Advances in Cryptology -- CRYPTO 2025 , volume 16006 of Lecture Notes in Computer Science , pages 259--291. Springer Nature Switzerland...

    work page doi:10.1007/978-3-032-01907-3_9 2025

  17. [17]

    Cairo -- a T uring-complete STARK-friendly CPU architecture

    Lior Goldberg, Shahar Papini, and Michael Riabzev. Cairo -- a T uring-complete STARK-friendly CPU architecture. Cryptology ePrint Archive, Paper 2021/1063, 2021. https://eprint.iacr.org/2021/1063

    2021

  18. [18]

    On the size of pairing-based non-interactive arguments

    Jens Groth. On the size of pairing-based non-interactive arguments. In Advances in Cryptology -- EUROCRYPT 2016 , volume 9666 of Lecture Notes in Computer Science , pages 305--326. Springer, 2016. 10.1007/978-3-662-49896-5_11

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

  19. [19]

    Correctness by construction: Developing a commercial secure system

    Anthony Hall and Roderick Chapman. Correctness by construction: Developing a commercial secure system. IEEE Software , 19(1):18--25, 2002. 10.1109/52.976937

    work page doi:10.1109/52.976937 2002

  20. [20]

    C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM , 12(10):576--580, 1969. 10.1145/363235.363259

    work page doi:10.1145/363235.363259 1969

  21. [21]

    Multiparty asynchronous session types

    Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. Journal of the ACM , 63(1):1--67, 2016. 10.1145/2827695

    work page doi:10.1145/2827695 2016

  22. [22]

    Stephen C. Kleene. Recursive predicates and quantifiers. Transactions of the American Mathematical Society , 53:41--73, 1943. 10.1090/S0002-9947-1943-0007371-8

    work page doi:10.1090/s0002-9947-1943-0007371-8 1943

  23. [23]

    seL4: formal verification of an os kernel

    Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. sel4: Formal verification of an os kernel. In Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles , pages 207--220. ACM, 2009....

    work page doi:10.1145/1629575.1629596 2009

  24. [24]

    Communications of the ACM 52(7), 107–115 (Jul 2009).https://doi.org/10/c9sb7q,http://doi.acm.org/ 10.1145/1538788.1538814

    Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM , 52(7):107--115, 2009. 10.1145/1538788.1538814

    work page doi:10.1145/1538788.1538814 2009

  25. [25]

    A brief account of runtime verification.Journal of Logic and Algebraic Programming, 78(5):293–303, 2009

    Martin Leucker and Christian Schallhart. A brief account of runtime verification. The Journal of Logic and Algebraic Programming , 78(5):293--303, 2009. 10.1016/j.jlap.2008.08.004

    work page doi:10.1016/j.jlap.2008.08.004 2009

  26. [26]

    2023 , month =

    National Institute of Standards and Technology . Artificial intelligence risk management framework (ai rmf 1.0). Technical report, National Institute of Standards and Technology, 2023. 10.6028/NIST.AI.100-1

    work page doi:10.6028/nist.ai.100-1 2023

  27. [27]

    George C. Necula. Proof-carrying code. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages , pages 106--119. ACM, 1997. 10.1145/263699.263712

    work page doi:10.1145/263699.263712 1997

  28. [28]

    Pinocchio: Nearly practical verifiable computation

    Bryan Parno, Jon Howell, Craig Gentry, and Mariana Raykova. Pinocchio: Nearly practical verifiable computation. In 2013 IEEE Symposium on Security and Privacy , pages 238--252, 2013. 10.1109/SP.2013.47

    work page doi:10.1109/sp.2013.47 2013

  29. [29]

    RISC Zero zkVM Developer Documentation , 2026

    RISC Zero . RISC Zero zkVM Developer Documentation , 2026. Accessed 2026-05-25. https://dev.risczero.com/

    2026

  30. [30]

    Salgado and Steven M

    Abner J. Salgado and Steven M. Wise. Polynomial Interpolation , pages 231--265. Cambridge University Press, 2022. 10.1017/9781108942607

    work page doi:10.1017/9781108942607 2022

  31. [31]

    Srinath Setty, Justin Thaler, and Riad S. Wahby. Customizable constraint systems for succinct arguments. Cryptology ePrint Archive, Paper 2023/552, 2023. https://eprint.iacr.org/2023/552

    2023

  32. [32]

    Srinath Setty, Justin Thaler, and Riad S. Wahby. Unlocking the lookup singularity with lasso. In Advances in Cryptology -- EUROCRYPT 2024 , volume 14656 of Lecture Notes in Computer Science , pages 180--209. Springer, 2024. 10.1007/978-3-031-58751-1_7

    work page doi:10.1007/978-3-031-58751-1_7 2024

  33. [33]

    Proofs, Arguments, and Zero-Knowledge , volume 4 of Foundations and Trends in Privacy and Security

    Justin Thaler. Proofs, Arguments, and Zero-Knowledge , volume 4 of Foundations and Trends in Privacy and Security . Now Publishers, 2022. 10.1561/3300000030

    work page doi:10.1561/3300000030 2022