Proof carrying agent actions enable verifiable licensing of language model tool use
Abstract
LLM agents increasingly call tools and take irreversible actions, yet the reasoning that licenses an action is rarely checked before execution. We present Proof-Carrying Agent Actions (PCAA) : each governed action carries a typed Action Certificate that a planner-independent checker must accept before execution. A trusted execution shim derives the obligation set and the irreversibility classification from an authoritative tool contract and binds the certificate to the exact invocation with a canonical SHA-256 commitment. The checker compares that context with the certificate, re-derives typed support (proof, belief, hypothesis, contingency, conflict, or no-progress), and validates formula-level inference rules. Irreversible actions require Proof for every declared licensing obligation. The checker accepts the two valid certificates and rejects all fifteen unsafe certificates in a semantic battery; four additional structural cases confirm rejection of argument substitution, precondition omission, and risk-flag downgrade. A microbenchmark of a three-obligation payment certificate measures 53.7 μs median and 65.7 μs p95 for construction, checking, serialization, and buffered local persistence. A stateful guardrail with the same certified-state predicate matches PCAA on safety; PCAA’s distinct contribution is a typed, replayable decision artifact. Guarantees are relative to trusted tool contracts: PCAA checks their use, not their real-world semantic correctness.
Related
- The Accountability Axis for Agent Actions: A Verifiable Form (v0.1.0)
- Comparative Evaluation of a System One Model and a General-Purpose Large Language Model on the Korean Physical Therapist Licensing Examination
- Benchmarking large language models on the Ukrainian Krok 2 licensing examination in physical therapy: accuracy, consistency, and agreement
- Answering clinicians' questions over trial evidence tables with verifiable, feedback-driven language models
- From Answers to States: Verifiable Process-Level Evaluation of Chemical Reasoning in Large Language Models
BibTeX
@article{kadyrbek2026proof,
title = {{Proof carrying agent actions enable verifiable licensing of language model tool use}},
author = {Nurgali Kadyrbek and Madina Mansurova},
journal = {Scientific Reports},
year = {2026},
month = oct,
doi = {10.1038/s41598-026-74900-x},
url = {https://www.nature.com/articles/s41598-026-74900-x},
note = {CC BY 4.0},
}
RIS
TY - JOUR
TI - Proof carrying agent actions enable verifiable licensing of language model tool use
AU - Nurgali Kadyrbek
AU - Madina Mansurova
PY - 2026
DA - 2026/10/13
JO - Scientific Reports
DO - 10.1038/s41598-026-74900-x
UR - https://www.nature.com/articles/s41598-026-74900-x
AB - LLM agents increasingly call tools and take irreversible actions, yet the reasoning that licenses an action is rarely checked before execution. We present Proof-Carrying Agent Actions (PCAA) : each governed action carries a typed Action Certificate that a planner-independent checker must accept before execution. A trusted execution shim derives the obligation set and the irreversibility classification from an authoritative tool contract and binds the certificate to the exact invocation with a canonical SHA-256 commitment. The checker compares that context with the certificate, re-derives typed support (proof, belief, hypothesis, contingency, conflict, or no-progress), and validates formula-level inference rules. Irreversible actions require Proof for every declared licensing obligation. The checker accepts the two valid certificates and rejects all fifteen unsafe certificates in a semantic battery; four additional structural cases confirm rejection of argument substitution, precondition omission, and risk-flag downgrade. A microbenchmark of a three-obligation payment certificate measures 53.7 μs median and 65.7 μs p95 for construction, checking, serialization, and buffered local persistence. A stateful guardrail with the same certified-state predicate matches PCAA on safety; PCAA’s distinct contribution is a typed, replayable decision artifact. Guarantees are relative to trusted tool contracts: PCAA checks their use, not their real-world semantic correctness.
SN - 2045-2322
ER -