Cryptographic certificates of validity for trustworthy AI
arXiv:2606.23768v1 [cs.CR] 22 Jun 2026
Murdoch J. Gabbay Heriot-Watt University, Edinburgh, UK [email protected]
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 witnesschecking 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.
1
Introduction
Agentic AI systems are beginning to take actions, not merely produce recommendations. A travel assistant may book a flight; an enterprise agent may approve an invoice; a software agent may deploy code; a robotic agent may act in the physical world. For such systems a key question is: is this action authorised and policy compliant; is it correct? Cryptographic signatures traditionally authenticate origin, by certifying that the sender of a message knew a certain key. Logs can be used retrospectively to reconstruct events. However, cryptographic signatures, logs, and monitoring cannot prove that an action will satisfy correctness, safety, or compliance conditions in advance. In this paper, we propose a complementary mechanism: cryptographic certificates of validity for agent actions, before actions are carried out. The idea is simple. 1. Express the relevant policy or correctness condition as a formal specification in an appropriate logic. 2. Compile the resulting finite witness-checking problem to cryptography-friendly polynomial constraints (as we will sketch).
3. Require the agent or an associated prover to attach a succinct cryptographic proof that the constraints are satisfied. (In zero-knowledge settings, the verifier may check the certificate without learning private witness data.) The slogan is: do not trust an action because of its origin; trust it because it carries cryptographically checkable evidence of correctness. A note on scope may now be helpful. The mathematics in Section 2 is application-agnostic: it provides an arithmetisation of first-order logic validity to judgements on polynomial constraints. This may be useful wherever a verifier requires succinct cryptographic evidence that a stated condition holds. This builds a bridge from first-order specification to cryptographic certification. The setting of agentic AI makes the assurance problem concrete and urgent — autonomous action is a signal case in which origin-based authentication and posthoc logging may not be fully adequate. But the mathematical architecture which we use to address this problem — predicate → polynomial constraint → cryptographic certificate — is general, and might be usefully specialised to any domain where untrusted parties must provide checkable evidence of correctness. From this perspective, systems of AI agents are just heterogeneous distributed systems of agents who may be independently developed and may act according to their own priorities. They may also (to borrow a term from distributed systems) be Byzantine, meaning that they do not satisfy the expected specification. Our proposal is to make selected actions proof-carrying, in a very particular sense: for their action to be accepted, they must produce a cryptographic certificate of validity of their correctness predicate. Advanced AI assistants can plan and execute sequences of actions [Gabriel et al., 2024]. Thus we need accountability, which requires evidence of where, why, how, and by whom agents are used [Chan et al., 2024]. This paper offers a complementary assurance: further to identity, logging, and risk-management practices such as those articulated in the NIST AI Risk Management Framework [National Institute of Standards and Technology, 2023], selected agent actions should carry compact certificates that a formal specification has been validated. We can think of this as a cryptographic analogue of proof-carrying code [Necula, 1997], instantiated using succinct arguments and polynomial arithmetisation [Thaler, 2022; Gabbay, 2024; Gabbay, 2025;
t ::= X | a ∈ Z | t + t | t ∗ t | Ci (t) | len(C) | reify(ϕ) ϕ, ψ ::= t = t | ϕ ∧ ϕ | ϕ ∨ ϕ | ∀C X.ϕ | Ci < t | t < Ci Above, i∈[arity(C)]. These grammars are in BNF style, such that ϕ and t to the right of ::= represent any predicate or term. Thus ϕ ∧ ϕ denotes a conjunction of two (possibly non-equal) predicates, and t = t denotes two (possibly non-equal) terms. Figure 1: Syntax of terms and predicates (Definition 2.3)
[ X]]ς = X [ a]]ς = a [ t + t′ ] ς = [ t]]ς + [ t′ ] ς [ t ∗ t′ ] ς = [ t]]ς ∗ [ t′ ] ς [ Ci (t)]]ς = itplnt(ς(C)i )([[t]]ς ) [ len(C)]]ς = len(ς(C)) [ reify(ϕ)]]ς = [ ϕ]]ς [ t = t′ ] ς = ([[t]]ς − [ t′ ] ς )2 [ ϕ ∧ ϕ′ ] ς = P [ ϕ]]ς + [ ϕ′ ] ς [ ϕ ∨ ϕ′ ] ς = [ ϕ]]ς ∗ [ ϕ′ ] ς [ ∀C X.ϕ]]ς = x∈[len(ς(C))] [ ϕ]]ς (x) 0 ∀j∈[len(ς(C))].(ς(C)i,j < [ t]]ς (j)) [ Ci < t]]ς = 1 otherwise 0 ∀j∈[len(ς(C))].([[t]]ς (j) < ς(C)i,j ) [ t < Ci ] ς = 1 otherwise
Notation 2.5. An integer matrix is an element C ∈ Zar ×ln where ar ∈ N (for arity) is the number of rows and ln ∈ N (for length) is the number of columns. Write len(C) for ln the number of columns in C, which we may call the length of C. Write Ci for the ith row in C (a vector of length len(C)). Write Ci,j for the i, j-th element in C; i is the row number and j is the column number. Definition 2.6. Suppose ⃗a = (a1 , . . . , an ) ∈ Zln is a lntuple of integers, for ln ∈ N. Say that P ∈ Q[X] interpolates ⃗a at (1, 2, . . . , ln) when ∀x ∈ [ln].P (x) = ax . It is a fact [Salgado and Wise, 2022, Chapter 9] that every ⃗a ∈ Zln can be interpolated by a unique polynomial interpolant itplnt(a1 , . . . , aln ) ∈ Q[X] of degree at most ln91, so itplnt(a1 , . . . , aln )(x) = ax .1 Definition 2.7. 1. An interpretation ς assigns to C ∈ PolyFunc a matrix ς(C) ∈ Zarity(C)×len(ς(C)) . ς(C) always has arity(C) rows; the number of columns depends on ς. 2. Define semantics [ t]]ς , [ ϕ]]ς ∈ Q[X] as in Figure 2. 3. If x ∈ Z then define the (validity) judgement x ⊨ς ϕ to mean [ ϕ]]ς (x) = 0. If ϕ is closed (has no free variables) then define the (validity) judgement ⊨ς ϕ to mean [ ϕ]]ς (0) = 0.2
In clauses mentioned in Ci above, we insist on i ∈ [arity(C)] for well-formedness.
Lemma 2.8. [ ϕ]]ς (x) ≥ 0 for every x ∈ Q, and in particular for every x ∈ Z.
Figure 2: Polynomial semantics for terms and predicates (Definition 2.7)
Proof. Routine induction on Figure 2, noting that: for x, y ∈ Q, (x − y)2 ≥ 0; and for x, y ≥ 0, x + y, x ∗ y ≥ 0.
Garreta et al., 2025]. One final note, for the record: a certificate of validity for a formal specification does not in and of itself prove that the formal specification is the right specification. It proves, under the stated assumptions and to within appropriate soundness bounds of the underlying cryptographic back end, that the formal specification has been validated.
2
We can now prove soundness and completeness; validity with respect to the predicate connectives in Figure 1 behaves exactly as those symbols suggest: Theorem 2.9 ([Gabbay, 2024; Gabbay, 2025]). 1. x ⊨ς t = t′ if and only if [ t]]ς (x) = [ t′ ] ς (x). 2. x ⊨ς ϕ ∧ ϕ′ if and only if x ⊨ς ϕ ∧ x ⊨ς ϕ′ and x ⊨ς ϕ ∨ ϕ′ if and only if x ⊨ς ϕ ∨ x ⊨ς ϕ′ . 3. x ⊨ς ∀C X.ϕ if and only if x′ ⊨ς ϕ for every x′ ∈ [len(ς(C))]. 4. x ⊨ς t < Ci if and only if ς(C)i,j is strictly greater than [ t]]ς (j) for every j ∈ [len(ς(C))], and similarly for x ⊨ς Ci < t.
A compact slice of maths
Notation 2.1. Define [n] = {1, . . . , n} ⊆ N. If R is a ring and X is a formal variable symbol then P ∈ R[X] is a formal sum of powers of X, which we call a polynomial (with coefficients in R). Polynomials can be added and multiplied in the usual way. For example, (1+X)∗(1−X) = 1−X 2 ∈ Z[X]. Notation 2.2. If P, Q ∈ Z[X] then write P (Q) ∈ Z[X] for the result of instantiating X to Q in P . For example if P = X + 1 and Q = 2 ∗ X then P (Q) = 2 ∗ X + 1. Definition 2.3. Fix an index variable symbol X and a set of polynomial function symbols C, D ∈ PolyFunc, each of which has a fixed but arbitrary arity arity(C) ∈ N≥1 . Write C : n for the assertion “C ∈ PolyFunc and arity(C) = n”. Define terms and predicates inductively as in Figure 1. ≤ Ci ≤ t′ for (t−1< < Ci )∧ ∧ (Ci < Notation 2.4. We may write t≤ t′ + 1). We may call predicates based on < range-checks.
Proof. Routine from Figure 2 and Lemma 2.8, noting that: for x, y ∈ Q, (x9y)2 = 0 iff x = y; and for x, y ≥ 0, x + y = 0 iff x=0 ∧ y=0 and x ∗ y = 0 iff x=0 ∨ y=0.
3
Examples
3.1
Three one-line examples
Section 2 takes up one page of dense mathematics and concludes with one Theorem. This is compact and theoretical 1
The Wikipedia page and this overview are excellent and very accessible introductions. 2 The choice of evaluation point 0 is unimportant; we could equivalently use [ ϕ]]ς (1), since for closed ϕ, ∀x, x′ .[[ϕ]]ς (x) = [ ϕ]]ς (x′ ).
Logic
Polynomial
Truth values
0 = true/valid/success; strictly positive = false/invalid/failure. [ t = t′ ] ς = ([[t]]ς − [ t′ ] ς )2 , so equality is valid exactly at zero. [ ϕ ∧ ψ]]ς = [ ϕ]]ς + [ ψ]]ς ; sum of nonnegatives is zero iff both are zero. [ ϕ ∨ ψ]]ς = [ ϕ]]ς ∗ [ ψ]]ς ; product is zero iff at least one factor is zero. 0 when satisfied, 1 otherwise. Root test for a range of values. [ ϕ]]ς = 0 [ ϕ]]ς > 0
Equality Conjunction Disjunction Range check Top-level ∀ ϕ valid ϕ invalid
Figure 3: Table of semantic meaning (Remark 3.2)
much as logic gates are compact and theoretical: by composing together simple components we attain great expressivity, and by suitable implementation we can accomplish remarkable things. We give the reader a taste of how this works. = 0 and false as 0= = 1. Example 3.1. We can express truth as 0= The reader can check that [ 0 = 0]]ς = 0 (thus ⊨ς 0 = 0) and = 1) so these predicates do behave like [ 0 = 1]]ς = 1 (thus ⊭ς 0= ‘true’ and ‘false’. Assume m : 2, a : 3, and p : 1 with validity predicates χm = ∀m X.(m2 (X) = (91) ∗ m1 (X)) χa = ∀a X.(a3 (X) = a1 (X) + a2 (X)) χp = (0 < p1 ). Given an interpretation ς, we have P [ χm ] ς = x∈[len(ς(m))] (itplnt(m2 )(x) − (91) ∗ itplnt(m1 )(x))2 P [ χa ] ς = x∈[len(ς(a))] (itplnt(a3 )(x) − (itplnt(a1 )(x)+itplnt(a2 )(x)))2 [ χp ] ς = 0 if ∀x ∈ [len(ς(p))].ς(p)1,x > 0, and 1 otherwise
So: • ⊨ς χm when ς(m) is a two-row matrix where in each column the second entry is the negation of the first. Thus, each column in ς(m) represents a pair (x, 9x) for some x ∈ Z. arity(m) = 2 because λx.9x has one input and output. • ⊨ς χa when ς(a) is a three-row matrix where in each column the third entry is the sum of the first and the second; thus ς(a) has columns of the form (x, x′ , x+x′ ) and samples the graph of λx, x′ .x+x′ at len(ς(a)) many points. arity(a) = 3 because λx, x′ .x+x′ has two inputs and one output. • ⊨ς χp when ς(p) is a one-row matrix (a vector) of strictly positive numbers. arity(p) = 1 because ‘is strictly positive’ is a predicate on one argument. Remark 3.2. A table of semantic meanings is in Figure 3. The reader may be more used to seeing ‘true = 1; false = 0’, but representing truth with 0 and non-truth with strictly positive values also has pedigree. In a paper from 1943 [Kleene, 1943] on page 51 just after equation 17, Kleene writes “a
representing function π of P , the value of which is to be 0, 1, or undefined according as the value of P is true, false, or undefined”. More recently, in the sysexits.h file (credited to Eric Allman in 1980) which describes status codes for system programs, 0 represents successful termination and strictly positive values represent various kinds of failure. We will consider one more example, because it is an important one. We will indicate that our framework can handle recursion; this is the essence of looping and of Turing-complete computation. The reader will have to excuse that our example will be extremely simple, but it is the structure of the computation that interests us.
3.2
A recursive example
Definition 3.3. Recall the inductive definition of ab for a, b ∈ N≥0 : base case (BC) inductive step (IS)
pow (a, 0) = 1 pow (a, b+1) = a ∗ pow (a, b)
Remark 3.4. Note how Definition 3.3, and definitions like it, implicitly equate computation, inductively-defined relations, and derivation, because pow is a relation, it is inductively defined as above, and when we try to compute a value — pow (2, 2), say — we generate a derivation-tree as follows: pow (2, 0) = 1 pow (2, 1) = 2 pow (2, 2) = 4
base case inductive step inductive step
This example, simple as it is, illustrates the close link between logic, computation, and inductively defined relations. Definition 3.5. Suppose ln ∈ N≥1 . Say a 4 × ln matrix C encodes a partial power function when C
∀a ∈ 1..ln. C3,a = C1,a2,a . In words, C encodes a partial power function when for each column, the third entry is equal to the first entry raised to the power of the second. Definition 3.6. Assume pow : 4, so ς(pow) ∈ Z4×len(ς(pow)) . Figure 4 expresses a validity predicate χpow , that pow encodes a partial power function such that: 1. Row 1 (values of pow1 (a)) stores input values a. 2. Row 2 (values of pow2 (a)) stores input values b. 3. Row 3 (values of pow3 (a)) stores output values ab . 4. Row 4 (values of pow4 (a)) stores the index of a column representing the recursive call in the inductive step. Lemma 3.7. If ⊨ς χpow then ς(pow) encodes a partial power function. Proof. We examine the clauses in Figure 4 and using Theorem 2.9 we check that they correctly encode the definition in Definition 3.3.
Write pow1 (t)=in1 (t), pow2 (t)=in2 (t), pow3 (t)=out(t), and pow4 (t)=rec(t). BC(X) = (in2 (X) = 0) ∧ (out(X) = 1) ∧ IS(X) = in1 (X) = in1 (rec(X)) ∧ in2 (X) = in2 (rec(X))+1∧ out(X) = in1 (X) ∗ out(rec(X)) χpow = 1 ≤ rec ≤ len(pow) ∧ ∀ pow X.(BC(X) ∨ IS(X)) Figure 4: Exponentiation ab (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 0 1 1
2 1 2 1
2 2 4 2
2 2 4 2
2 1 2 3
2 0 1 3
2 0 1 2
2 2 4 3
2 1 2 1
2 0 1 1
3 0 1 1
2 0 1 1
3 1 3 1
2 1 2 2
These all represent the derivation-tree from Remark 3.4: 1. The leftmost matrix encodes in columns 1-3 respectively, the base case of a derivation that 20 = 1, the step 21 = 2, and the final step 22 = 4. Entry 4 in columns 2 and 3 contain a number which is a pointer to the previous step/column in the derivation; entry 4 in column 1 also contains a number but it is not used. 2. The columns need not appear in a particular order, provided that the pointers match up; the next matrix illustrates this by putting the columns in the reverse order. 3. Columns can be duplicated as per the third matrix. 4. The fourth (rightmost) matrix includes information from computing 21 = 2 and 31 = 3. Example 3.9. The converse implication for Lemma 3.7 does not hold. The predicate χpow certifies the pointwise correctness of the input-output samples in rows 1-3 and also that those samples can be assembled into a well-formed derivation tree, whose recursive calls are represented by in-range pointers in row 4. A matrix may encode true values of the partial 2 power function while failing χpow , if the certificate of 2 derivation is missing or malformed. For example, the 4 2 one-column matrix to the right contains the correct input-output sample (2,2,4), since 22 = 4. However, it omits the recursive premise (2,1,2) required by the inductive step. Formally, len(pow) = 1 and the row 4 entry is 2, so the range check 1 ≤ rec ≤ len(pow) fails. Equivalently: the supposed recursive pointer points outside the matrix. A second instructive failure is as per the 2 2 2 three-column matrix to the right. Rows 1-3 2 1 0 contain correct samples: 22 = 4, 21 = 2, and 4 2 1 2 3 0 20 = 1, and the first two recursive pointers are meaningful: column 1 points to column 2, and column 2 points to column 3. However, the underlined pointer in the base-case column is not in the range {1, 2, 3}. The basecase clause (BC) does not use this pointer, but our simple presentation imposes the uniform range check on all entries of the pointer row. Hence this matrix encodes correct samples of the partial power function but is not a well-formed χpow -certificate. Replacing the underlined 0 with any in-range value, for example with 1, would repair this.
In summary: rows 1-3 describe claimed values of the relation; row 4 supplies the proof-carrying structure that allows a verifier to check claims against the inductive definition. Remark 3.10. Example 3.9 connects directly to agent certification. Columns are not isolated output values; they are structured witnesses which reference each other to prove their validity. In an agentic setting this distinction separates a validator that checks whether an action is compliant from one that checks whether an action carries evidence of its compliance (in this case, columns pointing to one another to prove a recursive computation). This is precisely the proof-carrying structure that the certificates of Section 4 would cryptographically attest to. Remark 3.11. A more efficient specification of ab is: pow (a, 0) = 1 pow (a, 2 ∗ b) = pow (a, b) ∗ pow (a, b) pow (a, 2 ∗ b + 1) = a ∗ pow (a, b) ∗ pow (a, b) This yields smaller derivations, which correspond algorithmically to a runtime that is logarithmic in b rather than linear. We could translate this into our logic, and it would just yield an implementation that permits shorter matrices. Remark 3.12. The logic in Figure 1 is more expressive than it might seem. In particular, negation is expressible in the framework, via reify. A fuller treatment is in [Gabbay, 2025]. A proposal for a SNARK-friendly constraint system is in [Gabbay and Mendelsohn, 2026].
4
How to apply this mathematics to AI agents
Before we address the question of how to apply this mathematics to AI agents — the motivating application of this paper, although the framework in Sections 2 and 3 is general — it is important to understand that polynomial semantics can be plugged directly into cryptographic proof schemes. The semantics in Figure 2 is optimised for exposition, but variations optimised for implementation can be constructed.3 Thus it is important to appreciate that the presentation in Section 2 is optimised for fitting onto one page including Figure 2 and Theorem 2.9, consistent with clear exposition. We can optimise for practical implementability instead, but that would be a longer and less accessible presentation: the passage from cleanly presentable theory to applicability is analogous to the passage from a high-level programming language to something more like assembly language or bytecode. Be that as it may, the strategy for applying these ideas is simple: • Write down a predicate that expresses the desired notion of correctness, and translate it (using techniques analogous to program compilation) to an algebraic relation accepted by a cryptographic proof back end. Suitable back ends include integer or mixed-characteristic systems such as Zinc [Garreta et al., 2025] and polynomialcommitment/SNARK stacks such as Halo2 and related foundations [Electric Coin Company and Zcash Foundation, 2026; Boneh et al., 2021]. 3
One such variant has been submitted for publication, but at time of writing, submission rules prohibit sharing the results. By time of publication I hope to be able to provide links.
• Require the agent, or associated prover, to produce a cryptographic certificate accepted by the back end. Under the proof system’s assumptions, and subject to stated soundness error, a valid certificate convinces the verifier that the encoded relation has a witness. If this seems conceptually simple, that is because it is. Though this is a short paper, we can make this more concrete. At the boundary of an agentic system, we can represent a certificate of validity abstractly as Cert = (policyID, action, pub, vk, paramsHash, π). Here policyID identifies the formal predicate ϕ and the compiler version; action is the proposed action; pub is the public instance data needed to check that action; vk and paramsHash identify the approved verifier key and proof-system parameters; and π is the succinct cryptographic proof. The intended statement verified by π is ∃w. Rϕ,action (pub, w) = 0, where w is private witness data and Rϕ,action is the algebraic relation obtained by compiling the formal predicate to polynomial constraints. Thus verification of an action has the following form. 1. The policy author or system operator fixes a predicate ϕ expressing the required correctness, safety, or compliance condition. 2. A compiler translates ϕ, together with the relevant public action data, into an algebraic relation Rϕ,action . 3. The agent, or an associated prover, produces a proof π that there exists witness data w satisfying that relation. 4. The receiving system checks π using the approved verifier key and rejects action if verification fails. We can sum this up as a slogan: logical validity translates to vanishing of the corresponding algebraic relation. In this interface the verifier need not trust the agent, inspect internal implementation, or re-execute computation. It just checks the proof. Conversely, the certificate proves only the compiled formal claim: it does not prove that the policy was wisely chosen, that the compiler is bug-free, or that the proofsystem parameters were correctly governed. A practical compiler would use implementation-oriented arithmetisation techniques; for example multilinear encodings, range checks, and lookup arguments, targeting the back ends mentioned above (Zinc; Halo2). The mathematics of Sections 2 and 3 specifies the correctness condition that such a compiler must preserve. Roadmap. So we can propose a provisional roadmap. If a policy can be logically expressed as a predicate, and if a trusted compilation chain maps that predicate to an algebraic relation while preserving the zero-versus-positive philosophy of Figure 3, then any sound succinct argument for that relation yields a succinct certificate that the policy predicate is satisfied by the supplied witness data. Remaining questions are just what one would expect, moving from mathematics to a deployed assurance mechanism: how to author and audit correctness predicates; how to verify or test the compiler;
how to select and parameterise the proof back end; how to benchmark proving cost; and how to record policy versions and verifier configurations for later accountability.
5
Related work
Formal specification and verification. Formal methods provide mature tools for specifying and proving properties of software and systems. Hoare logic [Hoare, 1969], proofcarrying code [Necula, 1997], verified compilers like CompCert [Leroy, 2009], and verified kernels like seL4 [Klein et al., 2009] can provide machine-checkable assurance for critical systems. Correctness-by-construction makes assurance part of design and implementation [Hall and Chapman, 2002]. These approaches share with our proposal a formally specified notion of ‘correctness’. However, the deployments differ: proof-carrying code is not a black-box technique, whereas our proposal imposes no restrictions on how an agent is designed and implemented, other than insisting that some or all of the actions that it proposes be associated to a succinct certificate proving validity of an agreed correctness predicate. Runtime verification, proof-carrying code, and certificates. Runtime verification checks traces of an executing system against formal properties [Leucker and Schallhart, 2009]. Proof-carrying code asks an untrusted code producer to supply a proof that code satisfies a consumer’s safety policy [Necula, 1997]. Our proposal can be read as a cryptographic, succinct, and optionally zero-knowledge analogue of proof-carrying code: the consumer publishes or fixes a policy; the agent supplies an action and a certificate; and the verifier checks the certificate without re-running the agent’s entire computation or inspecting all private witness data. Succinct cryptographic proofs and verifiable computation. zk-SNARKs and related succinct arguments allow a prover to convince a verifier that a relation holds between a witness and an instance, while keeping verifier effort small and, in zero-knowledge variants, hiding some or all of the witness. Examples include Pinocchio [Parno et al., 2013], SNARKs for C [Ben-Sasson et al., 2013], Groth’s pairingbased arguments [Groth, 2016], and later general frameworks for polynomial IOPs, constraint systems, and related lookup machinery [Ben-Sasson et al., 2016; Bünz et al., 2020; Thaler, 2022; Setty et al., 2023; Setty et al., 2024]. The technical constructions underlying this paper use similar technology; in unpublished work we have shown how to arithmetise the first-order logic of this paper to polynomial constraints on integer/mixed-characteristic proof systems such as Zinc [Garreta et al., 2025], and we are studying how to translate to Halo2 [Electric Coin Company and Zcash Foundation, 2026] so that logical specifications can be connected to cryptographic back ends. zkVMs and proof-oriented execution environments. An engineering response to the difficulty of writing polynomial constraints directly is zero-knowledge virtual machines, like Cairo [Goldberg et al., 2021], RISC0 [RISC Zero, 2026], and Jolt [Arun et al., 2024]. These all offer verifiable receipts of
correct code execution. Work on formally verifying Cairo execution in Lean reflects the importance of connecting cryptographic proof systems to proof-assistant-level assurance [Avigad et al., 2021]. In contrast, the present proposal does not introduce another machine model. Its high-level specification language is first-order logic itself. Programs, policies, transaction rules, and compliance requirements are represented as predicates, which are compiled directly to polynomial proof obligations. Choreographic programming and distributed correctness. Choreographic programming and multiparty session types address distributed correctness from complementary angles. Multiparty session types use global protocol descriptions whose projections type-check communicating processes and establish communication safety, progress, and fidelity [Honda et al., 2016]. Choreographic programming writes a global coordination plan from which decentralised implementations can be generated correct by construction [Cruz-Filipe and Montesi, 2017] (subsequently developed to include functional [Cruz-Filipe et al., 2022] and machine-checked [Cruz-Filipe et al., 2023] formulations). These ideas may be relevant to agentic AI systems. Our proposal does not replace choreographic or protocol-based design, and it deals with the orthogonal problem of how to ensure that possibly Byzantine, possibly black-box agents — i.e. agents which we did not implement and which we may not be able to look inside — should still carry cryptographic certificates of correct behaviour.
6
Conclusions
Formal methods provide the language of formal specification; correctness-by-construction provides a design discipline; runtime verification and proof-carrying code provide certificate-oriented assurance; and zk-SNARKs/zkVMs provide cryptographically checkable execution. This paper articulates a synthesis of these ideas for trustworthy agentic AI: a consequential action may be logged and signed — and also, where feasible, it may be accompanied by a succinct certificate of validity of a formally specified notion of correctness, safety, or compliance. It remains to render these ideas into cryptographically implementable schemes, e.g. by reduction to SNARK-friendly constraint systems. This is ongoing work: a proposal has been very recently presented [Gabbay and Mendelsohn, 2026] and a conference paper submitted. Future work includes generating auditable deployment patterns; e.g. specification templates for common agent actions, benchmarks across proof back ends, recording of policy versions and verifier configurations, and independent cryptographic, formal-methods, and policy review. These are not mere engineering details. A cryptographic certificate proves satisfaction of the encoded formal predicate under the relevant proof-system assumptions and soundness bounds. It does not prove that the correctness predicate itself reflects safety, legal, operational, or ethical requirements. This specification gap must be addressed through governance, visibility, and risk-management processes; it cannot be closed
by mathematics, logic or cryptography alone [Chan et al., 2024; National Institute of Standards and Technology, 2023].
References [Arun et al., 2024] 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. doi:10.1007/978-3-031-58751-1 1. [Avigad et al., 2021] Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, and Alon Titelman. A verified algebraic representation of cairo program execution, 2021. doi:10.48550/arXiv.2109.14534. [Ben-Sasson et al., 2013] 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. doi:10.1007/978-3-642-40084-1 6. [Ben-Sasson et al., 2016] 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. doi:10.1007/978-3-662-53644-5 2. [Boneh et al., 2021] 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. doi: 10.1007/978-3-030-84242-0 23. [Bünz et al., 2020] Benedikt Bü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. doi:10.1007/978-3-030-45721-1 24. [Chan et al., 2024] 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 for Computing Machinery. doi:10. 1145/3630106.3658948. [Cruz-Filipe and Montesi, 2017] Luı́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. doi:10.1007/978-3-319-57666-4 3. [Cruz-Filipe et al., 2022] Luı́s Cruz-Filipe, Eva Graversen, Lovro Lugović, Fabrizio Montesi, and Marco Peressotti. Functional choreographic programming. In Theoretical Aspects of Computing – ICTAC 2022, Lecture Notes in Computer Science. Springer, 2022. doi:10.1007/ 978-3-031-17715-6 15.
[Cruz-Filipe et al., 2023] Luı́s Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. A formal theory of choreographic programming. Journal of Automated Reasoning, 67, 2023. doi:10.1007/s10817-023-09665-3. [Electric Coin Company and Zcash Foundation, 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. [Gabbay and Mendelsohn, 2026] Murdoch J. Gabbay and Andrew Mendelsohn. SNARKs for First Order Logic. Talk presented by Mendelsohn at the Workshop on Cryptographic Tools for Blockchains (CTB 2026, permalink), affiliated with Eurocrypt 2026, Rome, Italy, May 2026. Slides at https://www.ctb-workshop.org/slides/02 SNARKs-for-First-Order-Logic.pdf (permalink). [Gabbay, 2024] 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. [Gabbay, 2025] 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. [Gabriel et al., 2024] Iason Gabriel, Arianna Manzini, Geoff Keeling, Lisa Anne Hendricks, Verena Rieser, Hasan Iqbal, Nenad Tomašev, Ira Ktena, Zachary Kenton, Mikel Rodriguez, et al. The ethics of advanced ai assistants, 2024. doi:10.48550/arXiv.2404.16244. [Garreta et al., 2025] Albert Garreta, Hendrik Waldner, Ilia Vlasov, Katerina Hristova, Luca Dall’Ava, Marko Čupić, 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, 2025. doi:10.1007/978-3-032-01907-3 9. [Goldberg et al., 2021] Lior Goldberg, Shahar Papini, and Michael Riabzev. Cairo – a Turing-complete STARKfriendly CPU architecture. Cryptology ePrint Archive, Paper 2021/1063, 2021. https://eprint.iacr.org/2021/1063. [Groth, 2016] Jens Groth. On the size of pairing-based noninteractive arguments. In Advances in Cryptology – EUROCRYPT 2016, volume 9666 of Lecture Notes in Computer Science, pages 305–326. Springer, 2016. doi:10. 1007/978-3-662-49896-5 11. [Hall and Chapman, 2002] Anthony Hall and Roderick Chapman. Correctness by construction: Developing a commercial secure system. IEEE Software, 19(1):18–25, 2002. doi:10.1109/52.976937. [Hoare, 1969] C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–580, 1969. doi:10.1145/363235.363259. [Honda et al., 2016] Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types.
Journal of the ACM, 63(1):1–67, 2016. doi:10.1145/ 2827695. [Kleene, 1943] Stephen C. Kleene. Recursive predicates and quantifiers. Transactions of the American Mathematical Society, 53:41–73, 1943. doi:10.1090/ S0002-9947-1943-0007371-8. [Klein et al., 2009] 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. doi:10.1145/1629575.1629596. [Leroy, 2009] Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107–115, 2009. doi:10.1145/1538788.1538814. [Leucker and Schallhart, 2009] Martin Leucker and Christian Schallhart. A brief account of runtime verification. The Journal of Logic and Algebraic Programming, 78(5):293–303, 2009. doi:10.1016/j.jlap.2008.08.004. [National Institute of Standards and Technology, 2023] National Institute of Standards and Technology. Artificial intelligence risk management framework (ai rmf 1.0). Technical report, National Institute of Standards and Technology, 2023. doi:10.6028/NIST.AI.100-1. [Necula, 1997] 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. doi:10.1145/263699.263712. [Parno et al., 2013] 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. doi:10.1109/SP.2013. 47. [RISC Zero, 2026] RISC Zero. RISC Zero zkVM Developer Documentation, 2026. Accessed 2026-05-25. https://dev. risczero.com/. [Salgado and Wise, 2022] Abner J. Salgado and Steven M. Wise. Polynomial Interpolation, pages 231–265. Cambridge University Press, 2022. doi:10.1017/ 9781108942607. [Setty et al., 2023] 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. [Setty et al., 2024] 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. doi:10.1007/978-3-031-58751-1 7. [Thaler, 2022] Justin Thaler. Proofs, Arguments, and ZeroKnowledge, volume 4 of Foundations and Trends in Privacy and Security. Now Publishers, 2022. doi:10.1561/ 3300000030.