Technical Summary: Provably Auditable and Safe LLM Agents from Human-Authored Ontologies

1. Problem Statement

Large Language Model (LLM) agents exhibit nondeterministic behavior and hallucinations, posing significant risks in safety-critical domains requiring linear auditability, such as healthcare compliance and financial security. Current approaches to agent safety rely on operational "guardrails" (e.g., swapping agent harnesses or using LLMs as judges) which lack semantic guarantees. Specifically, multi-agent systems often suffer from "Write Skew" anomalies, where agents acting on disjoint local state slices independently propose actions that, when combined, violate global system invariants (e.g., exceeding a budget or violating regulatory constraints). Existing frameworks struggle to provide a mathematical guarantee that global state transitions will always preserve these invariants, regardless of agent behavior or external adversarial inputs.

2. Methodology

2.1 Agentic Redux Architecture

The paper introduces Agentic Redux, an agent architecture inspired by the Redux state management pattern. It separates the system into three layers:

1. Sub-agents: Each agent operates on an isolated "slice" of the global state. Agents propose actions based on their local view, potentially utilizing LLMs or tools. They cannot directly modify global state or observe other agents' slices.
2. Meta-agent: A central adjudicator with full visibility of the global state. It receives proposals from sub-agents and evaluates them against a set of declared invariants (rules that must always be true about the global state).
3. Commit Discipline: The meta-agent is the sole entity permitted to change the global state. It only commits a state transition if the resulting state preserves all invariants. If a proposal violates an invariant, it is rejected or escalated.

2.2 Ontology-First Agent Design

To apply Agentic Redux to specific domains, the authors propose a methodology called Ontology-First Agent Design:

1. Ontologization: A human expert constructs a "lower ontology" of the problem domain using the Basic Formal Ontology (BFO). This defines independent continuants (e.g., Patients, Vulnerabilities), processes, and roles.
2. Role Derivation: An LLM is tasked with analyzing the ontology to derive agent roles. This involves grouping processes with overlapping state footprints and assigning them to roles. The goal is fine-grained roles that adhere to the Principle of Least Privilege (PoLP), ensuring agents only see the state necessary for their specific tasks.
3. Invariant Derivation: An LLM extracts system invariants from the ontology, classifying them as local (enforceable by a single agent's slice) or cross-cutting (requiring the meta-agent's global view).
4. Domain Module Construction: The ontology and derived roles/invariants are converted into a typed Domain Module, which is then executed on the Agentic Redux kernel.

2.3 Formal Verification

The paper utilizes typed lambda calculus to formally model the Agentic Redux architecture. The system is defined as an "Architecture Functor" that takes a Domain Module as input. The authors prove that for any well-typed execution:

• Invariant Preservation: If the initial state satisfies the invariants, every reachable state in any execution (including those with nondeterministic LLM outputs or adversarial scheduling) preserves those invariants.
• Agent Confinement: Agents are mathematically restricted to observing and affecting only their assigned state slices.
• Linear Auditability: The system maintains an append-only ledger where every decision (approval, rejection, or escalation) is recorded with a proof of why the decision was made.

3. Key Contributions

• Agentic Redux Architecture: A novel agent framework that provides a semantic guarantee of safety by enforcing invariant preservation through a centralized meta-agent, effectively eliminating Write Skew anomalies.
• Formal Proofs: The first application of typed lambda calculus to prove that LLM agent executions are semantically guaranteed to be correct (invariant-preserving) and linearly auditable, even when sub-agents are buggy, malicious, or hallucinating.
• Ontology-First Agent Design: A methodology for semi-automatically deriving agent frameworks from human-authored ontologies, leveraging LLMs for role and invariant extraction while keeping the critical ontology construction in human hands.
• Counselor Queue Extension: A mechanism to handle edge cases where human intervention is required. The system allows a human "Counselor" to override decisions, but the system formally tracks these overrides in the audit log, distinguishing between "Safe Counselor Commits" (preserving invariants) and policy violations.
• Production-Grade Case Studies: The authors demonstrate the architecture in two distinct domains:
  1. Healthcare Billing Compliance (UDT): Ensuring Urine Drug Test billing adheres to complex, time-dependent regulations (e.g., abstinence tiers) where independent billing and clinical agents could otherwise cause coverage errors.
  2. Security Vulnerability Disclosure: Managing the disclosure pipeline for software vulnerabilities, ensuring coordination between patch development, embargo enforcement, and CVE attribution without leaking sensitive information between concurrent disclosures.

4. Results

• Theoretical Guarantees: The paper presents Theorem 1 (Invariant Preservation), proving that Agentic Redux executions never reach a state violating declared invariants, provided the initial state is valid. Theorem 2 (Audit Log Integrity) proves that the system generates a linear, append-only log of all decisions with full provenance. Corollary 1 establishes that Write Skew executions are structurally impossible under this architecture.
• Implementation: Working code for the Agentic Redux kernel and the two domain examples (UDT Compliance and Security Vulnerability Disclosure) is provided in a supporting repository. The code demonstrates the auto-derivation of agents from BFO ontologies.
• Comparison to Existing Patterns: The architecture is shown to be isomorphic to the "Risk Agents" framework used by CashApp, suggesting that Agentic Redux captures a "natural" architectural pattern for complex, regulated workflows.

5. Significance and Claims

The paper claims that Agentic Redux shifts the burden of safety from operational runtime monitoring to architectural design. By using type-theoretic properties, the architecture ensures that "bad behaviors can never happen" at the semantic level, regardless of the unpredictability of the LLMs acting as sub-agents.

The authors emphasize that this approach allows engineers to build systems where the "harness" (the safety mechanism) does not need to be swapped out as LLMs evolve, because the safety is guaranteed by the architecture's type system, not the specific model's output. The methodology of Ontology-First Agent Design is presented as a scalable way to translate human domain expertise into provably safe agent frameworks, focusing human effort on the ontology (the "truth") and leveraging LLMs for the mechanical derivation of roles and code.

The paper explicitly scopes its claims to safety (preventing bad things) and auditability, noting that liveness (ensuring good things eventually happen) and complexity metrics are addressed in future work. It acknowledges that while the architecture prevents invariant violations, it does not prevent the system from behaving poorly if the invariants themselves are poorly specified; thus, the quality of the human-authored ontology remains the critical factor.