{
  "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.",
  "abstract_shown": true,
  "affiliations": [],
  "article_type": null,
  "arxiv": null,
  "author_total": 2,
  "authors": [
    {
      "name": "Nurgali Kadyrbek",
      "orcid": "0000-0002-5461-8899"
    },
    {
      "name": "Madina Mansurova"
    }
  ],
  "bibtex": "https://research.draconitic.com/paper/eh16hx9mkmdxq.bib",
  "cited_by": 0,
  "doi": "10.1038/s41598-026-74900-x",
  "fulltext_url": null,
  "id": "eh16hx9mkmdxq",
  "issns": [
    "2045-2322"
  ],
  "landing_url": "https://www.nature.com/articles/s41598-026-74900-x",
  "language": null,
  "licence": "CC-BY-4.0",
  "licence_label": "CC BY 4.0",
  "licence_source": "article",
  "licence_url": "https://creativecommons.org/licenses/by/4.0",
  "metadata_licence": null,
  "native_subjects": [
    [
      "openalex",
      "1702|Logic, programming, and type systems"
    ]
  ],
  "openalex": "W7221658137",
  "pdf_url": "https://www.nature.com/articles/s41598-026-74900-x_reference.pdf",
  "pmcid": null,
  "pmid": null,
  "published": "2026-10-13",
  "publisher": "Springer Science and Business Media LLC",
  "ris": "https://research.draconitic.com/paper/eh16hx9mkmdxq.ris",
  "sources": [
    {
      "first_seen": "2026-10-30T12:17:26Z",
      "native_id": "10.1038/s41598-026-74900-x",
      "source": "crossref",
      "url": "https://www.nature.com/articles/s41598-026-74900-x"
    }
  ],
  "subjects": [],
  "title": "Proof carrying agent actions enable verifiable licensing of language model tool use",
  "title_text": "Proof carrying agent actions enable verifiable licensing of language model tool use",
  "type": "peer-reviewed",
  "updated_at": "2026-10-30T12:17:26Z",
  "url": "https://research.draconitic.com/paper/eh16hx9mkmdxq",
  "venue": "Scientific Reports",
  "versions": []
}