Propose, Ground, Prove, Attest: Proof-Gated Authorization for Agentic AI

Agentic AI systems place large language models (LLMs) in the path of consequential actions. The dominant safeguardusing one model to judge another via an LLM critic, constitutional grader, or model-scored policy checkleaves a probabilistic component in the authorization path and therefore inherits the very failure mode it is meant to contain. We argue that a guardrail is authoritative only if no language model sits in its decision path, and we separate two kinds of authority that current architectures conate: proposal authority, which an LLM should hold, and decision authority, which must rest on a process that cannot hallucinate. We present a proof-gated architecturepropose, ground, prove, attestin which an LLM pro- poses a candidate action, the proposal is grounded against a formal ontology, a solver (answer set programming via Clingo) derives whether the grounded proposal satises a gate's constraints, and the resulting proofnot the modelauthorizes the action. The prover is a gate's plug- gable reasoner owned by the orchestrator and never by an agent, making the safety invariant structural rather than procedural. In a reference implementation, a categorical gate runs end to end: it materializes named violations as facts so that a refusal carries its reasons, and writes every authorization to an append-only, full-SHA-256 hash-chained attestation ledger that an oine verier re-checks for tampering without re-running any model. A numeric threshold gate is specied through a boolean-in-grounding construction, demonstrated in an earlier prototype and pending re-integration. We map the attestation ledger to the NIST AI Risk Management Framework, measure sub-millisecond gate latency, and report results against a pinned imple- mentation. The motivating domain is regulated healthcare documentation, with the clinical rule sets held out of the artifact. We position the work against neuro-symbolic verication (LLM- Modulo), LLM-plus-ASP reasoning, model-based guardrails, the agentic-AI security literature, and classical access control, and state precisely what is and is not novel.