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.