Agenra: A Language and Verified Core for Stateful LLM Agent Authorization

Applications that deploy LLM agents keep revising the permissions their agents use. When authority is consumable, even widening a permission can break a legitimate workflow, because an early call may use up a grant that a later call needs. Checking individual requests, or watching one run succeed, misses this. We present Agenra, a policy language with a Lean enforcement core that tracks the values each call uses, resources discovered at run time, and authority consumed by earlier calls. Agenra treats safety and workflow preservation as separate properties. Our key idea is to certify a revision with a simulation between the old and new permission ledgers. Quota increases, appended grants and independent reorderings admit such simulations by construction, and Lean checks proposed simulations for other finite-quota revisions. The proofs use the deployed matching predicates and extend through the full monitor, covering discovered resources, payloads that are never enumerated, failed calls and approvals. They assume serialized calls and identical service results under both policies, and they trust the Python translation layer. On 51 authored revisions, the checks certify all 21 that preserve their clients and none of the 30 that do not, and every lost workflow is confirmed by replay. They also certify a real quota increase from an open-source agent application. In a report-delivery application, raising the send quota preserves every client yet permits a second approved send, so preservation does not imply safety.