ISDAIRE: A Formal Specification and Admissibility Framework for Executable Governance of Agentic AI Systems

As AI systems move from bounded recommendation into execution-bearing agenticarchitectures, the primary governance problem changes. The central difficulty is no longeronly whether a model can generate a plausible output. It is whether an action class has beenspecified with enough precision, authority binding, and boundary discipline to make runtimeenforcement meaningful at the point of irreversibility. Prior work on executable governanceformalised execution-boundary control and deterministic binding to the earliest governedirreversible execution boundary, but it did not claim to solve the separate problem of howadmissible action classes should be constructed ex ante 1, 2. This paper addresses that gap.The paper introduces ISDAIRE as a formal specification and admissibility frameworkfor governed action classes in agentic systems. ISDAIRE is presented not as a runtimecontrol surface and not as a universal safety architecture, but as the ex-ante specificationlayer that defines whether an action class has been specified strongly enough for executablegovernance. The framework is expressed through formal artefacts for intent, scope, domainseparation, authority source, irreversibility awareness, risk framing, and execution-boundarydefinition, together with explicit condition sets, dependency declarations, version binding,and review obligations. A domain synthesis function is introduced to map domain semanticsinto governed specification artefacts. To preserve consistency with OTANIS, the paperretains the canonical class-level admissibility predicate AdmissibleISDAIRE(𝛼) and introducesa narrower auxiliary predicate, StructuralAdmissible(𝛼), for the weaker property that thegoverned specification object is well formed, internally consistent, and authority bound.A stronger deployment-side predicate, AutonomousAdmissible(𝛼), is then reserved for caseswhere boundary completeness also holds. This paper does not claim that any of thesepredicates alone establishes semantic adequacy, safety, legal sufficiency, or deploymentacceptability. The paper distinguishes syntactic completeness from semantic adequacy. It argues thatruntime enforcement can only be as sound as the specification artefacts it is given, andthat omitted dependencies, omitted precursor boundaries, stale authority assumptions, orsemantically weak action classes remain design failures even when runtime enforcementis correct. A worked insurance payout example demonstrates how ISDAIRE constructsa governed action class for claim settlement, and how failures in boundary definition,dependency declaration, or authority binding propagate into execution risk. The paperpositions ISDAIRE as the formal admissibility layer beneath OTANIS and MGAG, whilealso introducing a narrower auxiliary predicate for specification-object soundness and astronger deployment-side qualification for autonomous execution. In that form, it providesa more defensible basis for specification, review, procurement qualification, and audit ofexecution-bearing agentic systems.