# Provably Auditable and Safe LLM Agents from Human-Authored Ontologies

arXiv: https://arxiv.org/abs/2606.04903 · HTML: https://mlsanity.com/paper/2606.04903/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Agent threats, guardrails and governance, one of 16 directions in LLM agents and tool use.
- Builds on 5 of its 23 references that are in the map.
- First posted on arXiv 3 Jun 2026.

## Placed in

- LLM agents and tool use / [Agent threats, guardrails and governance](https://mlsanity.com/agents/agent-threats-guardrails-and-governance/)

## Builds on (most cited first, 5 of 5)

- [Large Language Models](https://mlsanity.com/paper/2307.05782/) (2023)
- [Ontology Generation using Large Language Models](https://mlsanity.com/paper/2503.05388/) (2025)
- [Do LLMs Really Adapt to Domains? An Ontology Learning Perspective](https://mlsanity.com/paper/2407.19998/) (2024)
- [OntoURL: A Benchmark for Evaluating Large Language Models on Symbolic Ontological Understanding, Reasoning and Learning](https://mlsanity.com/paper/2505.11031/) (2025)
- [Ontology Learning with LLMs: A Benchmark Study on Axiom Identification](https://mlsanity.com/paper/2512.05594/) (2025)

## Abstract (arXiv)

We introduce the LLM agent architecture Agentic Redux, intended for use with nontrivial problem domains that require linear auditability. Using the typed lambda calculus, we prove that, run on appropriate domains, Agentic Redux executions are semantically guaranteed to be correct, with all decisions recorded in an append-only ledger. We present two production-grade appropriate domains, in healthcare billing compliance, and security vulnerability disclosure. Working code for Agentic Redux run on both domains is available in a supporting code repository. We also introduce Ontology-First Agent Design, a methodology for creation of agent frameworks on a problem domain, in which a human expert ontologizes the problem domain with Basic Formal Ontology, and then assigns an LLM to derive roles that agents and humans-in-the-loop can fill, in order to work the problems in the domain.