Paper deep dive
Provably Auditable and Safe LLM Agents from Human-Authored Ontologies
Aaron Sterling
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 94%
Last extracted: 7/9/2026, 1:35:07 AM
Summary
The paper introduces Agentic Redux, an LLM agent architecture designed for domains requiring linear auditability and semantic safety guarantees. By leveraging typed lambda calculus, the architecture mathematically proves that agent executions preserve system invariants, preventing failures like Write Skew. It employs a meta-agent to adjudicate proposals from sub-agents against an append-only ledger. The authors propose Ontology-First Agent Design, a methodology where human experts use Basic Formal Ontology (BFO) to model problem domains, and LLMs derive agent roles and domain modules. Production-grade implementations are demonstrated in healthcare billing compliance and security vulnerability disclosure, with a near-isomorphic architecture found in CashApp's Risk Agents framework.
Entities (11)
Relation Signals (8)
Ontology-First Agent Design → utilizes → Basic Formal Ontology
confidence 97% · human expert ontologizes the problem domain with Basic Formal Ontology
Agentic Redux → provides → Linear Auditability
confidence 96% · intended for use with nontrivial problem domains that require linear auditability
Agentic Redux → uses → Typed Lambda Calculus
confidence 95% · Using the typed lambda calculus, we prove that, run on appropriate domains, Agentic Redux executions are semantically guaranteed to be correct
Meta-Agent → adjudicates → Sub-agents
confidence 94% · the meta-agent adjudicates all proposals from local agents
Agentic Redux → prevents → Write Skew
confidence 92% · To prevent Write Skew (and other bad behaviors), the agent architecture must preserve invariants when the global state transitions
Human-in-the-Loop → supervises → Agentic Redux
confidence 91% · All theorems in this paper about pure Agentic Redux can be modified to cover Agentic Redux with Counselor Queue, where the Counselor is a human with authority over the system
Risk Agents → isnearisomorphicto → Agentic Redux
confidence 90% · Agentic Redux appears near-isomorphic to the Risk Agents framework, which was independently created by engineers at CashApp
LLMs → →
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract: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.
Tags
Links
- Source: https://arxiv.org/abs/2606.04903v1
- Canonical: https://arxiv.org/abs/2606.04903v1
PDF not stored locally. Use the link above to view on the source site.
Full Text
177,596 characters extracted from source content.
Expand or collapse full text
Provably Auditable and Safe LLM Agents from Human-Authored Ontologies †thanks: A supporting repository with code for the Agentic Redux kernel and all Problem Domain examples can be found at https://github.com/Thistleseeds/agentic-redux Aaron Sterling Thistleseeds asterling@thistleseeds.com Abstract 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. 1 Introduction 1.1 Semantic Verification of Safety LLMs hallucinate. Even when they respond correctly, they behave nondeterministically. In safety-priority domains that require linear auditability, like finance or healthcare compliance, agent behavior can be hard to manage. Currently, engineers manage the safety of agent behavior operationally. For example, Anthropic’s Managed Agents [11] make it easy to swap out a stale agent harness for an up-to-date harness. The primary goal of this paper is to show that, for some problem domains, using the correct agent architecture means you never have to swap out the harness, ever. The type-theoretic properties of the architecture provide a semantic guarantee of safety. Programming language theory, and the typed lambda calculus, provide a sophisticated toolbox to prove that bad behaviors can never happen. That said, while the theorems in this paper prove that our executions of interest are always correct, real world software is buggy. I recommend that builders follow a defense-in-depth approach of wrapping each agent in a governance layer (such as the layer provided by Microsoft Agent Framework[22]) that watches for exactly the behavior the type system prevents. While Managed Agents provides a runtime substrate, and Microsoft Agent Framework provides guardrails, this paper focuses on a third layer: agent architecture, the rules about what types of agents can exist, what each agent can see and do, how agents communicate with one another, and how state changes happen. To see why agent architecture matters, let’s consider a naive approach. Define the Microservices Architecture as the architecture where each agent behaves independently of all other agents, and all agents write to a shared log. A two-agent system for which the Microservices Architecture fails is the following. The system has a budget of $100,000. Agent A can either do nothing or spend $45,000. Agent B can either do nothing or spend $60,000. Each agent sees only its local state. Since, in the Microservices Architecture, both agents act independently of each other, it is within the rules for both agents to spend money simultaneously, which causes the system to exceed its $100,000 budget. (Berenson et al.[7] termed this kind of failing execution a Write Skew.) If, instead, the two agent system were running an architecture in which Agents A and B could propose actions to a meta-agent, and the meta-agent with view of the global state would adjudicate the proposals, then the meta-agent could ensure that the system would never exceed the budget. Robust microservices architectures mitigate Write Skew with error-reduction patterns (e.g., sagas). Similarly, current agent frameworks are managing problems like Write Skew either by trivializing inter-agent coordination to sidestep the problem; or by gatekeeping state changes in ways that they hope will work, such as asking an LLM whether the state change is OK, then following the LLM’s recomendation, with no consequence if the recommendation is incorrect. The second approach is the “LLM as Judge” pattern of [17]. Those approaches are used by all the multi-agent apps in awesome-llm-apps[25], a public Github repository with over 100,000 stars. A stronger approach would be to employ architecture with a mathematical guarantee that any change to the global state preserves “nice properties.” The rule (nice property), “The system can spend at most $100,000,” is an invariant of the system: it is a statement that must be always true about the global state. To prevent Write Skew (and other bad behaviors), the agent architecture must preserve invariants when the global state transitions. That preservation of invariants can be shown to be a semantic guarantee of a correctly-typed architecture, ensuring the agent framework complies with, e.g., regulatory requirements that must always be true. Real-world agent frameworks almost always deploy with a human-in-the-loop mechanism for a person in charge to act as supervisor or problem-solver. All theorems in this paper about pure Agentic Redux can be modified to cover Agentic Redux with Counselor Queue, where the Counselor is a human with authority over the system. In particular, both preservation of invariants and linear auditability still hold. For more on this topic, see section 4.2. 1.2 Threat Model (What is Safety) For purposes of this paper, I scope the notion of safety as follows. In scope: domain modules may contain bugs or misspecifications, agents may produce arbitrary proposals (whether from LLM hallucination, tool error, prompt injection, or deliberate adversarial construction); and, in the proof machinery, the oracle ω may supply arbitrary scheduling and response sequences. Theorem 1 guarantees that, regardless of these failures, invariants are always preserved. Theorem 2 guarantees that every decision is recorded faithfully, so the system can be linearly audited at any time. Out of scope: if an invariant is poorly specified, and does not support a real-world policy, the system will enforce it, but misbehave with respect to real-world application. While humans in the loop can make any policy decision, including commits that violate invariants, their decisions must be formatted in a way that obeys the system’s type contracts. Confidentiality of the audit log itself is not in scope. Some decisions in Security Vulnerability Disclosure depend on external signals, like assignment of an ID number to a CVE; recording those signals faithfully is the responsibility of the agent harness, which is not in scope. This paper focuses on safety requirements (bad things don’t happen); I consider liveness requirements (good things eventually happen) in [26]. 1.3 Agentic Redux 1.3.1 Agentic Redux Architecture This paper introduces the agent architecture Agentic Redux. It is inspired by the front-end application state manager Redux[1], created by Dan Abramov. Abramov wanted to ensure that the most recent, fresh state was always the state displayed to the user. Imagine you have the same web page open in two browser tabs. You click a check box in one tab, then switch to the other tab. Does the second tab display the checked box, or does it still display the stale state with the box unchecked? The Redux solution to this problem is to make all components presentation-only, and to centralize all state changes through a single decisonmaker that can see the global state of the app. A popular Redux saying is, “Smart container, dumb components.” In Agentic Redux, each agent sees only their local slice of the global state, and computes their own evaluation function based on that local state. The evaluation could be simple and synchronous, or complex and asynchronous, invoking LLMs or other tools. If an agent wants to change its local slice of state (the analogue to displaying a checked box because the user clicked an unchecked box), it proposes that change to a meta-agent. The meta-agent adjudicates all proposals from local agents. The meta-agent’s adjuducation function is written to preserve desired invariants of the global state. The meta-agent can see the global state, and is the only entity in the system with the power to change the global state. If the meta-agent changes the global state, it then sends each agent their local slice of the new global state. Agents propose; the meta-agent decides and directs. See fig. 1 for a diagram. Figure 1: The Agentic Redux architecture. Sub-agents receive isolated state slices and propose actions to a meta-agent, which adjudicates proposals against declared invariants before committing state transitions. Code is available at https://github.com/Thistleseeds/agentic-redux 1.3.2 Linear Auditability The meta-agent keeps a log. Each time the meta-agent declines a proposal from one of the subagents, the meta-agent records the denial, and why it denied the proposal (which invariant would not have been preserved if it had accepted the proposal). Each time the meta-agent accepts a proposal and changes the global state, it logs the new global state and proof that all invariants are preserved. This log provides an audit trail, ordered linearly in time, so every decision of the system can be reviewed by an external auditor. Linear auditability benefits from other properties Agentic Redux provides: the log is a ledger, meaning no data is ever removed, and writing is append-only; only the meta-agent writes to the log, and only when deciding whether to change the global state; every decision by the meta-agent about whether to change the global state produces exactly one log entry. The formal proof of all these benefits is discussed in section 4.1. Later in the paper, we will see architectures that allow either the meta-agent or a human-in-the-loop to write to the log. 1.3.3 Agentic Redux May Be a “Natural” Architecture I created Agentic Redux to handle issues I was running into when designing software for healthcare billing compliance. To provide evidence that Agentic Redux may be a “natural” agentic architecture, with application to a variety of problem domains, Agentic Redux appears near-isomorphic to the Risk Agents framework[10], which was independently created by engineers at CashApp. While CashApp created Risk Agents to solve problems in financial compliance, I stumbled across Risk Agents when reading minutes of a working group meeting that was discussing how to apply Risk Agents to automated social media moderation. For reasons of space, I will defer discussion of social media moderation until future work. However, the supporting code repository for this paper contains the full ontology and code examples for social media User Case Management, a problem domain that benefits from Agentic Redux (and from Risk Agents). The ontology is derived in part from Osprey[24], an open-source social media moderation tool connected to that working group. 1.4 Methodology 1.4.1 Domains and Functors To study the architecture separately from the problem it is helping to solve, I use a Programming Language Theory technique of separating a working system into three pieces: a Domain Module, an Architecture Functor, and a Client Program. The composition of the Domain Module and the Architecture Functor can be thought of as a module making a call to an operating system kernel. In the case of Agentic Redux, a domain provides invariants, the initial state, the meta-agent’s adjudication function, and the evaluate-and-propose functions run by the local agents. The meta-agent’s adjudication function is a synchronous checklist of invariants to preserve in all global state changes, with the subagent functions can be either synchronous or asynchronous. A local agent, using its own slice of state, may consult an LLM (or any other tool) before deciding whether to propose an action. The Agentic Redux kernel then runs the system, with the guardrail that, whenever global state might change, that change is allowed only if all invariants are preserved. The Client Program handles everything else: sandbox, session liveness, harness, test scenarios, governance. These features are important, but they are out of scope for this paper. I will assume that all Client Program features are available and work. I define the properties of the Architecture Functor with the typed lambda calculus[23], a formalization of programming language pseudocode. The typed lambda calculus is well-studied, and its literature contains deep theorems. Section 4 shows how to prove that Agentic Redux is semantically guaranteed to preserve system invariants. 1.4.2 Computational Ontology While a Domain Module is code that captures information about an area of interest, I will use Problem Domain to refer to a real-world problem space that humans are trying to reason about. I consider two Problem Domains in this paper: health care compliance, and security vulnerability disclosure. These domains sound different from each another (and they are!), but they share common underlying structure. Significantly, they both admit Write Skew executions if run on the Microservices Architecture, and they both avoid Write Skew executions if run on Agentic Redux. I move from Problem Domain to Domain Module by performing an intermediate step: construction of an ontology. While ontology dates back to the Greeks, the study of computational ontology began in the 1970s as part of early AI research[16]. There are now many computational ontologies available, to provide machine-understandable structure to music, anatomy, and other disciplines. My ontology of choice is the Basic Formal Ontology (BFO)[12], because it was created to ontologize complex processes, including organic processes, like disease progression in medicine. BFO is an “upper ontology,” meaning that it provides an abstract template for categories and relations that have been shown to be robust over time. A subject matter expert starts with BFO and constructs a “lower ontology,” which is a structural description of a concrete Problem Domain that follows the rules of BFO. If you are a subject matter expert interested in ontologizing your domain of expertise, I recommend the excellent book [3], which is now open access. 1.4.3 Ontology-First Agent Design The methodology I adopted (which may be of interest independent of Agentic Redux) I have termed Ontology-First Agent Design. The methodology is: (1) ontologize a Problem Domain using BFO; (2) ask an LLM to assess the ontology for domain fingerprints of interest; (3) if the domain has a fingerprint that Agentic Redux can help with, ask the LLM to convert the ontology into a Domain Module, i.e., into code; (4) run the Domain Module on Agentic Redux and observe the results, clarifying the ontology as needed. See fig. 2 for a diagram. Figure 2: Ontology-First Agent Design. The ontologies referenced in this paper were produced by this method. Ontology files are available at https://github.com/Thistleseeds/agentic-redux A domain fingerprint is an attribute of the Problem Domain that informs what is required to solve problems in that domain. The fingerprint, “All execution is seqential in a pipeline,” makes Write Skew impossible, and is evidence that a simple architecture like the Microservices Architecture might be enough solve problems in that domain. A fingerprint implying Write Skew indicates that a more sophisticated architecture is needed. All Problem Domains considered in this paper imply Write Skew, and also have an Auditability Fingerprint: the system must be able to report on every action the system performed, ordered linearly in time. A Problem Domain with both Write Skew and Auditability fingerprints may be a strong candidate to benefit from Agentic Redux. (A Problem Domain with just the Auditability fingerprint might be best run on a simple pipeline, if there are no nontrivial agent interactions.) While I chose the two Problem Domains considered in this paper because they are structurally similar, I ontologized each individually, and their ontologies are not a reskin. Including the User Case Management ontology in the discussion for a moment, both the security vulnerability and social media moderation domains contained a timed governance relationship that the health care compliance domain did not; and a relationship present in both health care compliance and security vulnerabiity disclosure was absent in social media moderation. Please consider this part of the paper a presentation of a case study of Ontology-First Agent Design. Between this paper and its upcoming parts, I have successfully used ontologies to auto-derive agents for systems with seven different problem domains and three different agent architectures (not just Agentic Redux). It’s a small sample size, but robust enough that I think it’s likely someone else could benefit from it too. 1.4.4 Human vs. LLM Ontology Creation It is worth pausing for a moment to review ontology creation by humans and by LLMs, because there is empirical data that might look contradictory at first glance, but, in fact, paints a unifying picture. LLMs are not as good as humans at ontology creation (sometimes called “ontology learning”), as shown in [4, 15, 6]. However, at least according to the OntoURL benchmarks, LLMs are better than humans at reasoning over an ontology that already exists[29]. Despite the previous results, the quality of LLM-generated ontologies can be higher than the quality of ontologies created by novice human engineers[19]. This is not a contradiction, because an LLM’s ability to 1-shot ontology creation is directly related to how completely humans already ontologized the space through documentation. The need for humans to pre-ontologize the space can be seen in [21], which presented LLMs with well-structured gibberish, and the LLMs were unable to ontologize the gibberish, showing an inability to reason over semantic relations between concepts. One goal of Ontology-First Agent Design is to focus human expert input where it is most needed: creation of the ontology (at the start), and refinements to the ontology to improve the system’s functionality (a feedback loop at the end). The LLM does the work in the middle, where it is most effective. 2 From Ontology to Agents 2.1 Basic Formal Ontology I will present just enough BFO to show how to define agents and system invariants, so Agentic Redux can run on those agents to preserve the invariants. The most important BFO definitions for our purposes are independent continuant, process and role. An independent continuant is a thing with its own relations and qualities. In the two ontologies considered in this paper, both have one primary independent continuant: a patient, or a security vulnerability. The Security Vulnerability Ontology also has a secondary independent continuant, which only plays a peripheral role as an occasional source of signals. A process is something that happens to an independent continuant, unfolding over time. In the Security Vulnerability Disclosure ontology, there are twelve processes, including: DevelopPatch, ReviewPatch, ReleaseFix, ExecuteDisclosure. Note the centrality of the independent continuant (the vulnerability) to each process: the vulnerability has a patch developed for it, the fix for the vulnerability is released, until finally the vulnerability is disclosed. A role is an externally grounded, optional, property of an independent continuant. “John is an employee at ACME Corporation,” is an example of a role. John, an independent continuant, holds the role relative to an independent continuant external to himself, and John would continue being John if he were no longer employed there. We can extend the original ontology by introducing workers: new independent continuants that bear “employment” roles grounded in the processes of the original ontology. In the examples we consider in this paper, these derived “employment roles” or “worker roles” are separate from, and in addition to, any roles that may have existed in the original ontology. A technical note: I strongly recommend you upload the pdf of BFO 2.0[13] to your LLM’s knowledge base, instead of the BFO ISO standard[14] in OWL or OWL DL. The OWL DL spec is the more useful format for tools like automated reasoners, but it lacks the lexical context that LLMs need when helping to create ontologies, as already discussed in section 1.4.4. 2.2 Derivation of Agent Roles Given an ontology of a problem domain, the roles we add to that ontology are the employment opportunities available to work on problems in the domain. Those roles are then filled either by agents, or by humans in the loop. Each role comes with a job description (which processes to perform) and a security clearance (which slice of the global state is available). I will now present a procedure (displayed visually in fig. 3) for determining which roles to create in order to extend a problem domain’s ontology. This is most of the work required to perform Step 3 (Convert Ontology to Domain Module) of Ontology-First Agent Design. As shown in the color coding of fig. 2, this is a procedure LLMs can perform well, in my experience. Procedure 1 (Role Derivation). List all processes in the ontology. For each process, list everything the process needs to read or write; call that list the process’s state footprint. Group processes whose state footprints substantially overlap. For each group of processes, define a role whose state footprint is the union of the group’s footprints. Verify that no role touches state that its processes do not need; if that check fails, redo the previous step to define more fine-grained roles. The preference for fine-grained roles in the Role Derivation procedure is an architectural best practice, not a logical requirement. Just one agent could perform all roles, and that would avoid any Write Skew executions, but it would come with all the drawbacks of monolithic architecture. Fine-grained roles reduce the blast radius of a faulty LLM step, and provide agent confinement, a type-level analogue to the Principle of Least Privilege (PoLP). PoLP is an access control property that is enforced by a governance layer to ensure a worker has access only to the resources needed to perform its work. Agent confinement, a generalization to agents of the classic Confinement Problem[18], restricts both what an agent can observe and what an agent can directly modify: an agent sees only the minimal slice of state needed to perform its work, and cannot directly modify state at all, since all state changes are mediated by the meta-agent. Figure 3: Role Derivation procedure. 2.3 Derivation of System Invariants Once we have roles and slices of state that we can assign to workers, we need to determine the system invariants that we want the Agentic Redux meta-agent to enforce. As with the Role Derivation procedure, I have found that LLMs are good at this step. See fig. 4 for a diagram. Invariants come from the problem domain, not from the architecture. The architecture’s job is to enforce invariants; the ontology’s job is to declare them. BFO provides two natural sources of invariants: policy rules and process preconditions. Procedure 2 (Invariant Derivation). Step 1: List all policy rules. Identify every information content entity (ICE) in the ontology that represents a policy rule. Each such ICE contributes at least one invariant. List the state components each constraint references; call that list the invariant’s state footprint. Step 2: Extract process preconditions. For every process in the ontology, list the preconditions that must hold before the process can occur. Each statement of type, “Process P cannot occur unless these preconditions hold,” is an invariant. The invariant’s state footprint includes the state written by any prerequisite process, and the state read by the gated process. If you have an LLM derive the invariants, one human verifcation method would be to walk the life cycle of the ontology’s independent continuant. At every state transition, check that the conjunction of declared invariants is sufficient to prevent any transition the domain should prohibit. If a transition is possible that the domain expert considers invalid but no invariant blocks, add the missing invariant as either a policy rule or a process prerequisite, then rerun the procedure. Once you have listed all system invariants, classify them as either local or cross-cutting. A local invariant is an invariant whose state footprint is entirely contained within the state footprint of a worker. A cross-cutting invariant is an invariant whose state footprint intersects with the state footprints of at least two workers. (A globally shared resource, like the $100,000 budget in the system in the Introduction, is an example of a cross-cutting invariant.) A local invariant can be enforced by the local worker whose state footprint contains it. It is the meta-agent’s responsibility, in Agentic Redux, to enforce that the cross-cutting invariants are preserved. Figure 4: Deriving invariants, then assigning the cross-cutting invariants to the Agentic Redux meta-agent. 2.4 Summary We’ve walked through how to derive worker roles and system invariants from a domain ontology. (The ontologies available in the supporting code repository are BFO ontologies of problem domains, extended with roles and workers.) In the ontologies considered in this paper, one worker is a human in the loop, while the rest of the workers are agents. In other problem domains, perhaps it would make sense for all the workers to be agents. The Agentic Redux meta-agent enforces preservation of a system invariant if that invariant affects the state footprint of at least two workers. Now let’s turn to the problem domains to see concrete examples. 3 Motivating Problem Domains 3.1 UDT Compliance I created Agentic Redux to ensure compliance with billing requirements of Arizona’s AHCCCS Program[27]. These requirements can be difficult to parse, which can lead to service providers, or individuals with few resources, being denied reimbursement for services they thought were covered. In particular, when a Urine Drug Test (UDT) is, or is not, covered, can be confusing. My goal, when defining the UDT Compliance problem domain, was to be able to inform people with 100% accuracy whether their UDT would be covered by AHCCCS. This required coordination between billing and lab ordering, which led me to the construction of a meta-agent that could see both billing and lab ordering states. There are two types of UDTs: a presumptive test, and a definitive test. A presumptive test uses immunoassay methods, and provides general results like, “Opioids detected.” A definitive test uses a more specialized, more expensive method, to detect specific drugs, and can provide results like, “Fentanyl at xyz concentration detected.” The AHCCCS regulations prohibit an immunoassay test from being used to confirm a presumptive test; a definitive test is required to confirm the results of a presumptive test. At the same time, the number of UDTs AHCCCS will cover in a week is dependent on an individual’s abstinence tier, which is based on the number of days since the individual’s last positive test. Someone with an abstinence tier of 90+ days, is eligible for three definitive tests in a 90-day period. Someone with an abstinence tier of 0-30 days, is eligible for one definitive test every 7 days. Putting everything together, we can see a billing pitfall that is structurally identical to a Write Skew execution. A patient, call him David, is in the 90+ day abstinence tier. He takes a definitive test on March 23rd, which is negative. Then, on March 26th, he takes a presumptive test, which detects opioids. The service provider then orders a definitive test, also on March 26th, because of the results of presumptive test. However, this definitive test will not be covered, because it is the second definitive test in a 7-day period, and David’s abstinence tier just reset to 0-30 days, which only allows one definitive test in a 7-day period. If the biller is working with the now-stale state that David’s abstinence tier is 90+ days, the new definitive test appears covered, since it is the second test in a 90-day period. In order to evaluate coverage correctly, the biller needs current information from the lab-order team, and from the clinical team that tracks abstinence tiers. Therefore, if we agentify the workflow, with a LabOrder agent, a Billing agent, and a Clinical agent, we also need a meta-agent that can see the global state in order to make a final decision. See table 1 for a list of agents and their slices of state, in this agentified workflow. Agentic Redux as presented in section 1.3 is not sufficient to model UDT Compliance. Both medical best practices and AHCCCS regulations mandate that the clinical response to a patient’s relapse be a human decision point. Therefore, the original Agentic Redux presented in fig. 1 is augmented with a Counselor Queue, that allows for a human in the loop, as shown in fig. 5. The ontology of the UDT Compliance problem domain is available in the supporting code repository, as is fully working code for a UDT Compliance domain module, and Agentic Redux augmented with a Counselor Queue. The independent continuant of the UDT Compliance ontology is the Patient. The roles are as shown in table 1: LabOrder, Billing, and Clinical. Table 1: Sub-agent roles in the UDT compliance domain. Role Agent Visible State Slice LabOrder Lab Order Agent Clinical rationale Billing Billing Agent Claim history Clinical Clinical Analysis Agent Abstinence tier tracking Figure 5: Agentic Redux expanded with a Counselor Queue for the UDT Compliance probem domain. 3.2 Security Vulnerability Disclosure The Security Vulnerability Disclosure ontology is motivated by a bottleneck I first heard described by Carlini in a video of a talk he gave at the [un]prompted security conference[9], since explained in detail by Lynch[20], and supported by an announcement from Anthropic Red[8]. The Anthropic Red announcement is particularly interesting for this paper, because it shows that Anthropic Red has already converged on a methodology that is Agentic-Redux shaped. The Anthropic Red methodology is less formal than Agentic Redux, and, at least to my mind, would benefit from typed architecture that is correct by construction. This section of the paper is my response to a call Carlini made at the end of his talk, when he asked for assistance to get through the upcoming security crisis. As with the UDT Compliance ontology, fully-tested source code for running the Security Vulnerabiity Disclosure domain module on the Agentic Redux kernel is available in the supporting code repository. 3.2.1 Security Vulnerability Disclosure Ontology Following the method of Ontology-First Agent Design, I ontologized the Security Vulnerability Disclosure problem domain, and then directed an LLM to derive roles that LLM agents and a human-in-the-loop would fill. The scope of the problem domain was from just after the validation of a vulnerability to its eventual disclosure to the organization owning the component containing the vulnerability. While the UDT Compliance ontology has one independent continuant, the Patient, the Security Vulnerability Disclosure ontology has two independent continuants: the Vulnerability, and the Receiving Organization. The Vulnerability is the primary entity that participates in the disclosure adjudication pipeline; it is analogous to the Patient in the UDT Compliance ontology. The Receiving Organization has no UDT Compliance analogue. For purposes of this ontology (and this paper), it is primarily a source of signals that processes in the disclosure adjudication pipeline wait for before proceeding. If one were to ontologize the work to be done from disclosure to resolution, the Receiving Organization would play a larger role. Security Vulnerability Disclosure is a more complex problem domain than UDT Compliance, as can be seen from the larger number of relations a Vulnerability can have with Qualities and with Information Content Entities, see fig. 6. The differences are also visible if you compare the happy path of the independent continuant’s journey through each ontology, as shown in fig. 7. Despite the differences, the Agentic Redux architectures auto-derived from the two ontologies are almost isomorphic. (See fig. 5 for the UDT Compliance architecture, and fig. 8 for the Security Vulnerability Disclosure architecture.) The only difference is that there are three proposing subagents in UDT Compliance, and four proposing subagents in Security Vulnerability Disclosure. This is because the adjudication pipeline in both problem domains is essentially identical: specalized team members with incomplete information propose actions to a decider with full knowledge of the global state. Agentic Redux formalizes this shape to give it a semantic guarantee of safety. An interesting feature of Security Vulnerability Disclosure is that, according to published reports, Anthropic Red is already using an Agentic-Redux-shaped one-agent architecture to assist with the adjudication pipeline. Claude is positioned as both proposer and decider: “I suggest this new action and here’s why,” “Ok, let me decide based on everything else going on.” This situation may allow Agentic Redux to offer complexity-theoretic advantages (speedup), not just safety. Let’s discuss complexity theory now. Figure 6: The independent continuant Vulnerability and its relations, in the Security Vulnerability Disclosure ontology. Figure 7: A comparison between the happy paths of the independent continuant’s journey in the UDT Compliance ontology and the Security Vulnerability Disclosure ontology. Figure 8: The Agentic Redux architecture for the Security Vulnerability Disclosure ontology. 3.2.2 Checkability Over Correctness While the intuition that it is easier to verify than it is to create has been part of computer science since at least the P/NP Problem, I believe Checkability Over Correctness was coined by Allan as a design principle of the programming language Vera[2]. Applied to the context of Agentic Redux, the asymmetry between the potential complexity of subagents and the simplicity of the meta-agent is good design. The subagents have the hard job of proposing the correct next step for the global state. This might involve LLM calls, tool calls, and the handling of ambiguity. The meta-agent, by contrast, runs a simple check against a list of must-haves (the invariants). If everything on the list checks green (all invariants are preserved), the meta-agent transitions the global state. Otherwise, the meta-agent denies the proposal to transition. While Agentic Redux ensures safety for every adjudicable problem domain, in the case of Security Vulnerability Disclosure, the simplicity of the meta-agent may also provide speedup. Instead of the current reported Anthropic process, in which an LLM is on both sides of the decision function (as both proposer and decider), under Agentic Redux, only the proposer is slow to act. This time savings may add up when managing multiple vulnerabilities in the same co-disclosure group, and potentially thousands of vulnerabilities overall. For reasons of space, I defer machinery for liveness and complexity until [26]. Before leaving the topic, though, it’s worth discussing an ontological difference between Security Vulnerability Verification and Security Vulnerability Disclosure. I also ontologized Security Vulnerability Verification, the phase immediately before Security Vulnerability Disclosure, in which a security finding is evaluated to determine whether it is a genuine vulnerability. (I don’t include that ontology in this paper, but it’s available in the supporting code repository.) The Agentic Redux architecture for Security Vulnerability Verification is literally isomorphic to that of Security Vulnerability Disclosure—same diagram, different labels. Yet, while Agentic Redux would provide a guarantee of safety to Security Vulnerability Verification, it may not provide speedup. This is due to the ontological features of the human-in-the-loop queue that make vulnerability verification different from either UDT Compliance or Security Vulnerability Disclosure. In both UDT Compliance and Security Vulnerability Disclosure, the human-in-the-loop queue is an exception handler. On a happy path, the agents may do all the work and never need human intervention. With Security Vulnerability Verification, on the other hand, the verifier is a human, so the happy path always includes the human-in-the-loop, and the human expert is responsible for performing the verification. For vulnerability verification, checkability is hard, so it seems difficult to gain speedup by leveraging Checkability Over Correctness. 3.2.3 Security Agents and Invariants In the UDT Compliance ontology, all invariants were dependent only on internal information. In the Security Vulnerability Disclosure ontology, some invariants depend on internal information, while others depend on both internal and external information. The external information arrives in the form of observed signals from the Receiving Organization, that the disclosing organization records as data of the global state. MAINTAINER_RATE_LIMIT is an example of an invariant of the first type. It’s an internal limit to prevent the overburdening of a software maintainer. The meta-agent checks the current number of disclosures against an internal cap, and denies the disclosure if the cap would be exceeded. CVE_ATTRIBUTION_CONSISTENCY is an example of an invariant of the second type. The system observes and records an external signal, assigning a ID number to a CVE. The meta-agent then enforces that any proposal referring to that CVE must use the externally-assigned ID number for that CVE. The full list of invariants appears in table 2. The subagents are very similar to the subagents of UDT Compliance. Each works on, and makes proposals about, its own disjoint slice of state. For example, the Patch Tracking Agent updates patch information based on observations made about the behavior of the Receiving Organization. The Patch Tracking Agent’s slice of state is limited to a single vulnerability, so disclosure information cannot leak to other potential Receiving Organizations. For a description of all four agents, see table 3. Table 2: Domain invariants derived from the Security Vulnerability Disclosure ontology, grouped by the provenance of the state they read. The first group adjudicates against state populated entirely by the discovering organization’s sub-agent actions; the second additionally reads recorded state populated by observation of external facts (CVE identifiers assigned by an external numbering authority, receiving-organization patch releases, public-knowledge transitions). Both groups are state predicates evaluated at the adjudication instant. Invariant Requirement Adjudicable from discovering-organization state alone. MAINTAINER_RATE_LIMIT No more than N reports to the same subsystem maintainer (within the same receiving organization) within a configured sliding window. The count aggregates across the portfolio and protects receiving-organization capacity. COMMITMENT_REGISTRY_CONSISTENCY The commitment registry is well-formed at every adjudication point: every published commitment hash corresponds to exactly one (artifact, vulnerability) pair; every resolution proposal targets an existing committed hash; and no resolution proposal targets a hash already resolved. The eventual-resolution obligation is deferred to Paper 2. DISCLOSURE_TIMELINE_CONSISTENCY When vulnerabilities are co-disclosed (members of the same CoDisclosureGroup), they must be at compatible disclosure phases at the planned joint disclosure timestamp. A disclosure-execution proposal for a group member is valid only if every other member is also at EMBARGOED (with disclosure preconditions met) or already DISCLOSED for the same group. RECEIVING_ORG_CONFINEMENT When the discovering organization is coordinating disclosure with multiple receiving organizations concurrently for distinct vulnerabilities, the patch-tracking role’s slice for vulnerability A in receiving organization X must not contain details for vulnerability B in receiving organization Y. State slices for concurrent disclosures with disjoint receiving organizations must themselves be disjoint. Adjudicable from recorded state, including observed external facts. EMBARGO_ENFORCEMENT Vulnerability details cannot be publicly disclosed before the later of (a) the maintainer’s patch being released, or (b) the embargo deadline elapsing. The specific embargo regime is configured via EmbargoSpec. Bypassed only when PublicKnowledgeStatus is publicly-known. PATCH_BEFORE_DISCLOSURE A vulnerability cannot be disclosed until a robust fix has been developed and released, except for vulnerabilities whose PublicKnowledgeStatus is publicly-known (fix released immediately upon availability) or whose embargo deadline has elapsed without a fix. CVE_ATTRIBUTION_CONSISTENCY If a CVE identifier is assigned, the disclosure record must reference the same identifier; if a CVE record already exists from intra-organizational deduplication, the disclosure must use that identifier rather than requesting a new one. CVE_ATTRIBUTION_UNIQUENESS Across the portfolio, each CVE identifier binds to exactly one vulnerability. No two distinct vulnerabilities share the same CVE attribution. DISCLOSURE_COMPLETENESS The disclosure record at publication time must include (a) a link to the released patch (or a statement of why the patch is unavailable for public-knowledge or embargo-elapsed cases), (b) all resolved commitment hashes for the vulnerability, (c) the assigned CVE identifier if one exists, and (d) attribution. Agent Work Reporter Coordination Agent Submits validated vulnerability reports to receiving organizations, records acknowledgment receipts, and proposes embargo extensions. Operates over the outbound submission queue and per-(receiving-org, maintainer) rate-limit status without portfolio-wide visibility. Patch Tracking Agent Updates the recorded PatchRecord status from externally-observable receiving-side signals (commits, release notes, advisories) for the assigned vulnerability and proposes severity revisions originating from the receiving organization. Slice is confined to one vulnerability so concurrent disclosures cannot leak across receiving organizations. Commitment Management Agent Publishes cryptographic commitment hashes for held artifacts (report, PoC, writeup) and proposes their resolution at disclosure time. Sees only the assigned vulnerability’s hashes; the meta-agent checks registry-wide uniqueness and resolution targeting. Disclosure Agent Proposes co-disclosure groupings, asserts disclosure readiness, and executes public disclosure once the meta-agent clears the embargo, patch, completeness, CVE-attribution, and timeline-consistency invariants. Holds group-peer visibility to form proposals while leaving timeline adjudication centralized. Table 3: Subagents derived from the BFO-grounded security vulnerability disclosure ontology, one per Role(Agent) entry. 4 Overview of Formal Proofs 4.1 Proofs About Agentic Redux Intuitively, a proof that Agentic Redux always preserves invariants might be: As shown in fig. 1, global state cannot change unless the meta-agent changes it, and the meta-agent will only commit to a new global state if that new state preserves invariants. While straightforward, it takes a fair amount of machinery to prove formally. I have deferred the formal work to Appendix appendix A, and I will discuss key points here. To reason clearly about nondeterministic executions, the proofs use a standard technique of converting nondeterministic executions into deterministic executions that receive information from an oracle ω. You can think of ω as a possibly infinite sequence of data that contains each LLM response and tool use response, in order, received by the agents in a now-deterministic execution. The theorem formalizing, “Agentic Redux always preserves invariants,” is as follows. Theorem 1 (Invariant Preservation). For every D:AdjudicableD: Adjudicable, every client program e0e_0 well-typed over (D) AgenticRedux(D), every initial framework state s0s_0 of type D FState_D with s0.⊧Ds_0. domain invariants_D, and every oracle trace ω∈Ωω∈ : every reachable domain state in (e0,s0,ω) Exec(e_0,s_0,ω) satisfies D invariants_D. The theorem statement informally translates to, “For every domain module with the Auditability Fingerprint, if the initial state of the system preserves invariants, then every global state reachable through any nondeterministic execution of an Agentic Redux system preserves invariants.” This theorem provides the semantic safety promised in the Introduction of the paper. The proof of Theorem 1 appears in section A.2.1. The guarantee of Theorem 1 is stronger than the Redux slogan, “Smart container, dumb components.” Even if the domain is buggy or malicious, the meta-agent of Agentic Redux ensures invariants are preserved. As long as the invariants capture real-world policies, the rest of the components can be evil, not just dumb. With the Invariant Preservation theorem, we can now formalize two claims we have been making informally. The first is Agent Information Confinement: agents, at all steps of an execution, can only see, and only affect, their assigned slice of state. That is formalized as Proposition 1, and proved in section A.2.2. The second claim is: Write Skew executions cannot occur under Agentic Redux. A Write Skew execution produces a global state that violates invariant preservation, which, by Theorem 1, Agentic Redux does not permit. This argument is formalized as Corollary 1 in section A.2.3. Other than preservation of invariants, the most important property we need from Agentic Redux is linear auditability. We obtain a formal proof that Agentic Redux is linearly auditable from Theorem 2 (Audit Log Integrity). The theorem statement refers to several technical definitions, so I defer both the theorem statement and its proof to section A.2.4. Informally, the Audit Log Integrity theorem asserts, “If the system changes state, the action that caused the change is logged with the tag APPROVED; if a proposed state change is declined, either by REJECT or ESCALATE, the decision and the reason for the decision are both logged. The log grows by exactly one entry per adjudication, from no other computation step, and entries are never modified once written.” The final proof about Agentic Redux in the Appendix is Theorem 3 (Type Safety), stated and proved in section A.2.5. We don’t need Type Safety for any results in this paper. However, Type Safety demonstrates that the Agentic Redux Calculus is well-behaved from the perspective of a programming language theorist. It is also a property I intend to build on when considering other agent architectures in future work. 4.2 Extending Proofs to the Counselor Queue The domain examples of section 3 include a Counselor Queue: a mechanism by which an escalated proposal is resolved by a human in the loop (fig. 5). When the meta-agent encounters an invariant failure whose domain-declared outcome is escalate, the proposal is deposited into a review queue to await a counselor’s decision. For purposes of a formal proof about all executions, the counselor has full policy authority. The counselor, i.e., the supervising human in the loop, can change the global state in a way that violates invariants. This may cause the system to behave badly, and it’s the harness’s job to clean things up, which is critically important in real life, but out of the scope of this paper. Please note: the counselor has policy authority, but is type-theoretically constrained. The counselor cannot “do anything,” but must write a decision to the log, using the same consistent format as the meta-agent. The main difference is that the counselor can violate invariants, while the meta-agent cannot. To use the language of distributed systems, counselor decisions are not Byzantine failures. The proof machinery assumes that, once the meta-agent has escalated a decision to the counselor, all activity stops until the counselor makes a decision, to guarantee that the counselor decides with respect to the current global state. That is a strong requirement, but it accurately models the real-world behavior of the problem domains considered in this paper. In UDT Compliance, if the supervising MD needs to make a clinical decision, everyone waits for the decision, then responds accordingly. Similarly, if a decision about a security vulnerability escalates to a human expert, work on that vulnerability report pauses until the expert makes a decision. Let’s call a state change directed by the counselor a Safe Counselor Commit if the state change preserves all invariants. After defining additional machinery (for example, now two writers can write to the log, not just one), it’s possible to show by induction that the system preserves invariants and maintains audit integrity, if every counselor commit is a Safe Counselor Commit. Intuitively, if all invariants hold at time step 0, each commit of the meta-agent or the counselor preserves invariants, and each decision by the meta-agent or the counselor is appended to the log, then every state of the system must preserve invariants, and the log is linearly auditable, as before. Formal proofs of Counselor Queue extensions of theorems for Invariant Preservation, Audit Log Integrity, and Type Safety appear in sections A.3.2 and A.3.3. 5 Conclusion and Future Work This paper has focused on safety properties to support problem domains that require linear auditability. It introduced the LLM agent architecture Agentic Redux, which contains a meta-agent that enforces that every state change must respect global invariants, i.e., respect safety properties. It also presented a procedure to semi-automatically design agents that solve a problem of interest, in which a human expert ontologizes the problem domain, then uses an LLM to derive agents that perform the roles needed to solve problems in that domain. The followup paper[26] will consider liveness properties, and will introduce complexity measures to compare how different coding agent strategies perform on coding tasks. The goal is to develop a framework with which it is possible to compare different programs run on the same agent architecture, and the same program run on different agent architectures. Acknowledgments I am grateful to my Thistleseeds cofounder Yuri Downing for raising the funds that made this research possible; and to Soma Chaudhuri, who taught me how to reason about distributed systems. References [1] D. Abramov (2015–2026) Redux: a JS library for predictable and maintainable global state management. External Links: Link Cited by: §1.3.1. [2] A. Allan (2026) Vera: a language designed for machines to write. External Links: Link Cited by: §3.2.2. [3] R. Arp, B. Smith, and A. D. Spear (2015) Building ontologies with basic formal ontology. MIT Press. External Links: Document Cited by: §1.4.2. [4] H. Babaei Giglou, J. D’Souza, N. Mihindukulasooriya, and S. Auer (2025-Oct.) LLMs4OL 2025 overview: the 2nd large language models for ontology learning challenge. Open Conference Proceedings 6. External Links: Link, Document Cited by: §1.4.4. [5] P. Bailis, A. Fekete, M. J. Franklin, A. Ghodsi, J. M. Hellerstein, and I. Stoica (2014) Coordination avoidance in database systems. In Proceedings of the VLDB Endowment, External Links: Document Cited by: §A.1.2. [6] R. M. Bakker, D. L. D. Scala, M. H. T. de Boer, and S. A. Raaijmakers (2025) Ontology learning with LLMs: a benchmark study on axiom identification. External Links: 2512.05594, Link Cited by: §1.4.4. [7] H. Berenson, P. Bernstein, J. Gray, J. Melton, E. O’Neil, and P. O’Neil (1995-05) A critique of ANSI SQL isolation levels. SIGMOD Rec. 24 (2), p. 1–10. External Links: ISSN 0163-5808, Link, Document Cited by: Remark A.36, §A.2.3, §1.1. [8] N. Carlini, K. Lucas, E. B. Asher, N. Cheng, H. Lakhani, D. Forsythe, and K. Guru (2026) Evaluating and mitigating the growing risk of LLM-discovered 0-days. Anthropic Red. External Links: Link Cited by: §3.2. [9] N. Carlini (2026) Blackhat LLMs. [un]prompted. External Links: Link Cited by: §3.2. [10] CashApp/Block (2026) Risk agents. Note: Minutes of meeting of ROOST Coop working group External Links: Link Cited by: §1.3.3. [11] A. Engineering (2026) Scaling managed agents: decoupling the brain from the hands. Anthropic Engineering. External Links: Link Cited by: §1.1. [12] B. S. et al. (2002–2026) Basic Formal Ontology. External Links: Link Cited by: §1.4.2. [13] B. S. et al. (2020) Basic Formal Ontology 2.0. Note: Direct link to pdf External Links: Link Cited by: §2.1. [14] B. S. et al. (2021) Basic Formal Ontology ISO standard. Note: 2021 External Links: Link Cited by: §2.1. [15] N. Fathallah, S. Staab, and A. Algergawy (2024) LLMs4Life: large language models for ontology learning in life sciences. External Links: 2412.02035, Link Cited by: §1.4.4. [16] T. Gruber (2009) Ontology. Encyclopedia of Database Systems. External Links: Document Cited by: §1.4.2. [17] V. Lakshmanan and H. Hapke (2025-10) Generative AI design patterns. O’Reilly Media, Sebastopol, CA. External Links: ISBN 9798341622654, Link Cited by: §1.1. [18] B. W. Lampson (1973-10) A note on the confinement problem. Commun. ACM 16 (10), p. 613–615. External Links: ISSN 0001-0782, Link, Document Cited by: §2.2. [19] A. S. Lippolis, M. J. Saeedizade, R. Keskisärkkä, S. Zuppiroli, M. Ceriani, A. Gangemi, E. Blomqvist, and A. G. Nuzzolese (2025) Ontology generation using large language models. In The Semantic Web: 22nd European Semantic Web Conference, ESWC 2025, Portoroz, Slovenia, June 1–5, 2025, Proceedings, Part I, Berlin, Heidelberg, p. 321–341. External Links: ISBN 978-3-031-94574-8, Link, Document Cited by: §1.4.4. [20] M. Lynch (2026) Claude code found a linux vulnerability hidden for 23 years. External Links: Link Cited by: §3.2. [21] H. T. Mai, C. X. Chu, and H. Paulheim (2025) Do LLMs really adapt to domains? an ontology learning perspective. In The Semantic Web – ISWC 2024, G. Demartini, K. Hose, M. Acosta, M. Palmonari, G. Cheng, H. Skaf-Molli, N. Ferranti, D. Hernández, and A. Hogan (Eds.), Cham, p. 126–143. External Links: ISBN 978-3-031-77844-5, Document Cited by: §1.4.4. [22] Microsoft (2026) Microsoft agent framework. External Links: Link Cited by: Remark A.24, §1.1. [23] B. C. Pierce (2002) Types and programming languages. MIT Press. External Links: Link Cited by: §A.1.14, §A.1.14, §A.2.5, §1.4.1. [24] ROOST (2026) Osprey. External Links: Link Cited by: §1.3.3. [25] S. Saboo (2026) Awesome LLM apps. External Links: Link Cited by: §1.1. [26] A. Sterling (2026) Different coding agent strategies are better at different jobs. Note: In preparation Cited by: §A.2.5, §1.2, §3.2.2, §5. [27] A. H. C. C. C. System (2025) AHCCCS covered behavioral health services guide. External Links: Link Cited by: §3.1. [28] A. K. Wright and M. Felleisen (1994) A syntactic approach to type soundness. Information and Computation 115 (1), p. 38–94. External Links: Document Cited by: §A.2.5. [29] X. Zhang, H. Lai, Q. Meng, and J. Bos (2025) OntoURL: a benchmark for evaluating large language models on symbolic ontological understanding, reasoning and learning. External Links: 2505.11031, Link Cited by: §1.4.4. Appendix A The Agentic Redux Calculus Note about the proofs in this Appendix: The text in the main body of the paper is 99% text I wrote myself. The text in the Appendix, though, is about 10% mine and 90% LLM-generated. I’l have more to say about the methodology soon. For purposes of this paper: the prompts I provided were extensive, and the process was iterative, not a one-shot. I caught errors in earlier versions of some proofs, but the ones here now look good to me. I believe that these are the first LLM-enabled proofs of program correctness written in the typed lambda calculus. Perhaps this approach can eventually become a form of agentic self-verification. A.1 Preliminaries We introduce the typed lambda calculus in which Agentic Redux is defined as an architecture functor. Following the three-entity structure of section 1.4.1, a running system is obtained by composing three pieces: a domain module providing a conforming domain signature, the Agentic Redux architecture functor consuming that signature, and a client program that instantiates the composition and sequences its operations. This section fixes the calculus-level vocabulary in which each of these pieces is expressed and in which the theorems of section A.2 are stated. The Role Derivation and Invariant Derivation procedures of section 2 are the inputs to the formalisation; in particular, the notion of a state footprint introduced there becomes a first-class object in the calculus. This section fixes the vocabulary needed to state the five theorems of section A.2, one proposition, and one corollary. No theorem is proved here. A.1.1 State Signatures and Footprints Procedure 1 treats a state footprint as “a list of state components a process reads or writes.” We make this precise by fixing, per domain, a finite set of atomic state components. Definition A.1 (State signature). A state signature for a domain D is a pair ΣD=(D,τD) _D=( Fields_D, _D) where: • D Fields_D is a finite set of field names, one per BFO-atomic state component declared by the ontology (a quality of the independent continuant, a role binding, an information content entity bound to the continuant, etc.); • τD:D→ _D: Fields_D→ Type assigns a type to each field name. The state type of D is the dependent record type D≜∏f∈DτD(f). State_D\; \; _f∈ Fields_D _D(f). We write s.fs.f for the component of s:Ds: State_D at field f. Remark A.2 (Atomicity). The granularity of D Fields_D is set by the ontology, not by the representation chosen in code. In the UDT compliance domain, the BFO ontology distinguishes the determinable consecutiveDays from the derived determinable tier, so both appear as separate elements of UDT Fields_UDT even though in code they are siblings under an abstinence record. Record-level groupings in the implementation are an encoding convenience; the state signature is flat. Definition A.3 (Footprint). A footprint in D is a subset F⊆DF Fields_D. The restriction of s:Ds: State_D to F is the sub-record s↾F≜(s.f)f∈F:∏f∈FτD(f).s\! \!F\; \;(s.f)_f∈ F\;:\; _f∈ F _D(f). Footprints form a lattice under subset ordering, with union and intersection; both operations are used in procedures 1 and 2. A.1.2 Derived Footprints: Processes, Roles, Invariants procedures 1 and 2 assign footprints to processes, roles, and invariants. We lift those assignments into the calculus. Remark A.4 (Whose roles?). BFO treats roles uniformly as qualities borne by independent continuants. In the ontologies of section 2, roles appear in two places: • Roles of the domain’s independent continuant. The Vulnerability bears a PipelinePhase role with values ranging over DISCOVERED, TRIAGED, …, DISCLOSED; the Patient bears a ProgramPhase role. These are qualities of the continuant that evolve as it moves through its lifecycle. Formally, they live in D Fields_D as ordinary state fields, typically with an enumerated type. They do not mandate the existence of an agent. • Roles of workers. Procedure 1 introduces workers — new independent continuants bearing roles such as StaticAnalysisRole, LabOrderRole, TriageRole. These roles come with footprints and process assignments; they are filled by agents or by humans in the loop; they are the subject of Agent Confinement. In this section, D Roles_D refers to the second kind only: the worker roles produced by Procedure 1. A reference to a pipeline-phase-type field in an invariant footprint (e.g., “Disclosure requires PipelinePhase = EMBARGOED”) is a reference to a D Fields_D element, not to a D Roles_D element. Definition A.5 (Process footprint). For each process p declared in the ontology, (p)⊆D footprint(p) Fields_D is the footprint specified by Procedure 1: every field read or written during p. Definition A.6 (Agent role and role footprint). An agent role (or worker role) r∈Dr∈ Roles_D is a label drawn from a finite set fixed by the domain, together with an assignment r↦(r)r procs(r) of a set of processes to r. The role footprint is (r)≜⋃p∈(r)(p). footprint(r)\; \; _p∈ procs(r) footprint(p). In the remainder of this section and in all subsequent theorems, “role” without qualification refers to an agent role in this sense (cf. Remark A.1.2). Definition A.7 (Slice). The slice for role r is the restricted record type D(r)≜∏f∈(r)τD(f), Slice_D(r)\; \; _f∈ footprint(r) _D(f), and the projection function is D(s,r)≜s↾(r) project_D(s,r) s\! \! footprint(r). Definition A.8 (Well-formed role assignment). A domain D has a well-formed role assignment iff for every role r and every field f∈(r)f∈ footprint(r) there exists a process p∈(r)p∈ procs(r) with f∈(p)f∈ footprint(p). Well-formedness formalises the final check of Procedure 1 (“no role touches state its processes do not need”). All theorems in section A.2 assume the role assignment is well-formed. Definition A.9 (Invariant footprint). Let D invariants_D be the ordered list of invariants declared by Procedure 2. For each invariant ι∈D ∈ invariants_D, (ι)⊆D footprint( ) Fields_D is the footprint declared in that procedure: the fields ι references. Definition A.10 (Local and cross-cutting invariants). An invariant ι is local to role r iff (ι)⊆(r) footprint( ) footprint(r). It is cross-cutting iff (ι)⊈(r) footprint( ) footprint(r) for every r∈Dr∈ Roles_D. This matches the classification of section 2.3: an invariant is cross-cutting precisely when no single role’s slice suffices to evaluate it. Definition A.11 (Coordination-requiring invariant set). The invariant set D invariants_D is coordination-requiring iff there exist a state s∈Ds∈ State_D with s⊧Ds invariants_D, actions a1,a2∈Da_1,a_2∈ Action_D, and timestamps t1,t2∈t_1,t_2∈ Time such that D(s,ai,ti)⊧D applyMutation_D(s,a_i,t_i) invariants_D for i∈1,2i∈\1,2\, yet applying a1a_1 and a2a_2 independently from s can yield a state violating some ι∈D ∈ invariants_D. A coordination-requiring invariant set is the footprint-based counterpart of the failure of I-confluence in the sense of Bailis et al. [5]: no coordination-free execution of agents producing a1a_1 and a2a_2 from disjoint slices can be guaranteed to preserve D invariants_D. The Write Skew example of the Introduction is the canonical witness: the budget invariant is coordination-requiring because independent $45,000 and $60,000 proposals both preserve it from the initial state yet their composition violates it. A domain whose invariant set is coordination-requiring needs an architecture that provides coordination; Agentic Redux is one such architecture. A.1.3 Domain Signatures The architecture functor consumes a weak domain signature (Adjudicable); the stronger signature ( DOMAIN) carries the role structure needed to state Agent Confinement. Definition A.12 (Three-valued invariant result). An invariant returns a value in the sum type ≜+()+() InvResult\; \;\ pass\\;+\; reject( String)\;+\; escalate( String) signalling, respectively, that the proposed action is compatible with the invariant; that it violates the invariant, with an accompanying diagnostic message; or that it requires human review before commit, with an accompanying explanation. We write (m) reject(m) and (m) escalate(m) for the payload-carrying values. Definition A.13 (Signature Adjudicable). A structure D satisfies Adjudicable iff it provides: • a state signature ΣD=(D,τD) _D=( Fields_D, _D); • a type D: Action_D: Occ of proposable actions; • an ordered list of invariants D=[ι1,…,ιn] invariants_D=[ _1,…, _n] with each ιi _i equipped with: – an identifier id(ιi)∈id( _i)∈ InvariantId, distinct across the list, – a footprint (ιi)⊆D footprint( _i) Fields_D, – a predicate ιi:D→ _i: State_D→ InvResult; • a total pure function D:D×D×→D applyMutation_D: State_D× Action_D× Time→ State_D. Remark A.14 (Invariants as state predicates). The predicate ιi _i takes only a domain state; it has no dependence on the action whose proposal triggered evaluation, nor on any pre-state separate from the one it is checking, nor on the oracle trace: the predicate is fully determined by its state argument, as declared by the signature D→ State_D→ InvResult. Invariants are fixed by the domain module at time 0, before any oracle is consulted, and the meta-agent cannot approve a state that violates them regardless of what oracle string its decision function reads. This is the central semantic choice of the architecture: the meta-agent alone bears responsibility for preservation of D invariants_D, and in particular does not delegate that responsibility to the domain’s D applyMutation_D function. A mutation that produces a state violating some ιi _i — whether through a bug, a misspecification, or adversarial input — is rejected by the post-check before any commit is performed. See Definition A.1.12 for the commit discipline that realises this. Definition A.15 (Signature DOMAIN). A structure D satisfies DOMAIN iff it satisfies Adjudicable and, in addition, provides: • a finite set of agent roles D Roles_D — exactly the worker roles produced by Procedure 1, not the BFO roles of the domain’s independent continuant (cf. Remark A.1.2); • a process assignment :D→℘(D) procs: Roles_D→ ( Procs_D), inducing a footprint (r) footprint(r) for each role; • a projection function D:D×(r:D)→D(r) project_D: State_D×(r: Roles_D)→ Slice_D(r) with D(s,r)=s↾(r) project_D(s,r)=s\! \! footprint(r); subject to the well-formed role assignment condition (Definition A.1.2). Remark A.16 (The footprint determines the slice). Under DOMAIN, the slice type D(r) Slice_D(r) is not a free parameter; it is computed from (r) footprint(r), which is in turn computed from (r) procs(r). A reviewer can audit “is this role seeing only what it should?” by reading the role’s process assignment and comparing against the footprint definition. This is the formal content of Procedure 1. A.1.4 Invariant Satisfaction Definition A.17 (Invariant satisfaction). A state s:Ds: State_D satisfies the invariant pipeline of D, written s⊧Ds invariants_D, iff for every invariant ι∈D ∈ invariants_D, ι(s)= (s)= pass. The sequential, short-circuited evaluation of the kernel’s pipeline is captured by the commit discipline (Definition A.1.12) rather than by ⊧ . The relation ⊧ records the model condition; the first-non- pass ordering records which invariant witnessed a failure. Definition A.18 (Failure witness). If s⊧̸Ds invariants_D, the failure witness is the first invariant ιk _k in list order for which ιk(s)≠ _k(s)≠ pass. The failure witness determines whether the outcome is rejected or escalated. Remark A.19 (Phase gating in lieu of action filtering). An invariant with an opinion only in certain domain-state shapes is expressed by having its predicate early-return pass outside those shapes. A typical pattern reads a phase-valued field from D Fields_D and returns pass unless that field takes a specified value. This is a domain-authoring convention, not a kernel concept: the kernel runs every invariant on every candidate, and phase-gated predicates become no-ops in irrelevant phases. Any scoping that might otherwise have been expressed as “this invariant applies only to these action types” is recast as “this invariant has an opinion only in these state shapes.” A.1.5 Oracles and Arbitration Agents and the meta-agent may consult external computations (LLMs, calculators, lookup tables, human counsellors at a queue) whose responses are not determined by the domain state. The client program may also schedule agents in different orders when their proposals arrive simultaneously in real time. We absorb all such non-determinism into a single oracle trace consulted by the execution. Definition A.20 (Oracle trace). Fix an abstract countable alphabet O of oracle responses. An oracle trace is a finite or infinite sequence ω∈∗∪ω ^* ^ω. The space of oracle traces is denoted Ω . A configuration that consumes an oracle advances through ω one element per consultation. Oracle consultations include: LLM inference outputs, random-number outputs, counsellor-queue decisions, wall-clock timestamps, and the arbitration order in which the coordination protocol elicits proposals from agents. Nothing in ω is a function of the domain state; any such dependency enters an agent via its slice or the meta-agent via its state input. A.1.6 Agents Definition A.21 (Agent). Let D:D: DOMAIN and r∈Dr∈ Roles_D. An agent for role r over D is a computable partial function αr:D(r)×Ω⇀D(r) _r\;:\; Slice_D(r)× Action_D(r) satisfying: 1. Typed output. When αr(σ,ω) _r(σ,ω) is defined, its value is an action classified as belonging to role r (i.e. tagged with r in whatever discipline the domain uses). 2. Slice-only state dependence. The function takes no other inputs that depend on D State_D; in particular, αr _r does not receive state from outside (r) footprint(r) and does not observe the slices of other agents. 3. Oracle determinism. For fixed σ and ω, αr(σ,ω) _r(σ,ω) is deterministic. The space of agents for role r is written D(r) Agent_D(r). Remark A.22 (Realisations). Condition 2 constrains the interface, not the implementation. An agent function may be realised by a classical algorithm, by an LLM consulted with prompts constructed from σ, by a composition of pure tool calls over σ, or by a human typing decisions at a terminal. In each realisation, the LLM response, tool output, or human decision appears as an element consumed from ω. Synchronous and asynchronous implementations are equally admissible; asynchronicity is an operational detail invisible at the calculus level. A shared-oracle semantics is used throughout (one ω per execution, consulted by all agents and the meta-agent); a per-role reformulation with projections ω↾rω\! \!r is equivalent. Remark A.23 (No peer-to-peer communication). The type of αr _r has no channel for messages from other agents. The calculus has no primitive permitting Agent A to observe Agent B’s slice, to receive B’s proposal, or to await B’s completion. The only indirect flow of information from B to A is through the meta-agent: if B’s proposal is committed and the commit touches a field in (A)∩(B) footprint(A)∩ footprint(B), then A’s next invocation will see the new value in its slice. This is mediated by the store, not by a message channel. The hub-and-spoke topology of fig. 1 is therefore not merely stipulated but enforced by the agent type. Remark A.24 (Tools as pure functions of the slice). A tool invoked by an agent that read a field f∉(r)f∉ footprint(r) would inject state outside the slice into αr _r’s output, violating Condition 2. At the calculus level this is ruled out structurally: a well-typed αr _r can only construct queries from σ and consume responses from ω. A governance layer such as Microsoft Agent Framework [22] provides operational enforcement of the same discipline at runtime. A.1.7 The Meta-Agent Definition A.25 (Meta-agent). Let D:AdjudicableD: Adjudicable. A meta-agent for D is a computable partial function μD:D×D×Ω⇀D, _D\;:\; State_D× Action_D× Time× Outcome_D, where D≜(D)++(D) Outcome_D Approval( State_D)+ Rejection+ Escalation( PendingProposal_D). The meta-agent has full state access and is the only component permitted to produce an approved-tagged outcome. The meta-agent’s function is supplied by the architecture, not by the domain. Agentic Redux fixes μD _D to be the concrete adjudication function defined in section A.1.10. A different architecture (e.g., an LLM-judged adjudicator) may supply a different μD _D with the same type. Remark A.26 (The meta-agent as a serialisation point). The meta-agent is the architecture’s serialisation point in the sense of classical concurrency control: the component through which all state-changing proposals pass in a well-defined order. Alternative architectures may instantiate the serialisation point differently — for example, by admitting a bounded window of speculative parallel proposals that are validated against a snapshot, or by layering partition-local serialisation points beneath a global one. Such variants are beyond the scope of this paper; we note only that the architecture signature of section A.1.11 is rich enough to accommodate them. A.1.8 Agent Population Definition A.27 (Agent population). An agent population over D:D: DOMAIN is a family Π=(αr)r∈D,αr∈D(r) \;=\;( _r)_r∈ Roles_D, _r∈ Agent_D(r) containing exactly one agent per role. The “given agents A, B, C” template is made precise by fixing Π=(αA,αB,αC) =( _A, _B, _C). An architecture for these agents is the data of section A.1.11. A.1.9 Framework State The kernel’s operational state is a framework envelope around the domain state, carrying the audit log and the review queue. Definition A.28 (Framework state). For D:AdjudicableD: Adjudicable, the framework state type is D≜×D×(D)×D. FState_D\; \; EntityId× State_D× List( AuditEntry_D)× ReviewQueue_D. We write s.s. domain, s.s. audit, s.s. queue for the projections onto the domain state, the audit log, and the review queue respectively. Definition A.29 (Audit entry). An audit entry records the outcome of an adjudication: D≜ AuditEntry_D\; \; ×,, Id× Time×\ approved, rejected, escalated\ ×D×(×). × Action_D× Option( InvariantId× String). Definition A.30 (Review queue and pending proposal). D≜×D×, PendingProposal_D\; \; Id× Action_D× InvariantId× String× Time, D≜(D). ReviewQueue_D\; \; List( PendingProposal_D). The audit log and review queue evolve deterministically with every adjudication: an approved commit appends one audit entry; a rejection appends an audit entry and leaves the queue unchanged; an escalation appends both an audit entry and a pending proposal. Domain invariants D invariants_D are statements about s.s. domain, not about s.s. audit or s.s. queue; integrity of the audit log and queue is a separate kernel-level property. A.1.10 Coordination Protocol and Commit Discipline An architecture is individuated by two independent pieces of data: who runs when, and how proposals become committed transitions. Definition A.31 (Coordination protocol). A coordination protocol is a computable partial function π:D×Π×Ω⇀D×D.π\;:\; FState_D× × Roles_D× Action_D. Given the current framework state, the agent population, and the oracle trace, π selects a role r, invokes αr _r on D(s.,r) project_D(s. domain,r), and returns the pair (r,a)(r,a) where a is the returned action. Definition A.32 (Commit discipline). A commit discipline is a computable partial function κ:D×D×Ω⇀D.κ\;:\; FState_D× Action_D× Time× FState_D. Given the current framework state, a proposed action, a timestamp, and the oracle trace, κ produces the next framework state, including any updates to the audit log and review queue. The separation is deliberate: π decides what is proposed and by whom; κ decides what happens to proposals. Agentic Redux, and the extensions previewed for future work, differ in (π,κ)(π,κ) while sharing the same agent population type. A.1.11 Agent Architecture Definition A.33 (Agent architecture). An agent architecture over a domain D:D: DOMAIN is a tuple =(Π,μD,π,κ)A\;=\;( ,\; _D,\;π,\;κ) consisting of an agent population, a meta-agent, a coordination protocol, and a commit discipline. The “given agents A, B, C, an architecture is Y” template reads, in this vocabulary: an architecture for (αA,αB,αC)( _A, _B, _C) is any tuple (Π,μD,π,κ)( , _D,π,κ) with Π=(αA,αB,αC) =( _A, _B, _C). Agentic Redux is the specific instance of section A.1.12 below. A.1.12 Agentic Redux as an Instance Definition A.34 (Agentic Redux coordination protocol). The Agentic Redux coordination protocol πAgentic Reduxπ Agentic Redux operates as follows. At each step, given a framework state s, an agent population Π , and an oracle trace ω: 1. consult ω to select a role r∈Dr∈ Roles_D (the arbitration choice); 2. compute the slice σ=D(s.,r)σ= project_D(s. domain,r); 3. invoke αr(σ,ω) _r(σ,ω) to obtain an action a; 4. return (r,a)(r,a). At most one (r,a)(r,a) pair is in flight to the commit discipline at any time. Simultaneity among real-world agents is absorbed into the arbitration choice in Step 1. Definition A.35 (Agentic Redux commit discipline). The Agentic Redux commit discipline κAgentic Reduxκ Agentic Redux is the function that, on input (s,a,t,ω)(s,a,t,ω): 1. computes the candidate domain state s^≜D(s.,a,t) s\; \; applyMutation_D(s. domain,a,t); 2. walks D invariants_D in list order, evaluating each invariant on s s; 3. halts on the first invariant ιk∈D _k∈ invariants_D whose evaluation on s s does not return pass: • if ιk(s^)=(m) _k( s)= reject(m), appends to s.s. audit a single entry with tag rejected, action a, timestamp t, and witness slot (id(ιk),m) Some(id( _k),m), and returns the framework state with domain and queue components unchanged; • if ιk(s^)=(m) _k( s)= escalate(m), appends to s.s. audit a single entry with tag escalated, action a, timestamp t, and witness slot (id(ιk),m) Some(id( _k),m), and appends to s.s. queue a single pending proposal carrying action a, id(ιk)id( _k), m, and t, returning the framework state with domain component unchanged; 4. if every invariant returns pass on s s, appends to s.s. audit a single entry with tag approved, action a, timestamp t, and witness slot None, and returns the framework state with domain component s s and queue component unchanged. Each branch appends exactly one audit entry; the approve and reject branches leave the queue unchanged, and the escalate branch appends exactly one pending proposal. Remark A.36 (Eager validation and strict serialisation). κAgentic Reduxκ Agentic Redux produces a candidate domain state via D applyMutation_D and then evaluates every invariant on that candidate before committing it to the framework state (Step 4 of section A.1.12). In the terminology of concurrency control, this is eager validation combined with strict serialisation: proposals are dispatched one at a time (section A.1.13), invariants are checked synchronously against the candidate, and the candidate is committed only when every invariant has returned pass. The isolation level is serializable in the sense of Berenson et al. [7]: Write Skew (anomaly A5B) is structurally excluded (section A.2, Corollary 1). Definition A.37 (The Agentic Redux architecture). For D:D: DOMAIN, and for any agent population Π over D, the Agentic Redux architecture over D with population Π is the tuple (D,Π)≜(Π,μDAgentic Redux,πAgentic Redux,κAgentic Redux), AgenticRedux(D, )\; \;( ,\; _D Agentic Redux,\;π Agentic Redux,\;κ Agentic Redux), where μDAgentic Redux _D Agentic Redux is the meta-agent whose behaviour is specified by κAgentic Reduxκ Agentic Redux. When the population is clear from context we write simply (D) AgenticRedux(D). A.1.13 Configurations, Reduction, Executions The calculus’s operational semantics is a deterministic small-step reduction on configurations parameterised by an oracle trace. The reduction relation is sequential: at most one step occurs per transition, and there is no concurrent or parallel composition. Definition A.38 (Configuration). A configuration is a triple ⟨e,s,ω⟩ e,\,s,\,ω where: • e is the client program term under reduction; • s:Ds: FState_D is the current framework state; • ω∈Ωω∈ is the remaining oracle trace. The oracle position advances as the reduction consumes trace elements. Definition A.39 (Well-typed configuration over (D) AgenticRedux(D)). A configuration ⟨e,s,ω⟩ e,\,s,\,ω is well-typed over (D) AgenticRedux(D) iff: 1. e is closed and ∅⊢De:τ _De:τ for some type τ, per the typing rules of section A.1.15; 2. s:Ds: FState_D and s.:Ds. domain: State_D. Remark A.40 (Slice freshness via the reduction rules, not typing). An earlier draft of Definition A.1.13 included a third condition constraining slices passed to agents to be derived from the current framework state. That content is enforced structurally by E-Coordinate, which reads s from the enclosing configuration at the moment the rule fires and computes D(s.,r) project_D(s. domain,r) at that same moment, together with the term grammar’s lack of a value form for slices (Remark A.1.14), which prevents any reduction from introducing a captured slice for later invocation. The dropped typing condition is therefore redundant with the operational semantics. Definition A.41 (Reduction). The reduction relation ⟨e,s,ω⟩⟶⟨e′,s′,ω′⟩ e,\,s,\,ω \; \; e ,\,s ,\,ω is a deterministic single-step relation on configurations. Its defining rules appear in section A.1.14; the key architecture rules are E-Coordinate (invoking πAgentic Reduxπ Agentic Redux to elicit a proposal) and E-Adjudicate (invoking κAgentic Reduxκ Agentic Redux to produce an outcome). Each rule consumes zero or more elements from ω and advances the trace accordingly. We write ⟶∗ ^* for the reflexive-transitive closure. Definition A.42 (Execution). An execution of e0e_0 from initial framework state s0s_0 with oracle trace ω is the unique (finite or infinite) sequence ⟨e0,s0,ω⟩⟶⟨e1,s1,ω1⟩⟶⟨e2,s2,ω2⟩⟶⋯ e_0,\,s_0,\,ω \; \; e_1,\,s_1,\, _1 \; \; e_2,\,s_2,\, _2 \; \;·s generated by the reduction relation, where each ωi+1 _i+1 is the suffix of ωi _i remaining after the reduction step consumed its oracle reads. We write (e0,s0,ω) Exec(e_0,s_0,ω) for this sequence. Remark A.43 (Sequentiality absorbs simultaneity). The reduction relation is a function of the configuration and the oracle: each non-terminal configuration has exactly one successor. Concurrent real-world activity — two agents producing proposals at the same wall-clock moment, or two users clicking a button simultaneously — is modelled by selecting an arbitration order from the oracle in πAgentic Reduxπ Agentic Redux’s Step 1. A theorem that ranges over all oracle traces therefore ranges over all possible arbitration orders, which is to say over all possible concurrent schedules. This is the architecture’s answer to “what happens if two agents act at once?”: the meta-agent serialises them in oracle-chosen order, and the theorems hold for every order. Definition A.44 (Reachable domain state). A domain state s∈Ds∈ State_D is reachable in (e0,s0,ω) Exec(e_0,s_0,ω) iff there exists an index i such that si.=s_i. domain=s. A.1.14 Operational Semantics We now give the reduction rules declared in Definition A.1.13. The relation operates on configurations ⟨e,s,ω⟩ e,\,s,\,ω (Definition A.1.13) and is deterministic: each non-terminal configuration has exactly one successor. Core term language. The reduction rules refer to a small core term language sufficient to house the architecture primitives. Here we fix only the constructors needed by the rules below. e::= e\;::=\;\; v∣x∣x=e1e2 v\; \;x\; \; let\;x=e_1\; in\;e_2 ∣ \; \; coordinate ∣(e1,e2) \; \; adjudicate(e_1,e_2) ∣(e) \; \; entry(e) ∣ \; \; done with values ranged over by v: v::= v\;::=\;\; ()∣(r,a)∣∣ ()\; \;(r,a)\; \; approved\; \; rejected\; \; escalated The pair value (r,a)(r,a) is a coordinated proposal: a role paired with the action that role’s agent returned. The three outcome tags approved, rejected, escalated are values; they are the result tags attached to audit entries by Definition A.1.9. The term coordinate has no explicit arguments because, by Definition A.1.12, πAgentic Reduxπ Agentic Redux reads the current framework state and oracle trace directly from the configuration. The term (e1,e2) adjudicate(e_1,e_2) takes a coordinated proposal e1e_1 (reducing to a pair (r,a)(r,a)) and a timestamp e2e_2 (reducing to a value in Time). The term (e) entry(e) indicates a commit-cycle entry point — the client program’s only way to request that the kernel perform one coordinate/adjudicate cycle — and reduces to the outcome tag of the cycle. The term done marks a terminal program. This is the minimum surface needed to state the reduction rules. A realistic client program will wrap these primitives in loops or recursive calls; such wrappers are themselves client code and reduce by the standard rules of the ambient typed lambda calculus [23]. Evaluation contexts. Reduction is defined by a small set of primitive rules together with a compatible-closure rule under evaluation contexts: E::=[⋅]∣x=Ee∣(E,e)∣(v,E)∣(E).E\;::=\;[\,·\,]\; \; let\;x=E\; in\;e\; \; adjudicate(E,e)\; \; adjudicate(v,E)\; \; entry(E). E-Ctx ⟶⟨e,s,ω⟩⟨e′,s′,ω′⟩ ⟶⟨E[e],s,ω⟩⟨E[e′],s′,ω′⟩ 44.35983pt $ e,\,s,\,ω \; \; e ,\,s ,\,ω $ 57.87372pt $ E[e],\,s,\,ω \; \; E[e ],\,s ,\,ω $ All other rules operate on terms at the top of the evaluation context; E-Ctx lifts them to arbitrary program positions. Evaluation is left-to-right and call-by-value. Administrative reductions. The following rules are standard and consume no oracle. They govern sequencing of the client program. E-Let ⟶⟨=letxvine,s,ω⟩⟨e[/vx],s,ω⟩ $ \;$ 78.40591pt $ let\;x=v\; in\;e,\,s,\,ω \; \; e[v/x],\,s,\,ω $ No other administrative rules are needed: the remaining client-level constructors (application, case analysis, etc.) step by the standard call-by-value rules of the typed lambda calculus [23], lifted through E-Ctx onto configurations without consulting s or ω. Architecture reductions. The two rules below are the operational heart of Agentic Redux. They invoke, respectively, the Agentic Redux coordination protocol (Definition A.1.12) and the Agentic Redux commit discipline (Definition A.1.12). Writing ω⇒kω′ω _kω for “ω′ω is the suffix of ω remaining after k consultations,” we let each rule consume whatever oracle prefix the invoked function consumes. The consumed count is not fixed by the calculus — πAgentic Reduxπ Agentic Redux consumes oracle for the arbitration choice and for any oracle reads performed by the invoked agent, while κAgentic Reduxκ Agentic Redux consumes no oracle, since invariants are pure state predicates (section A.1.3) — but is a deterministic function of the inputs passed to πAgentic Reduxπ Agentic Redux or κAgentic Reduxκ Agentic Redux. Coordinate. The coordinate term reads the current framework state and oracle, invokes πAgentic Reduxπ Agentic Redux to arbitrate a role, project its slice, and invoke its agent, and reduces to the returned (r,a)(r,a) pair. The framework state is unchanged: πAgentic Reduxπ Agentic Redux is a pure function of its inputs and produces a proposal, not a commit. E-Coordinate =πAgentic Redux(s,Π,ω)(r,a) ⇒kωω′ where k is the number of oracle reads performed by πAgentic Redux ⟶⟨coordinate,s,ω⟩⟨(r,a),s,ω′⟩ 164.7051pt $ π Agentic Redux(s, ,ω)\;=\;(r,a)$ $ ω\; _k\;ω where $ k$ is the number of oracle reads performed by $ π Agentic Redux$$ 69.49123pt $ coordinate,\,s,\,ω \; \; (r,a),\,s,\,ω $ The agent population Π is fixed by the client program’s instantiation of (D,Π) AgenticRedux(D, ) (Definition A.1.12); it is a parameter of the reduction relation, not a runtime value. If πAgentic Redux(s,Π,ω)π Agentic Redux(s, ,ω) is undefined — for example, because Π is empty, or because the selected agent’s partial function does not terminate on the given slice — the configuration is stuck; E-Coordinate does not apply. Stuckness of well-typed configurations is ruled out by Type Safety (Theorem 5). Adjudicate. The adjudicate term takes a coordinated proposal (r,a)(r,a) and a timestamp t and invokes κAgentic Reduxκ Agentic Redux to produce a new framework state and an outcome tag. By Definition A.1.12, κAgentic Reduxκ Agentic Redux either appends an approval audit entry and applies the mutation, or appends a rejection/escalation audit entry and leaves s.s. domain unchanged. We split the rule by outcome so that the three cases are individually inspectable in proofs. E-Adjudicate-Approve =κAgentic Redux(s,a,t,ω)s′.audit=s.audit++[approval entry] s′.=queues.queue s′.=domainapplyMutationD(s.domain,a,t) ⇒kω′ ⟶⟨adjudicate((r,a),t),s,ω⟩⟨approved,s′,ω′⟩ 145.43646pt $ κ Agentic Redux(s,a,t,ω)\;=\;s $ $ s . audit\;=\;s. audit\,+\!+\,[\,approval entry\,]$ $ s . queue\;=\;s. queue$ $ s . domain\;=\; applyMutation_D(s. domain,a,t)$ $ ω\; _k\;ω $ 97.1718pt $ adjudicate((r,a),t),\,s,\,ω \; \; approved,\,s ,\,ω $ E-Adjudicate-Reject =κAgentic Redux(s,a,t,ω)s′.audit=s.audit++[rejection entry] s′.=queues.queue s′.=domains.domain ⇒kω′ ⟶⟨adjudicate((r,a),t),s,ω⟩⟨rejected,s′,ω′⟩ 98.70825pt $ κ Agentic Redux(s,a,t,ω)\;=\;s $ $ s . audit\;=\;s. audit\,+\!+\,[\,rejection entry\,]$ $ s . queue\;=\;s. queue$ $ s . domain\;=\;s. domain$ $ ω\; _k\;ω $ 94.74123pt $ adjudicate((r,a),t),\,s,\,ω \; \; rejected,\,s ,\,ω $ E-Adjudicate-Escalate =κAgentic Redux(s,a,t,ω)s′.audit=s.audit++[escalation entry] s′.queue=s.queue++[pending proposal] s′.=domains.domain ⇒kω′ ⟶⟨adjudicate((r,a),t),s,ω⟩⟨escalated,s′,ω′⟩ 150.41663pt $ κ Agentic Redux(s,a,t,ω)\;=\;s $ $ s . audit\;=\;s. audit\,+\!+\,[\,escalation entry\,]$ $ s . queue\;=\;s. queue\,+\!+\,[\,pending proposal\,]$ $ s . domain\;=\;s. domain$ $ ω\; _k\;ω $ 97.394pt $ adjudicate((r,a),t),\,s,\,ω \; \; escalated,\,s ,\,ω $ The three rules are exhaustive and mutually exclusive: κAgentic Redux(s,a,t,ω)κ Agentic Redux(s,a,t,ω) is a deterministic function (Definition A.1.12) whose output falls into exactly one of the three branches. The “approval entry,” “rejection entry,” “escalation entry,” and “pending proposal” appearing in the rules are the concrete audit and queue items constructed by κAgentic Reduxκ Agentic Redux; their exact shape is fixed by Definitions A.1.9 and A.1.9. Entry and termination. The entry constructor provides a syntactic marker for a complete commit cycle. Its rule is administrative: E-Entry ⟶⟨entry(v),s,ω⟩⟨v,s,ω⟩ $ \;$ 55.21516pt $ entry(v),\,s,\,ω \; \; v,\,s,\,ω $ A configuration ⟨,s,ω⟩ done,\,s,\,ω is terminal: no rule applies. Values other than done are terminal only when no enclosing evaluation context can step them via E-Ctx or E-Let. Structural lemmas. Five lemmas about the reduction relation will be cited by the metatheory of section A.2. All are proved by inspection of the rules of section A.1.14. Lemma A.45 (Determinism). ⟶ is a partial function on configurations. Proof. The primitive reduction rules operate on disjoint top-level term constructors ( let, coordinate, adjudicate, entry), so at most one primitive rule applies at any evaluation-context redex. The three E-Adjudicate-* rules are discriminated by the output of κAgentic Reduxκ Agentic Redux, which is a computable partial function of its inputs (Definition A.1.12). E-Ctx lifts primitive rules through evaluation contexts left-to-right and call-by-value; the evaluation context for a given non-value term is unique. Each rule that consults the oracle does so through a single call to πAgentic Reduxπ Agentic Redux or κAgentic Reduxκ Agentic Redux, each a computable partial function of its inputs (Definitions A.1.10, A.1.10); the number of oracle elements consumed, and the resulting suffix ω′ω , are therefore functions of the configuration alone, not additional nondeterministic choices. ∎ Remark A.46 (Rule classification). The reduction rules of section A.1.14 fall into two classes by the shape of their conclusion’s domain clause: a rule is applyMutation-applying if its conclusion fixes s′.=D(s.,a,t)s . domain= applyMutation_D(s. domain,a,t) for some action and timestamp, and domain-preserving otherwise — meaning its conclusion either fixes s′.=s.s . domain=s. domain explicitly or leaves s entirely unchanged. The unique applyMutation-applying rule of the base calculus is E-Adjudicate-Approve; E-Let, E-Coordinate, E-Adjudicate-Reject, E-Adjudicate-Escalate, and E-Entry are domain-preserving. E-Ctx inherits the class of the rule it lifts. The metatheory below depends on the rule set only through this classification: an extension that declares each new rule applyMutation-applying or domain-preserving extends every result whose proof appeals only to the classification, with Lemma A.1.14 and the domain-preserving case of Theorem 1 extending verbatim. The applyMutation-applying case requires the extension to discharge its own analogue of Lemma A.1.14, a non-classification property. Lemma A.47 (Domain-state localization). For every reduction step ⟨e,s,ω⟩⟶⟨e′,s′,ω′⟩ e,\,s,\,ω e ,\,s ,\,ω generated by a domain-preserving rule, possibly lifted through E-Ctx, s′.=s.s . domain=s. domain. Proof. By case analysis on the primitive rule invoked, with E-Ctx as the inductive step. Rules E-Let and E-Entry leave s entirely unchanged. Rule E-Coordinate carries s through its conclusion without modification. Rules E-Adjudicate-Reject and E-Adjudicate-Escalate both include s′.=s.s . domain=s. domain as an explicit premise. E-Ctx preserves s′.=s.s . domain=s. domain by the inductive hypothesis applied to the inner step. This is the formal content, at the level of the reduction relation, of “the meta-agent is the only component permitted to produce an approved-tagged outcome” (Definition A.1.7): the applyMutation-applying rule E-Adjudicate-Approve is the sole route by which s.s. domain can change in the base calculus. ∎ Lemma A.48 (Approval soundness). If ⟨((r,a),t),s,ω⟩⟶⟨,s′,ω′⟩ adjudicate((r,a),t),\,s,\,ω approved,\,s ,\,ω under E-Adjudicate-Approve, then s′.⊧Ds . domain invariants_D. Proof. The E-Adjudicate-Approve rule applies when κAgentic Redux(s,a,t,ω)κ Agentic Redux(s,a,t,ω) follows the pass-all branch of Definition A.1.12. By Step 1 of that definition, κAgentic Reduxκ Agentic Redux computes the candidate s^=D(s.,a,t) s= applyMutation_D(s. domain,a,t) before walking the invariant list. By Step 2, each invariant is evaluated on s s. The pass-all branch (Step 4) is reached precisely when every ι∈D ∈ invariants_D returns pass on s s, which by Definition A.1.4 is s^⊧D s invariants_D. The rule’s premises fix s′.=D(s.,a,t)=s^s . domain= applyMutation_D(s. domain,a,t)= s, yielding s′.⊧Ds . domain invariants_D. ∎ Lemma A.49 (Non-approval witness). If ⟨((r,a),t),s,ω⟩⟶⟨,s′,ω′⟩ adjudicate((r,a),t),\,s,\,ω rejected,\,s ,\,ω under E-Adjudicate-Reject, or ⟨((r,a),t),s,ω⟩⟶⟨,s′,ω′⟩ adjudicate((r,a),t),\,s,\,ω escalated,\,s ,\,ω under E-Adjudicate-Escalate, then there exist ιk∈D _k∈ invariants_D and m∈m∈ String such that, letting s^=D(s.,a,t) s= applyMutation_D(s. domain,a,t): • on the E-Adjudicate-Reject branch, ιk(s^)=(m) _k( s)= reject(m); • on the E-Adjudicate-Escalate branch, ιk(s^)=(m) _k( s)= escalate(m); • in particular ιk(s^)≠ _k( s)≠ pass; and • the entry appended to s′.s . audit by this step has witness slot (id(ιk),m) Some(id( _k),m). Proof. In either case, κAgentic Redux(s,a,t,ω)κ Agentic Redux(s,a,t,ω) follows the non- pass-all branch of Definition A.1.12. Step 1 computes s^=D(s.,a,t) s= applyMutation_D(s. domain,a,t); Step 2 evaluates each invariant on s s; Step 3 halts on the first invariant ιk∈D _k∈ invariants_D with ιk(s^)≠ _k( s)≠ pass. By Definition A.1.3, ιk(s^) _k( s) must have the form (m) reject(m) or (m) escalate(m) for some m∈m∈ String. On the reject branch of Step 3, Definition A.1.12 appends to s.s. audit an entry with witness slot (id(ιk),m) Some(id( _k),m); analogously on the escalate branch. In both cases ιk(s^)≠ _k( s)≠ pass. ∎ Lemma A.50 (Audit append discipline). For every reduction step ⟨e,s,ω⟩⟶⟨e′,s′,ω′⟩ e,\,s,\,ω e ,\,s ,\,ω : • if the step is an instance of E-Adjudicate-Approve, E-Adjudicate-Reject, or E-Adjudicate-Escalate (possibly lifted through E-Ctx), then s′.=s.++[entry]s . audit=s. audit\,+\!+\,[\,entry\,] for exactly one entry, fixed by Definition A.1.12; • otherwise, s′.=s.s . audit=s. audit. Proof. By case analysis on the primitive rule invoked, with E-Ctx as the inductive step. The three E-Adjudicate-* rules each have premise s′.=s.++[entry]s . audit=s. audit\,+\!+\,[\,entry\,] for one entry whose shape is fixed by Definition A.1.12. The remaining rules (E-Let, E-Coordinate, E-Entry) carry s through their conclusions syntactically, so the audit field is unchanged. E-Ctx preserves both cases by the inductive hypothesis applied to the inner step. ∎ Remark A.51 (Slices are computed at invocation time). The coordinate rule reads s from the enclosing configuration at the moment the rule fires, and πAgentic Reduxπ Agentic Redux computes the slice D(s.,r) project_D(s. domain,r) at that same moment. No rule captures a slice into a term for later use: the term language has no value form for slices. An agent can therefore only be invoked on a slice derived from the current framework state. A.1.15 Typing Rules The typing judgment for the calculus takes the form Γ⊢De:τ _De:τ, parameterised by a fixed D:D: DOMAIN and a variable context Γ mapping variables to types. Types are drawn from the following grammar: τ::=∣D∣D∣τ1×τ2∣D.τ\;::=\; Unit\; \; Roles_D\; \; Action_D\; \; Time\; \; _1× _2\; \; Outcome_D. The types D Roles_D, D Action_D, and Time are base types whose inhabitants are the role, action, and timestamp constants supplied by the domain and the ambient calculus. The type Unit has inhabitants ()() and done. Remark A.52 (Outcome type at the calculus level). The type D Outcome_D appearing in the typing grammar above is the three-tag type inhabited by the outcome constants ,, approved, rejected, escalated. This is the calculus-level projection of the meta-agent’s output type (Definition A.1.7), whose branches additionally carry payloads. At reduction time, the payload information is routed into the framework-state update performed by κAgentic Reduxκ Agentic Redux (Definition A.1.12), while the three tags alone remain as the term-level residual. The rules for variables, let-bindings, and the two inhabitants of Unit are standard. T-Var :x∈τΓ :Γ⊢Dxτ $ x:τ∈ $ 20.40631pt $ _Dx:τ$ T-Unit :Γ⊢D()Unit \> $ \ $ 26.88382pt $ _D(): Unit$ T-Done :Γ⊢DdoneUnit \> $ \ $ 31.49496pt $ _D done: Unit$ T-Let :Γ⊢De1τ1 Γ,x:τ1⊢De2:τ2 :=Γ⊢Dletxe1ine2τ2 64.90134pt $ _De_1: _1$ $ ,x: _1 _De_2: _2$ 50.2361pt $ _D let\;x=e_1\; in\;e_2: _2$ The base-type constants are typed by axiom. T-Role ∈rRolesD :Γ⊢DrRolesD 21.80629pt $ r∈ Roles_D$ 31.05814pt $ _Dr: Roles_D$ T-Action ∈aActionD :Γ⊢DaActionD 24.63094pt $ a∈ Action_D$ 33.8828pt $ _Da: Action_D$ T-Time ∈tTime :Γ⊢DtTime $ t∈ Time$ 26.57129pt $ _Dt: Time$ T-Approved :Γ⊢DapprovedOutcomeD \> $ \ $ 53.94826pt $ _D approved: Outcome_D$ T-Rejected :Γ⊢DrejectedOutcomeD \> $ \ $ 51.51767pt $ _D rejected: Outcome_D$ T-Escalated :Γ⊢DescalatedOutcomeD \> $ \ $ 54.17046pt $ _D escalated: Outcome_D$ A coordinated proposal (r,a)(r,a) is typed by the product-introduction rule specialised to the role/action pair. T-Proposal :Γ⊢DrRolesD :Γ⊢DaActionD :Γ⊢D(r,a)×RolesDActionD 74.94095pt $ _Dr: Roles_D$ $ _Da: Action_D$ 60.6891pt $ _D(r,a): Roles_D× Action_D$ The three architecture primitives are typed as follows. T-Coordinate :Γ⊢Dcoordinate×RolesDActionD \> $ \ $ 70.15155pt $ _D coordinate: Roles_D× Action_D$ T-Adjudicate :Γ⊢De1×RolesDActionD :Γ⊢De2Time :Γ⊢Dadjudicate(e1,e2)OutcomeD 90.94858pt $ _De_1: Roles_D× Action_D$ $ _De_2: Time$ 73.17393pt $ _D adjudicate(e_1,e_2): Outcome_D$ T-Entry :Γ⊢DeOutcomeD :Γ⊢Dentry(e)OutcomeD 38.9152pt $ _De: Outcome_D$ 53.42912pt $ _D entry(e): Outcome_D$ T-Coordinate assigns the coordinate primitive the type of its reduct, a coordinated proposal. T-Adjudicate requires a coordinated proposal and a timestamp and returns an outcome tag. T-Entry preserves the outcome type of its argument, marking a complete commit cycle. Remark A.53 (What the typing discipline does and does not enforce). The typing rules rule out ill-formed combinations such as (,) adjudicate( approved, approved), which would be operationally stuck under the rules of section A.1.14. They do not enforce domain-level well-formedness of the action in a proposal (r,a)(r,a); in particular, they do not require that a∈D(r)a∈ Action_D(r) in the sense of Definition A.1.6. That refinement is enforced operationally by πAgentic Reduxπ Agentic Redux, which produces proposals by invoking αr _r on D(r) Slice_D(r) and whose returned action is classified as belonging to role r by Condition 1 of Definition A.1.6. Pushing the role-indexing into the type system would require dependent products and is not necessary for any result in this paper. A.1.16 Vocabulary for Theorem Statements Every concept appearing in the informal theorem statements of section A.2 has a formal counterpart above. The following table records the dependency of each theorem on the preceding definitions. Result Scope Required definitions T1 Invariant Preservation Adjudicable A.1.3, A.1.3, A.1.4, A.1.12, A.1.13, A.1.13, A.1.13 P1 Agent Confinement DOMAIN A.1.1, A.1.2, A.1.2, A.1.3, A.1.6, A.1.5, A.1.13 T2 Audit Log Integrity Adjudicable A.1.3, A.1.3, A.1.4, A.1.9, A.1.12, A.1.13, A.1.13 T3 Type Safety DOMAIN A.1.13, A.1.13, A.1.13, A.1.15 C1 Write Skew Freedom DOMAIN A.1.2, A.2.3, A.1.13, A.1.13, T1 A.2 Metatheory A.2.1 Invariant Preservation Theorem 1 (Invariant Preservation). For every D:AdjudicableD: Adjudicable, every client program e0e_0 well-typed over (D) AgenticRedux(D), every initial framework state s0s_0 of type D FState_D with s0.⊧Ds_0. domain invariants_D, and every oracle trace ω∈Ωω∈ : every reachable domain state in (e0,s0,ω) Exec(e_0,s_0,ω) satisfies D invariants_D. Proof. Let s be a reachable domain state in (e0,s0,ω) Exec(e_0,s_0,ω). By Definition A.1.13, there exists an index i≥0i≥ 0 with s=si.s=s_i. domain. We show, by induction on i, that sj.⊧Ds_j. domain invariants_D for every 0≤j≤i0≤ j≤ i; specialising to j=ij=i yields s⊧Ds invariants_D. Base case (j=0j=0). By hypothesis, s0.⊧Ds_0. domain invariants_D. Inductive step. Assume sj.⊧Ds_j. domain invariants_D for some j<ij<i. The execution’s step at index j is a reduction ⟨ej,sj,ωj⟩⟶⟨ej+1,sj+1,ωj+1⟩ e_j,\,s_j,\, _j e_j+1,\,s_j+1,\, _j+1 , and is classified by whether it is an instance of E-Adjudicate-Approve. Case 1: the step is generated by a domain-preserving rule (Remark A.1.14). By Lemma A.1.14, sj+1.=sj.s_j+1. domain=s_j. domain. The inductive hypothesis gives sj+1.⊧Ds_j+1. domain invariants_D. Case 2: the step is generated by an applyMutation-applying rule. In the base calculus the unique such rule is E-Adjudicate-Approve, possibly lifted through E-Ctx. The primitive-rule instance then has the form ⟨((r,a),t),sj,ωj⟩⟶⟨,sj+1,ωj+1⟩ adjudicate((r,a),t),\,s_j,\, _j \; \; approved,\,s_j+1,\, _j+1 for some role r, action a, and timestamp t; E-Ctx (section A.1.14) passes the framework state and oracle through unchanged. By Lemma A.1.14, sj+1.⊧Ds_j+1. domain invariants_D. In either case, sj+1.⊧Ds_j+1. domain invariants_D, completing the induction. ∎ Remark A.54 (Reachable-state form). Theorem 1 is stated about reachable domain states rather than about a relation between each approval step’s pre-state and its committed action. The reachable-state form is what a compliance argument actually needs to cite (“no reachable state violates an invariant”), and it is available only because Lemma A.1.14 establishes invariant satisfaction on the post-state of each approval, rather than on the pre-state-plus-action pair that was evaluated. The soundness of the commit-discipline post-check (Remark A.1.3) is therefore what drives the inductive step; a per-approval-step statement phrased on the pre-state-plus-action pair would reveal only a weaker, contingent relationship. A.2.2 Agent Confinement Proposition 1 (Agent Confinement). For every D:D: DOMAIN, the following two confinement properties hold. (i) Observation confinement. For every role r∈Dr∈ Roles_D, every agent αr∈D(r) _r∈ Agent_D(r), every oracle trace ω∈Ωω∈ , and every pair of domain states s1,s2∈Ds_1,s_2∈ State_D with D(s1,r)=D(s2,r) project_D(s_1,r)= project_D(s_2,r): if αr(D(s1,r),ω) _r( project_D(s_1,r),ω) is defined then αr(D(s2,r),ω) _r( project_D(s_2,r),ω) is defined and equal. (i) Write-authority confinement. For every primitive reduction ⟨,s,ω⟩⟶⟨(r,a),s′,ω′⟩ coordinate,\,s,\,ω (r,a),\,s ,\,ω under E-Coordinate: s′=s =s. In particular, s′.=s.s . domain=s. domain. Proof. Part (i). Immediate from Definition A.1.6: an agent αr _r is a function whose first argument is its role’s slice. By hypothesis, the two slices agree, so the applications αr(D(s1,r),ω) _r( project_D(s_1,r),ω) and αr(D(s2,r),ω) _r( project_D(s_2,r),ω) are at the same argument pair, hence equal where defined. Part (i). Immediate from E-Coordinate (section A.1.14): the conclusion of the rule is ⟨(r,a),s,ω′⟩ (r,a),\,s,\,ω , threading the framework state s unchanged from the premise. The equality s′=s =s is therefore syntactic, and s′.=s.s . domain=s. domain follows. This case of Lemma A.1.14 is thus strengthened: invoking an agent mutates neither the domain state nor any other component of the framework state. ∎ A.2.3 Write Skew Freedom A write-skew execution at the calculus level is the formal counterpart of Berenson et al.’s anomaly A5B in the database-isolation setting [7]: a committed state violating a constraint that references state modified by more than one concurrent transaction — a constraint no transaction, operating on its own view, could have caused to fail alone. In the calculus, a sub-agent observes exactly its role’s slice (Definitions A.1.2, A.1.6), so the calculus-level analogue of such a constraint is a cross-cutting invariant (Definition A.1.2). Scheduling non-determinism that in the classical setting arises from concurrent transactions is absorbed here into the oracle, which selects the arbitration order in which πAgentic Reduxπ Agentic Redux elicits proposals (Remark A.1.13); ranging over all ω∈Ωω∈ therefore ranges over all possible schedules. Definition A.55 (Write-skew execution at the calculus level). An execution (e0,s0,ω) Exec(e_0,s_0,ω) of (D) AgenticRedux(D) is a write-skew execution iff there exist a reachable domain state s and a cross-cutting invariant ι∈D ∈ invariants_D with ι(s)≠ (s)≠ pass. Corollary 1 (Write Skew Freedom). For every D:D: DOMAIN, every client program e0e_0 well-typed over (D) AgenticRedux(D), every initial framework state s0s_0 of type D FState_D with s0.⊧Ds_0. domain invariants_D, and every oracle trace ω∈Ωω∈ : (e0,s0,ω) Exec(e_0,s_0,ω) is not a write-skew execution. Proof. By Theorem 1, every reachable domain state in (e0,s0,ω) Exec(e_0,s_0,ω) satisfies D invariants_D, hence satisfies every cross-cutting invariant in particular. The execution therefore does not meet Definition A.2.3. ∎ A.2.4 Audit Log Integrity Theorem 2 (Audit Log Integrity). For every D:AdjudicableD: Adjudicable, every client program e0e_0 well-typed over (D) AgenticRedux(D), every initial framework state s0s_0 of type D FState_D, and every oracle trace ω∈Ωω∈ , the execution (e0,s0,ω) Exec(e_0,s_0,ω) satisfies: (i) Faithful approval entries. For every step ⟨ej,sj,ωj⟩⟶⟨ej+1,sj+1,ωj+1⟩ e_j,\,s_j,\, _j e_j+1,\,s_j+1,\, _j+1 in the execution that is an instance of E-Adjudicate-Approve (possibly lifted through E-Ctx) with coordinated proposal (r,a)(r,a) and timestamp t: the sole entry appended to sj+1.s_j+1. audit is tagged approved, carries action a and timestamp t, and has witness slot None. (i) Faithful non-approval entries with witness. For every step ⟨ej,sj,ωj⟩⟶⟨ej+1,sj+1,ωj+1⟩ e_j,\,s_j,\, _j e_j+1,\,s_j+1,\, _j+1 in the execution that is an instance of E-Adjudicate-Reject (resp. E-Adjudicate-Escalate), possibly lifted through E-Ctx, with coordinated proposal (r,a)(r,a) and timestamp t: the sole entry appended to sj+1.s_j+1. audit is tagged rejected (resp. escalated), carries action a and timestamp t, and has witness slot (id(ιk),m) Some(id( _k),m) where ιk∈D _k∈ invariants_D satisfies ιk(D(sj.,a,t))=(m) _k( applyMutation_D(s_j. domain,a,t))= reject(m) (resp. (m) escalate(m)); in particular ιk(D(sj.,a,t))≠ _k( applyMutation_D(s_j. domain,a,t))≠ pass. (i) Exclusivity of provenance. For every reduction step ⟨ej,sj,ωj⟩⟶⟨ej+1,sj+1,ωj+1⟩ e_j,\,s_j,\, _j e_j+1,\,s_j+1,\, _j+1 in the execution that is not an instance of E-Adjudicate-Approve, E-Adjudicate-Reject, or E-Adjudicate-Escalate (possibly lifted through E-Ctx): sj+1.=sj.s_j+1. audit=s_j. audit. (iv) Append-only monotonicity. For every reduction step in the execution, sj.s_j. audit is a prefix of sj+1.s_j+1. audit. (v) Per-step exactness. For every reduction step in the execution that is an instance of E-Adjudicate-Approve, E-Adjudicate-Reject, or E-Adjudicate-Escalate (possibly lifted through E-Ctx): |sj+1.|=|sj.|+1|s_j+1. audit|=|s_j. audit|+1. Proof. Fix a step ⟨ej,sj,ωj⟩⟶⟨ej+1,sj+1,ωj+1⟩ e_j,\,s_j,\, _j e_j+1,\,s_j+1,\, _j+1 of the execution, derived from a primitive reduction rule, possibly lifted through E-Ctx (section A.1.14), which passes the framework state and oracle through unchanged. Clause (i). The primitive rule is E-Adjudicate-Approve. By Step 4 of Definition A.1.12, κAgentic Reduxκ Agentic Redux appends to sj.s_j. audit exactly one entry, tagged approved, with action a, timestamp t, and witness slot None; this is the entry fixed by the rule’s premise sj+1.=sj.++[approval entry]s_j+1. audit=s_j. audit\,+\!+\,[\,approval entry\,]. Clause (i). The primitive rule is E-Adjudicate-Reject or E-Adjudicate-Escalate. By Lemma A.1.14, the halt-witnessing invariant ιk∈D _k∈ invariants_D satisfies ιk(s^)=(m) _k( s)= reject(m) (resp. (m) escalate(m)) where s^=D(sj.,a,t) s= applyMutation_D(s_j. domain,a,t), and the sole entry appended to sj+1.s_j+1. audit has tag rejected (resp. escalated), action a, timestamp t, and witness slot (id(ιk),m) Some(id( _k),m). Clauses (i)–(v). Immediate from Lemma A.1.14: its E-Adjudicate-* branch fixes sj+1.=sj.++[entry]s_j+1. audit=s_j. audit\,+\!+\,[\,entry\,] for exactly one entry, supplying the prefix property of Clause (iv) and the cardinality identity of Clause (v); the complementary branch fixes sj+1.=sj.s_j+1. audit=s_j. audit, supplying Clause (i) and the trivial-prefix case of Clause (iv). ∎ Remark A.56 (Scope of Theorem 2 and “linearly in time”). Theorem 2 is purely structural: it characterises which reduction steps append to the audit log and what those entries look like. The companion semantic claim — that an approval step leaves the domain state satisfying D invariants_D — is the content of Theorem 1 (via Lemma A.1.14); it is not restated here. Clauses (i)–(v) together make precise the “linearly in time” claim of the informal body-text (section 1.3.2): the audit log grows by exactly one entry per adjudicate step, from no other reduction rule, and existing entries are never modified. A.2.5 Type Safety The metatheory above establishes the safety and auditability properties on which compliance arguments for Agentic Redux depend: invariant preservation and its write-skew corollary (Theorem 1, Corollary 1), audit log integrity (Theorem 2), and agent confinement (Proposition 1). The proofs of these results refer to D only through the operations declared by Adjudicable (Theorems 1 and 2, Corollary 1) and additionally by DOMAIN (Proposition 1); no step case-analyzes on a particular D. Instantiating Agentic Redux at any D of the appropriate signature therefore yields a system for which every corresponding result holds. We close the metatheory with Type Safety, the standard Progress-and-Preservation result for the calculus. Type Safety is not cited by any other result in this paper. It is presented here for two reasons. First, it documents that the calculus’s term grammar and typing rules interact cleanly with the reduction relation. Second, the architecture variants developed in [26] — Optimistic Parallel Redux and Hierarchical Agents — extend the term grammar of this paper with new constructors (respectively, a parallel-dispatch form with merge and retry, and a delegation form). Under those extensions the Progress cases acquire genuine content: a merge can fail, and a delegation can fall through a level of the hierarchy. Type Safety then becomes the theorem under which the new term forms are shown to interact cleanly with their extended reduction rules. The present result is the base case of that sequence. Theorem 3 (Type Safety). For every D:D: DOMAIN, every well-typed configuration over (D) AgenticRedux(D) satisfies: • (Preservation) If ⟨e,s,ω⟩ e,\,s,\,ω is well-typed over (D) AgenticRedux(D) with ∅⊢De:τ _De:τ, and ⟨e,s,ω⟩⟶⟨e′,s′,ω′⟩ e,\,s,\,ω e ,\,s ,\,ω , then ⟨e′,s′,ω′⟩ e ,\,s ,\,ω is well-typed over (D) AgenticRedux(D) with ∅⊢De′:τ _De :τ. • (Progress) If ⟨e,s,ω⟩ e,\,s,\,ω is well-typed over (D) AgenticRedux(D) and e is not a value, then either there exists a reduction step ⟨e,s,ω⟩⟶⟨e′,s′,ω′⟩ e,\,s,\,ω e ,\,s ,\,ω , or the configuration is operationally stuck on an undefined invocation of πAgentic Reduxπ Agentic Redux, κAgentic Reduxκ Agentic Redux, or an agent in Π . The proof uses three standard auxiliary lemmas. Lemma A.57 (Canonical forms). If ∅⊢Dv:τ _Dv:τ for a value v, then: • if τ=τ= Unit, then v∈(),v∈\(), done\; • if τ=D×Dτ= Roles_D× Action_D, then v=(r,a)v=(r,a) for some r∈Dr∈ Roles_D and a∈Da∈ Action_D; • if τ=τ= Time, then v is a timestamp constant; • if τ=Dτ= Outcome_D, then v∈,,v∈\ approved, rejected, escalated\. Proof. By inspection of section A.1.15. For each type, the only rules whose conclusions match a value of that type are the ones listed: T-Unit and T-Done for Unit; T-Proposal for D×D Roles_D× Action_D; T-Time for Time; and T-Approved, T-Rejected, T-Escalated for D Outcome_D. ∎ Lemma A.58 (Substitution). If Γ,x:τ1⊢De:τ2 ,x: _1 _De: _2 and Γ⊢Dv:τ1 _Dv: _1 for a value v, then Γ⊢De[v/x]:τ2 _De[v/x]: _2. Proof. By induction on the derivation of Γ,x:τ1⊢De:τ2 ,x: _1 _De: _2, standard for simply-typed calculi [23, Lemma 9.3.8]. The architecture primitives T-Coordinate, T-Adjudicate, and T-Entry have no dependence on Γ beyond the types of their subterms, so each case reduces to the inductive hypothesis applied to those subterms. ∎ A third ingredient is a decomposition lemma for evaluation contexts: a well-typed term filling an evaluation context has a well-defined type for the hole, and substituting a term of the same type into the hole preserves the overall type. This is standard for evaluation-context formulations of reduction [28]. Lemma A.59 (Evaluation-context decomposition). If ∅⊢DE[e1]:τ _DE[e_1]:τ, then there exists a type τ1 _1 such that ∅⊢De1:τ1 _De_1: _1, and for every e1′e_1 with ∅⊢De1′:τ1 _De_1 : _1, ∅⊢DE[e1′]:τ _DE[e_1 ]:τ. Proof. By induction on E (section A.1.14). • E=[⋅]E=[·]: take τ1=τ _1=τ; immediate. • E=x=E′e2E= let\;x=E \; in\;e_2: by inversion of T-Let, there exists τ1′ _1 with ∅⊢DE′[e1]:τ1′ _DE [e_1]: _1 and x:τ1′⊢De2:τx: _1 _De_2:τ. The inductive hypothesis on E′E supplies τ1 _1 and the substitution property; T-Let reconstructs the conclusion. • E=(E′,e2)E= adjudicate(E ,e_2): by inversion of T-Adjudicate, ∅⊢DE′[e1]:D×D _DE [e_1]: Roles_D× Action_D and ∅⊢De2: _De_2: Time, with τ=Dτ= Outcome_D. Apply the IH to E′E at type D×D Roles_D× Action_D. • E=(v,E′)E= adjudicate(v,E ): by inversion of T-Adjudicate, ∅⊢Dv:D×D _Dv: Roles_D× Action_D and ∅⊢DE′[e1]: _DE [e_1]: Time. Apply the IH to E′E at type Time. • E=(E′)E= entry(E ): by inversion of T-Entry, ∅⊢DE′[e1]:D _DE [e_1]: Outcome_D with τ=Dτ= Outcome_D. Apply the IH to E′E at type D Outcome_D. ∎ Proof of Theorem 3. We prove Preservation and Progress in turn. Preservation. Suppose ⟨e,s,ω⟩ e,\,s,\,ω is well-typed with ∅⊢De:τ _De:τ and s:Ds: FState_D, and a reduction ⟨e,s,ω⟩⟶⟨e′,s′,ω′⟩ e,\,s,\,ω e ,\,s ,\,ω is derived. We case-analyse on the primitive reduction rule invoked, with E-Ctx as the inductive step. Case E-Let. e=x=ve2e= let\;x=v\; in\;e_2 and e′=e2[v/x]e =e_2[v/x]. By inversion of T-Let, ∅⊢Dv:τ1 _Dv: _1 and x:τ1⊢De2:τx: _1 _De_2:τ. By Lemma A.2.5, ∅⊢De2[v/x]:τ _De_2[v/x]:τ. Framework state unchanged: s′=s =s. Case E-Coordinate. e=e= coordinate and e′=(r,a)e =(r,a) where (r,a)=πAgentic Redux(s,Π,ω)(r,a)=π Agentic Redux(s, ,ω). By T-Coordinate, τ=D×Dτ= Roles_D× Action_D. Definition A.1.12 specifies that πAgentic Reduxπ Agentic Redux selects r∈Dr∈ Roles_D and returns the action a produced by αr _r; by the agent’s type signature and Condition 1 of Definition A.1.6, a is an element of D Action_D classified as belonging to role r. Thus T-Role gives ∅⊢Dr:D _Dr: Roles_D, T-Action gives ∅⊢Da:D _Da: Action_D, and T-Proposal concludes ∅⊢D(r,a):D×D _D(r,a): Roles_D× Action_D. Framework state unchanged. Case E-Adjudicate-Approve. e=((r,a),t)e= adjudicate((r,a),t) and e′=e = approved. By inversion of T-Adjudicate, τ=Dτ= Outcome_D. By T-Approved, ∅⊢D:D _D approved: Outcome_D. The rule’s premises fix s′.=D(s.,a,t):Ds . domain= applyMutation_D(s. domain,a,t): State_D by the signature of D applyMutation_D (Definition A.1.3); s′.=s.++[approval entry]s . audit=s. audit\,+\!+\,[approval entry] has type (D) List( AuditEntry_D) by Definition A.1.9; s′.=s.s . queue=s. queue. Hence s′:Ds : FState_D. Case E-Adjudicate-Reject. e′e is rejected, of type D Outcome_D by T-Rejected. The rule leaves s.s. domain unchanged, appends a rejection audit entry, and preserves the queue; s′:Ds : FState_D. Case E-Adjudicate-Escalate. e′e is escalated, of type D Outcome_D by T-Escalated. The rule leaves s.s. domain unchanged, appends an escalation audit entry, and appends a pending proposal of type D PendingProposal_D (Definition A.1.9) to the queue; s′:Ds : FState_D. Case E-Entry. e=(v)e= entry(v) and e′=ve =v. By inversion of T-Entry, ∅⊢Dv:D _Dv: Outcome_D with τ=Dτ= Outcome_D, so ∅⊢De′:τ _De :τ. Framework state unchanged. Case E-Ctx. e=E[e1]e=E[e_1] and e′=E[e1′]e =E[e_1 ] with ⟨e1,s,ω⟩⟶⟨e1′,s′,ω′⟩ e_1,\,s,\,ω e_1 ,\,s ,\,ω by a sub-derivation. By Lemma A.2.5, there exists τ1 _1 with ∅⊢De1:τ1 _De_1: _1. By the inductive hypothesis on the sub-derivation, ∅⊢De1′:τ1 _De_1 : _1 and s′:Ds : FState_D. By Lemma A.2.5 again, ∅⊢DE[e1′]:τ _DE[e_1 ]:τ. Progress. Suppose ⟨e,s,ω⟩ e,\,s,\,ω is well-typed with ∅⊢De:τ _De:τ and e is not a value. We show that either a reduction applies or the configuration is operationally stuck on an undefined invocation of πAgentic Reduxπ Agentic Redux, κAgentic Reduxκ Agentic Redux, or an agent in Π . Proceed by structural induction on e. Case e=xe=x. Impossible: e is closed. Case e is a value. Excluded by hypothesis. Case e=x=e1e2e= let\;x=e_1\; in\;e_2. By inversion of T-Let, ∅⊢De1:τ1 _De_1: _1 for some τ1 _1. If e1e_1 is a value, E-Let applies. Otherwise, the inductive hypothesis on e1e_1 either supplies a step (lifted by E-Ctx with E=x=[⋅]e2E= let\;x=[·]\; in\;e_2) or an operational stuckness that the outer configuration inherits. Case e=e= coordinate. If πAgentic Redux(s,Π,ω)π Agentic Redux(s, ,ω) is defined (including every agent invocation it performs), E-Coordinate applies. Otherwise the configuration is operationally stuck on an undefined invocation of πAgentic Reduxπ Agentic Redux or of an agent in Π (Definitions A.1.6, A.1.12). Case e=(e1,e2)e= adjudicate(e_1,e_2). By inversion of T-Adjudicate, ∅⊢De1:D×D _De_1: Roles_D× Action_D and ∅⊢De2: _De_2: Time. • If e1e_1 is not a value: the IH on e1e_1 gives a step (lifted by E-Ctx with E=([⋅],e2)E= adjudicate([·],e_2)) or a stuckness. • If e1e_1 is a value and e2e_2 is not: the IH on e2e_2 gives a step (lifted by E-Ctx with E=(e1,[⋅])E= adjudicate(e_1,[·])) or a stuckness. • If both are values: by Lemma A.2.5, e1=(r,a)e_1=(r,a) for r∈Dr∈ Roles_D and a∈Da∈ Action_D, and e2=te_2=t for a timestamp t. If κAgentic Redux(s,a,t,ω)κ Agentic Redux(s,a,t,ω) is defined, its output falls in exactly one of the three mutually exclusive branches of Definition A.1.12, so exactly one of E-Adjudicate-Approve, E-Adjudicate-Reject, E-Adjudicate-Escalate applies. If undefined, the configuration is operationally stuck on κAgentic Reduxκ Agentic Redux. Case e=(e1)e= entry(e_1). By inversion of T-Entry, ∅⊢De1:D _De_1: Outcome_D. If e1e_1 is a value, E-Entry applies. Otherwise the IH on e1e_1 supplies a step (lifted by E-Ctx with E=([⋅])E= entry([·])) or a stuckness. This exhausts the cases of the structural induction, completing the proof. ∎ Remark A.60 (Scope of Type Safety). Theorem 3 is stated at scope D:D: DOMAIN because the Progress case for coordinate invokes πAgentic Reduxπ Agentic Redux and Π , which are defined only over domains carrying role structure (Definitions A.1.12, A.1.8). Type Safety therefore does not apply at Adjudicable scope: a domain lacking role structure has no coordinate primitive to type. The κAgentic Reduxκ Agentic Redux-based results (Theorem 1, Theorem 2, Corollary 1) do not share this restriction. A.3 The Counselor Queue Extension We extend the calculus of section A.1 with the machinery needed to formalise the Counselor Queue informally discussed in sections 3.1 and 4.2, and extend the metatheory of section A.2 to cover it. Two features of the base calculus carry the weight of the extension. The review queue is already part of the framework state (Definition A.1.9) and is populated by E-Adjudicate-Escalate; the extension activates an already-present data structure rather than introducing a new one. And the three-valued invariant result (Definition A.1.3) already distinguishes escalate from reject, so the per-invariant decision whether a failure admits human override is taken by the domain author at invariant-declaration time; no new escalation-trigger mechanism is needed. The extension is conservative: a domain that does not instantiate the extended signature yields a system identical to the one of section A.1.12, and the results of section A.2 apply to it unchanged. A.3.1 Definitions and Reduction Rules Definition A.61 (Signature Adjudicable+ Adjudicable^+). A structure D satisfies Adjudicable+ Adjudicable^+ iff it satisfies Adjudicable (Definition A.1.3) and, in addition, provides: • a type D: Counselor_D: Occ of counselor identities; • an authorisation predicate authorizedD:D→,authorized_D: Counselor_D→\ true, false\. An element c:Dc: Counselor_D with authorizedD(c)=authorized_D(c)= true is called a counselor. Remark A.62 (Policy authority, not type authority). The counselor may commit any sc:Ds_c: State_D, regardless of whether sc⊧Ds_c invariants_D, and regardless of which action’s escalation triggered the counselor’s involvement. The counselor’s state argument is well-typed — this is not an untyped escape hatch — but no kernel-level predicate filters it on policy grounds. Byzantine behaviour is explicitly out of scope; the counselor’s decisions are policy judgements, not adversarial inputs. Extended audit entries. The audit entry type is extended with two additional shapes. Definition A.63 (Extended audit entry). D+≜D+D+D AuditEntry_D^+\; \; AuditEntry_D\;+\; CommitEntry_D\;+\; RejectEntry_D, where D≜ CommitEntry_D\; \; ×D Id× Time×\ cCommitted\× Counselor_D ×D× × State_D× Id ×(×), × List( InvariantId× InvResult), D≜ RejectEntry_D\; \; ×D Id× Time×\ cRejected\× Counselor_D ×. × String× Id. The second Id field of each entry records the identifier of the originating escalation entry. The (×) List( InvariantId× InvResult) field of a CommitEntry is the detection vector: the kernel walks D invariants_D on the counselor-committed state scs_c and records, per invariant, the returned InvResult value. The detection vector is informational: the kernel does not use it to decide whether to commit, and its contents do not affect any reduction rule below. It exists so an auditor reviewing the log can mechanically identify counselor commits that did not preserve invariants, and so the harness has a programmatic signal on which to base operational recovery (cf. Remark A.3.1). Escalation–pending-proposal Id sharing. For the extension, we fix a convention implicit in the base calculus’s presentation of Step 3 of Definition A.1.12: the Id of the pending proposal appended to s.s. queue by E-Adjudicate-Escalate is the same as the Id of the escalation audit entry appended to s.s. audit by the same rule instance. This makes “the escalation entry associated with the current pending proposal” a well-defined phrase. Extended term language and typing. The term language gains one new constructor, awaitCounselor, and two new value forms, cCommitted and cRejected: e::=⋯∣,v::=⋯∣.e\;::=\;·s\; \; awaitCounselor, v\;::=\;·s\; \; cCommitted\; \; cRejected. Evaluation contexts are unchanged; awaitCounselor is atomic. The types gain one constant: τ::=⋯∣D,τ\;::=\;·s\; \; CounselorOutcome_D, with D≜, CounselorOutcome_D \ cCommitted, cRejected\. T-CCommitted :Γ⊢DcCommittedCounselorOutcomeD \> $ \ $ 80.93439pt $ _D cCommitted: CounselorOutcome_D$ T-CRejected :Γ⊢DcRejectedCounselorOutcomeD \> $ \ $ 75.52464pt $ _D cRejected: CounselorOutcome_D$ T-AwaitCounselor :Γ⊢DawaitCounselorCounselorOutcomeD \> $ \ $ 86.67052pt $ _D awaitCounselor: CounselorOutcome_D$ Freeze discipline on base rules. Each of the four architecture rules of section A.1.14 acquires one additional premise, s.=[]s. queue=[\,]. Writing the extended E-Coordinate rule explicitly to illustrate: E-Coordinate+ s.=queue[] =πAgentic Redux(s,Π,ω)(r,a) ⇒kω′ ⟶⟨coordinate,s,ω⟩⟨(r,a),s,ω′⟩ 125.0319pt $ s. queue=[\,]$ $ π Agentic Redux(s, ,ω)=(r,a)$ $ ω _kω $ 68.10237pt $ coordinate,\,s,\,ω (r,a),\,s,\,ω $ The premise s.=[]s. queue=[\,] is added verbatim to the three E-Adjudicate-* rules (section A.1.14); we write E-Adjudicate-Approve+, etc., for the resulting rules. All other premises and conclusions are unchanged. While s.≠[]s. queue≠[\,], the four base architecture rules do not fire; only the counselor rules below, the administrative rules E-Let and E-Entry, and the evaluation-context lift E-Ctx, remain available. Counselor reduction rules. The counselor consults the oracle. We write ω↝(,c,sc)ω ( cCommitted,c,s_c) to denote “the oracle’s next consumption supplies a counselor-commit directive with counselor identity c and committed state scs_c,” and analogously ω↝(,c,m)ω ( cRejected,c,m). E-Counselor-Commit s.=queue[p] ↝ω(cCommitted,c,sc) =authorizedD(c)true s′.=domainsc s′.=queue[] s′.audit=s.audit++[commit entry] ⇒kω′ ⟶⟨awaitCounselor,s,ω⟩⟨cCommitted,s′,ω′⟩ 108.16373pt $ s. queue=[p]$ $ ω ( cCommitted,c,s_c)$ $ _D(c)= true$ $ s . domain\;=\;s_c$ $ s . queue\;=\;[\,]$ $ s . audit\;=\;s. audit\,+\!+\,[\,commit entry\,]$ $ ω _kω $ 94.98141pt $ awaitCounselor,\,s,\,ω \; \; cCommitted,\,s ,\,ω $ E-Counselor-Reject s.=queue[p] ↝ω(cRejected,c,m) =authorizedD(c)true s′.=domains.domain s′.=queue[] s′.audit=s.audit++[reject entry] ⇒kω′ ⟶⟨awaitCounselor,s,ω⟩⟨cRejected,s′,ω′⟩ 103.87204pt $ s. queue=[p]$ $ ω ( cRejected,c,m)$ $ _D(c)= true$ $ s . domain\;=\;s. domain$ $ s . queue\;=\;[\,]$ $ s . audit\;=\;s. audit\,+\!+\,[\,reject entry\,]$ $ ω _kω $ 89.57169pt $ awaitCounselor,\,s,\,ω \; \; cRejected,\,s ,\,ω $ The “commit entry” appended by E-Counselor-Commit is the D CommitEntry_D value with counselor c, state scs_c, reference field p.p. id (the originating escalation entry’s Id, by the Id-sharing convention above), and detection vector [(id(ιk),ιk(sc))]ιk∈D[(id( _k), _k(s_c))]_ _k∈ invariants_D. The “reject entry” appended by E-Counselor-Reject is the D RejectEntry_D value with counselor c, reason m, and reference field p.p. id. The rules are mutually exclusive: the oracle’s next consumption either supplies a cCommitted-tagged directive or a cRejected-tagged one, not both. If s.=[]s. queue=[\,], neither rule’s first premise is satisfied and the configuration is stuck on awaitCounselor. If the oracle supplies an unauthorised counselor identity, neither rule’s third premise is satisfied and the configuration is stuck. Both forms of stuckness are intended; they are the awaitCounselor analogues of the operational stuckness of Theorem 3 on undefined invocations of πAgentic Reduxπ Agentic Redux, κAgentic Reduxκ Agentic Redux, or an agent. The extended architecture. Definition A.64 (+ AgenticRedux^+). For D:D: DOMAIN additionally satisfying Adjudicable+ Adjudicable^+, the Agentic Redux architecture with Counselor Queue over D is the architecture whose reduction rules are the four base architecture rules of section A.1.14 with the freeze premise s.=[]s. queue=[\,] added, together with E-Counselor-Commit and E-Counselor-Reject. We write +(D) AgenticRedux^+(D) for the resulting system. Lemma A.65 (Queue cardinality bound). For every initial framework state s0:Ds_0: FState_D with s0.=[]s_0. queue=[\,], every client program e0e_0 well-typed over +(D) AgenticRedux^+(D), and every oracle trace ω: every reachable configuration sjs_j in (e0,s0,ω) Exec(e_0,s_0,ω) satisfies |sj.|≤1|s_j. queue|≤ 1. Proof. Induction on j. The base case holds by hypothesis. For the inductive step, the only rule that extends the queue is E-Adjudicate-Escalate+, which appends one pending proposal and has premise sj.=[]s_j. queue=[\,], so |sj+1.|=1|s_j+1. queue|=1. The two counselor rules have premise sj.=[p]s_j. queue=[p] and set sj+1.=[]s_j+1. queue=[\,]. All other rules leave the queue unchanged, preserving the inductive hypothesis. ∎ Lemma A.66 (Extended audit append discipline). For every reduction step of +(D) AgenticRedux^+(D) ⟨e,s,ω⟩⟶⟨e′,s′,ω′⟩ e,\,s,\,ω e ,\,s ,\,ω : • if the step is an instance of E-Adjudicate-Approve+, E-Adjudicate-Reject+, E-Adjudicate-Escalate+, E-Counselor-Commit, or E-Counselor-Reject (possibly lifted through E-Ctx), then s′.=s.++[entry]s . audit=s. audit\,+\!+\,[\,entry\,] for exactly one entry, fixed by Definition A.1.12 for the three base rules and by section A.3.1 for the two counselor rules; • otherwise, s′.=s.s . audit=s. audit. Proof. The three E-Adjudicate-*+ cases inherit from Lemma A.1.14: the freeze premise restricts when the rules fire but does not alter their audit-appending conclusions. The two E-Counselor-* rules have explicit audit-append premises (section A.3.1), each appending exactly one entry. The remaining rules (E-Let, E-Entry, E-Coordinate+) carry the framework state through their conclusions syntactically. E-Ctx preserves both cases. ∎ Remark A.67 (Rule classification, extended). Each rule of +(D) AgenticRedux^+(D) is classified as in Remark A.1.14, by the shape of its conclusion’s domain clause: • the freeze-premised E-Adjudicate-Approve+ is applyMutation-applying; • E-Adjudicate-Reject+, E-Adjudicate-Escalate+, and E-Counselor-Reject are domain-preserving (each fixes s′.=s.s . domain=s. domain in its conclusion); • E-Let, E-Coordinate+, and E-Entry are domain-preserving (their conclusions leave s unchanged); • E-Counselor-Commit fits neither class: its conclusion fixes s′.=scs . domain=s_c for an oracle-supplied state scs_c that is in general distinct from both s.s. domain and any D applyMutation_D-image of it. Lemma A.1.14 therefore extends to +(D) AgenticRedux^+(D) for every step except those instantiating E-Counselor-Commit. By Lemma A.3.1, the phrase “the escalation entry associated with the current pending proposal” in the E-Counselor-* rules refers to a unique audit entry. A.3.2 Preservation of Base Results Theorems 1 and 3, Proposition 1, and Corollary 1 extend to + AgenticRedux^+ with small additions that exploit the parametric structure of their proofs. Theorem 2 (Audit Log Integrity) does not extend by the same pattern and is addressed separately in section A.3.3. All four results below presuppose the well-typed configurations of section A.1.13 extended to the new term forms, and the initial-queue hypothesis s0.=[]s_0. queue=[\,] needed for Lemma A.3.1. Theorem 1+ (Invariant Preservation under Safe Counselor Commits). For every D:D: DOMAIN additionally satisfying Adjudicable+ Adjudicable^+, every client program e0e_0 well-typed over +(D) AgenticRedux^+(D), every initial framework state s0s_0 of type D FState_D with s0.⊧Ds_0. domain invariants_D and s0.=[]s_0. queue=[\,], and every oracle trace ω∈Ωω∈ : if every step of (e0,s0,ω) Exec(e_0,s_0,ω) that is an instance of E-Counselor-Commit (possibly lifted through E-Ctx) produces a post-state sj+1s_j+1 with sj+1.⊧Ds_j+1. domain invariants_D, then every reachable domain state in (e0,s0,ω) Exec(e_0,s_0,ω) satisfies D invariants_D. Proof. The induction of the proof of Theorem 1 carries through; we add two cases to its inductive step. Case E-Counselor-Commit. By hypothesis, sj+1.⊧Ds_j+1. domain invariants_D. Case E-Counselor-Reject. The rule is domain-preserving (Remark A.3.1), so by Lemma A.1.14, sj+1.=sj.s_j+1. domain=s_j. domain. The inductive hypothesis gives sj+1.⊧Ds_j+1. domain invariants_D. This extends Case 1 of the proof of Theorem 1 to the new rule. The base cases (E-Adjudicate-Approve+ and everything else) are as in the proof of Theorem 1; the added freeze premise restricts when the base rules fire but does not alter their conclusions. ∎ Proposition 1+ (Agent Confinement, extended). Proposition 1 holds for +(D) AgenticRedux^+(D) verbatim. Proof. Part (i). The statement and proof depend only on the type signature of αr _r (Definition A.1.6), unchanged by the extension. A counselor is not an agent — the domain signature treats D Counselor_D and D Roles_D as disjoint sorts — so no counselor-related reduction rule is within the scope of the proposition. Part (i). E-Coordinate+ has the same conclusion ⟨(r,a),s,ω′⟩ (r,a),\,s,\,ω as E-Coordinate; the added freeze premise restricts when the rule fires but leaves its conclusion — and in particular the syntactic equality s′=s =s — unchanged. ∎ Corollary 1+ (Write Skew Freedom under Safe Counselor Commits). Under the hypotheses of Theorem 1+, (e0,s0,ω) Exec(e_0,s_0,ω) is not a write-skew execution (Definition A.2.3). Proof. Immediate from Theorem 1+, as in the proof of Corollary 1. ∎ Theorem 3+ (Type Safety, extended). For every D:D: DOMAIN additionally satisfying Adjudicable+ Adjudicable^+, every well-typed configuration over +(D) AgenticRedux^+(D) satisfies: • (Preservation) As in Theorem 3, with additional cases for the counselor rules. • (Progress) As in Theorem 3, with two additional forms of operational stuckness: an awaitCounselor term with s.=[]s. queue=[\,], and an awaitCounselor term for which the oracle’s next consumption supplies an unauthorised counselor identity. Proof. Preservation gains two cases. E-Counselor-Commit reduces :D awaitCounselor: CounselorOutcome_D to :D cCommitted: CounselorOutcome_D; the framework state components preserve their types by construction of the rule (Definition A.3.1). E-Counselor-Reject is analogous. Progress gains one case: e=e= awaitCounselor, of type D CounselorOutcome_D by T-AwaitCounselor. If s.=[p]s. queue=[p] and the oracle’s next consumption supplies an authorised counselor identity, exactly one of the two counselor rules applies, discriminated by the cCommitted vs. cRejected tag of the oracle directive. Otherwise, the configuration is operationally stuck. All other cases are as in the proof of Theorem 3. The added freeze premise on the four base architecture rules does not introduce a new class of stuckness: a configuration with e=e= coordinate or e=((r,a),t)e= adjudicate((r,a),t) and s.≠[]s. queue≠[\,] is stuck in the same sense that the base calculus admits — no rule applies — and this is the client’s signal to interpose an awaitCounselor term before further architecture-primitive activity. ∎ A.3.3 Extended Audit Log Integrity Theorem 2 (Audit Log Integrity) does not extend to +(D) AgenticRedux^+(D) by the parametric pattern used for the other base results. Two features of its statement explain why. First, Clauses (i) and (v) of Theorem 2 are rule-list claims: they name E-Adjudicate-Approve, E-Adjudicate-Reject, and E-Adjudicate-Escalate by name as the rules that append to the audit and under which per-step exactness holds. The extension introduces two further audit-appending rules, and the rule-list claims are structurally incomplete as stated. Second, Theorem 2 addresses a single commit-capable principal: the meta-agent, whose entries have the shape fixed by Definition A.1.9. The extension introduces a second commit-capable principal, the counselor, whose entries have a different shape (Definition A.3.1) and carry provenance information absent in the base: counselor identity, reference to the originating escalation entry, per-invariant detection vector on a post-hoc committed state. Multi-principal auditability additionally requires a trace-level property that Theorem 2 does not assert: every counselor entry in the log is the resolution of an escalation entry earlier in the log. This is the property that makes the extended log auditable in the operational sense — every counselor action can be traced back to the adjudication that occasioned it. We therefore state the extended auditability result as a new theorem. The base Theorem 2 remains valid for the subset of reduction rules it addresses; Theorem 4 covers the full rule set of +(D) AgenticRedux^+(D) and adds the provenance-chaining property. Theorem 4 (Extended Audit Log Integrity). For every D:D: DOMAIN additionally satisfying Adjudicable+ Adjudicable^+, every client program e0e_0 well-typed over +(D) AgenticRedux^+(D), every initial framework state s0s_0 of type D FState_D with s0.=[]s_0. queue=[\,], and every oracle trace ω∈Ωω∈ , the execution (e0,s0,ω) Exec(e_0,s_0,ω) satisfies: (i)–(i) Kernel-path faithful entries. Clauses (i) and (i) of Theorem 2 hold verbatim, with the E-Adjudicate-* rules replaced by their freeze-premised counterparts E-Adjudicate-*+. (i+) Exclusivity of provenance. For every reduction step that is not an instance of any of E-Adjudicate-Approve+, E-Adjudicate-Reject+, E-Adjudicate-Escalate+, E-Counselor-Commit, or E-Counselor-Reject (possibly lifted through E-Ctx): sj+1.=sj.s_j+1. audit=s_j. audit. (iv) Append-only monotonicity. For every reduction step in the execution, sj.s_j. audit is a prefix of sj+1.s_j+1. audit. (v+) Per-step exactness. For every reduction step that is an instance of any of the five rules listed in Clause (i+) (possibly lifted through E-Ctx): |sj+1.|=|sj.|+1|s_j+1. audit|=|s_j. audit|+1. (vi) Faithful counselor-commit entries. For every step that is an instance of E-Counselor-Commit (possibly lifted through E-Ctx) with oracle consumption (,c,sc)( cCommitted,c,s_c) and pending proposal p: the sole entry appended to sj+1.s_j+1. audit is a D CommitEntry_D with tag cCommitted, counselor c, committed state scs_c, escalation-reference p.p. id, and detection vector [(id(ιk),ιk(sc))]ιk∈D[(id( _k), _k(s_c))]_ _k∈ invariants_D; and authorizedD(c)=authorized_D(c)= true. (vii) Faithful counselor-reject entries. For every step that is an instance of E-Counselor-Reject (possibly lifted through E-Ctx) with oracle consumption (,c,m)( cRejected,c,m) and pending proposal p: the sole entry appended to sj+1.s_j+1. audit is a D RejectEntry_D with tag cRejected, counselor c, reason m, and escalation-reference p.p. id; and authorizedD(c)=authorized_D(c)= true. (viii) Escalation–resolution chaining. For every audit entry of tag cCommitted or cRejected in sj.s_j. audit for any j: the entry’s escalation-reference field is the Id of a unique earlier audit entry in sj.s_j. audit of tag escalated, and no other counselor entry in the entire execution shares that escalation-reference value. Equivalently: every escalated entry in the execution is referenced by at most one counselor entry. Proof. Fix a reduction step ⟨ej,sj,ωj⟩⟶⟨ej+1,sj+1,ωj+1⟩ e_j,\,s_j,\, _j e_j+1,\,s_j+1,\, _j+1 of the execution, derived from a primitive rule possibly lifted through E-Ctx. Clauses (i)–(i). Inherited from Theorem 2. The proofs refer to each rule’s premises and to Lemmas A.1.14 and A.1.14; none of these is altered by the extension, and the added freeze premise does not change the approval, rejection, or escalation branches’ conclusions. Clauses (i+)–(v+). Immediate from Lemma A.3.1: its audit-appending branch fixes sj+1.=sj.++[entry]s_j+1. audit=s_j. audit\,+\!+\,[\,entry\,] for exactly one entry, supplying the prefix property of Clause (iv) and the cardinality identity of Clause (v+); the complementary branch supplies Clause (i+) and the trivial-prefix case of Clause (iv). Clause (vi). E-Counselor-Commit’s premises fix sj+1.=sj.++[commit entry]s_j+1. audit=s_j. audit\,+\!+\,[\,commit entry\,], where the commit entry’s shape is fixed by Definition A.3.1: tag cCommitted, counselor c from the oracle consumption, committed state scs_c from the oracle consumption, detection vector computed by the kernel on scs_c (section A.3.1), and escalation-reference p.p. id where p is the pending proposal of the rule’s first premise. The authorisation condition authorizedD(c)=authorized_D(c)= true is an explicit premise of the rule. Clause (vii). Analogous, substituting E-Counselor-Reject and D RejectEntry_D. Clause (viii). We argue by induction on j. Base case (j=0j=0). s0.=[]s_0. audit=[\,] (no rule has yet fired); the claim holds vacuously. Inductive step. Suppose the claim holds for sjs_j. Consider the reduction sj→sj+1s_j→ s_j+1 by rule R. If R is not an audit-appending rule, sj+1.=sj.s_j+1. audit=s_j. audit by Clause (i+), and the claim persists. If R is E-Adjudicate-Approve+ or E-Adjudicate-Reject+, the appended entry is tagged approved or rejected. No counselor entry is added, and no new escalated entry is added, so the claim persists. If R is E-Adjudicate-Escalate+, the appended entry is a fresh escalated entry. No counselor entry has been appended at this step, so the new escalation entry has zero resolvers in sj+1.s_j+1. audit. All previously existing escalated entries retain their resolver counts. All previously existing counselor entries still reference the same (unchanged) escalated entries. The claim persists. If R is E-Counselor-Commit or E-Counselor-Reject, the appended entry is a counselor entry with escalation-reference p.p. id, where p=sj.(0)p=s_j. queue(0). By Lemma A.3.1 and the Id-sharing convention (section A.3.1), p.p. id is the Id of the unique escalated entry in sj.s_j. audit whose appending populated the queue with its current element. That escalated entry has no other counselor resolver in sj.s_j. audit: any such prior resolver would have emptied the queue in its step (Lemma A.3.1), after which the only way the current p could be in sj.s_j. queue is for a subsequent E-Adjudicate-Escalate+ step to have appended it, producing a different escalation entry with a different Id. Hence the new counselor entry’s escalation-reference is the first such reference in the execution, and the claim persists. This completes the induction. ∎ Remark A.68 (Linear auditability restored). Clauses (i+)–(v+) of Theorem 4 make precise the “linearly in time” claim of section 1.3.2 for the extended system: the audit log grows by exactly one entry per commit-rule step — kernel or counselor — from no other reduction rule, and existing entries are never modified. Clause (viii) adds the trace-level provenance that multi-principal auditability requires: every counselor action in the log points back to a unique adjudication step earlier in the log, and no escalation is resolved twice. Remark A.69 (Detection-vector auditability). Clause (vi) establishes that every cCommitted entry records the kernel’s evaluation of D invariants_D on the counselor-committed state. A human auditor reviewing the log can therefore identify, mechanically, every counselor commit that did not preserve invariants — an entry is invariant-preserving iff every InvResult in its detection vector is pass. This is the formal hook on which an operational recovery protocol in the harness can be built (cf. Remark A.3.1), and it is what makes the conditional hypothesis of Theorem 1+ effective: counselor-compliance violations are not only real but visibly real in the log.