1 Introduction↩︎

AI workflow systems compose language model calls with data retrieval, code execution, and external API access. Governance of these systems currently takes two forms. Behavioral approaches (RLHF [1], constitutional AI [2], guardrails [3]) train or filter model outputs but do not address whether the system’s effects (API calls, file writes, tool invocations) pass through any governance boundary. Structural approaches enforce invariants at the execution layer, but existing formalizations either lack machine-checked proofs or do not address composition: they verify individual programs rather than establishing that governance is closed under the system’s composition operators.

This paper develops an algebraic semantics for governed execution: a framework in which governance is axiomatized as a three-property algebra, compositional under all program combinators, and, within the formalized execution model, coterminous with expressibility. The central thesis is:

Governance, when formalized as an algebraic structure over interaction trees, induces compositional properties on programs, effects, and capabilities such that the governed fragment coincides with the expressible fragment in the modeled substrate.

1.0.0.1 Relationship to prior work in this line.

Prior papers in this line establish structural governance at the architectural level [4], expressive completeness via four primitives [5], and machine-checked safety proofs for the specific runtime [6]. The present paper abstracts and unifies those system-specific results into an algebraic semantics. The GovernanceAlgebra axiomatization lifts safety theorems to parametric results that hold for any system satisfying three axioms. The monoidal, effect, and capability layers explain why the system’s programs compose under governance, not just why individual programs are safe. Two companion papers address practical enforcement: [7] discharges the pure module constraint assumed by the safety theorems, replacing convention-based enforcement with WASM compilation and cryptographic purity certificates; [8] extends the governance boundary to the supply chain with dual-signature distribution provenance.

1.0.0.2 Three levels of “governed.”

We distinguish three levels that the paper addresses:

1. Syntactic expressibility: a program is constructible from the four primitive morphisms (code, reason, memory, call) via composition in category \(\mathbf{Mashin}\).

2. Semantic governance under interpretation: interpreting a program through the governance operator \(\mathcal{G}\) yields a tree satisfying the coinductive gov_safe predicate.

3. Trace-level evidence: the execution trace extracted from a governed program is well-governed (every I/O event preceded by a governance check) and maps to a tamper-evident ledger.

The coterminous boundary result connects levels 1 and 2: every syntactically expressible program is semantically governed under interpretation. Level 3 is a derived consequence (Section 7).

1.0.0.3 Contributions.

The paper makes four contributions, each mechanized in Rocq:

1. GovernanceAlgebra and monoidal structure (Sections 3–4). A three-axiom parametric record from which convergence, compositional closure, and goal preservation are derived. Category \(\mathbf{Mashin}\) admits a symmetric monoidal structure with verified pentagon, triangle, and hexagon coherence. All tensor compositions preserve governance.

2. Governed algebraic effects (Section 5). An algebraic effect system in which the handler algebra is constrained: only handlers carrying a machine-checked safety certificate (GovernedHandler) can be constructed in the governed fragment. The No Ambient Effects theorem proves that programs in the empty capability set emit only observability directives.

3. Capability-indexed composition with dual guarantee (Section 6). CapMorphisms bundle programs with capability bounds verified by a trust lattice. Composition operators (sequential, tensor, branch) preserve bounds. The dual guarantee establishes that within_caps and gov_safe hold simultaneously.

4. Coterminous boundary (Section 8). Within the formalized execution model, every expressible program is governed, and every governed program is the image of an expressible program. Turing completeness is preserved inside governance. Unmediated I/O is excluded from the governed fragment.

Section 7 derives trace semantics and ledger connection as consequences of the algebraic framework. Section 9 discusses mechanization and extraction to OCaml. Section 10 positions the work relative to prior results on algebraic effects, monoidal categories, and verified systems.

1.0.0.4 What is novel.

The individual ingredients (monoidal categories, algebraic effects, coinductive predicates, capability systems) are well-established. To our knowledge, this is the first mechanized framework combining governance-constrained interpretation, capability-bounded algebraic effects, and a coterminous expressibility/governance theorem over an interaction-tree-based execution model. The GovernanceAlgebra axiomatization is parametric: the derived theorems hold for any system satisfying three axioms, not only the concrete system we instantiate.

1.0.0.5 The Interaction Trees framework.

All formalizations use the Interaction Trees library [9], which represents programs as coinductive trees with three node types: pure values (\(\mathrm{Ret}\)), silent steps (\(\mathrm{Tau}\)), and visible events (\(\mathrm{Vis}\)). The governance pipeline transforms trees of directive events (\(\mathrm{DirectiveE}\)) into trees of governed events (\(\mathrm{GovIOE}\)). Coinductive properties are proved using the paco library [10] for parameterized coinduction.

2 Background↩︎

2.1 Interaction Trees↩︎

An interaction tree \(\mathrm{itree}\;E\;R\) is a potentially infinite tree coinductively defined by three constructors: \[\begin{align} \mathrm{Ret}(r) &\quad \text{pure value of type } R \\ \mathrm{Tau}(t) &\quad \text{silent computation step} \\ \mathrm{Vis}(e, k) &\quad \text{event } e : E\;X, \text{ continuation } k : X \to \mathrm{itree}\;E\;R \end{align}\]

Interaction trees form a monad: \(\mathrm{ret}\) injects values and \(\mathbin{>\!\!>\!\!=}\) sequences computations. Interpretation via handlers \(h : \forall X.\; E\;X \to \mathrm{itree}\;F\;X\) transforms \(\mathrm{itree}\;E\;R\) into \(\mathrm{itree}\;F\;R\). Equivalence is eutt (equivalence up to taus): two trees are equivalent if they produce the same visible events and return values, ignoring silent steps.

2.2 The Directive Type↩︎

The system’s effect signature is \(\mathrm{DirectiveE}\), an inductive type with 14 constructors covering all external capabilities:

Inductive DirectiveE : Type -> Type :=
  | LLMCall : LLMCallParams -> DirectiveE LLMResponse
  | HTTPRequest : HTTPRequestParams -> DirectiveE HTTPResponse
  | FileOp : FileOpParams -> DirectiveE FileResult
  | CallMachine : CallMachineParams -> DirectiveE CallMachineResult
  | MemoryOp : MemoryOpParams -> DirectiveE MemoryResult
  | DBOp : DBOpParams -> DirectiveE DBResult
  | ExecOp : ExecOpParams -> DirectiveE ExecResult
  | RecordStep : RecordStepParams -> DirectiveE unit
  | Broadcast : BroadcastParams -> DirectiveE unit
  | EmitEvent : EmitEventParams -> DirectiveE unit
  | GraphQLRequest : GraphQLRequestParams -> DirectiveE HTTPResponse
  | WebSocketOp : WebSocketOpParams -> DirectiveE WebSocketResult
  | MCPCall : MCPCallParams -> DirectiveE CallMachineResult
  | Observability : string -> DirectiveE unit.

The governed event type layers governance checks over I/O: \(\mathrm{GovIOE}= \mathrm{GovE}+ \mathrm{IOE}\), where \(\mathrm{GovE}\) carries governance stage checks and \(\mathrm{IOE}\) carries actual I/O events.

2.3 The Governance Operator↩︎

The operator \(\mathcal{G}: \mathrm{base\_handler} \to \mathrm{governed\_handler}\) wraps a base handler with governance checks. Before each I/O operation, \(\mathcal{G}\) emits a \(\mathrm{GovCheck}\) event; only if governance approves does the handler proceed. The key property is the coinductive safety predicate \(\texttt{gov\_safe}\):

The fundamental safety theorem, proved in prior work [6]:

2.4 Category \(\mathbf{Mashin}\)↩︎

The category \(\mathbf{Mashin}\) has types as objects and Kleisli arrows \(A \to \mathrm{itree}\;\mathrm{DirectiveE}\;B\) as morphisms. Identity is \(\mathrm{ret}\), composition is monadic bind (\(\mathbin{>\!\!>\!\!=}\)). Four primitive morphism constructors generate all programs:

• \(\mathrm{\small code}(f) : A \to B\) – pure computation, \(\mathrm{ret}(f(a))\)

• \(\mathrm{\small reason}(\mathrm{build}, \mathrm{extract}) : A \to B\) – LLM inference

• \(\mathrm{\small memory}(\mathrm{build}, \mathrm{extract}) : A \to B\) – semantic storage

• \(\mathrm{\small call}(\mathrm{build}, \mathrm{extract}) : A \to B\) – machine invocation

Category laws (identity, associativity) hold up to eutt, proved in Category.v [6].

3 Governance Algebra↩︎

The central abstraction is a three-axiom record that captures what it means to be a governance operator.

The three axioms are independent. Safety does not imply transparency: an operator could alter permitted results. Transparency does not imply safety: an operator could be transparent without wrapping I/O with governance checks. Properness is orthogonal to both.

From these three axioms, we derive:

This follows because \(\mathrm{machine\_at\_level}\;n\;R\) is definitionally \(\mathrm{itree}\;\mathrm{DirectiveE}\;R\) for all \(n\), so G1 applies directly. Governance holds uniformly across the meta-recursive tower.

The positive direction follows from G1. The negative direction follows from \(\texttt{bare\_io\_not\_safe}\): bare I/O nodes in the governed tree violate gov_safe because no governance check has approved them. This is a property of the gov_safe predicate, independent of any particular operator. The asymmetry is a theorem about the formal model: structural governance (effect mediation via \(\mathcal{G}\)) provides a guarantee that output-oriented controls alone cannot replicate within this framework, because output controls do not address the governance-check structure of the interaction tree.

This follows from G2 (transparency): permissive governance erases the governance events and preserves the base handler’s semantics.

3.0.0.1 Instantiation.

The concrete Mashin operator \(\mathcal{G}\) instantiates the record:

Definition mashin_governance : GovernanceAlgebra :=
  mk_gov_algebra Gov
    governed_interp_safe     (* G1 from Safety.v    *)
    governed_transparency    (* G2 from Transparency.v *)
    Gov_base_proper.         (* G3 from Functor.v   *)

All derived properties immediately apply to \(\mathcal{G}\). The algebra-level theorems (any_governance_algebra_subsumes, any_governance_algebra_converges, any_governance_algebra_preserves_goals) establish these properties for any operator satisfying the three axioms.

4 Enriched Monoidal Category↩︎

We extend category \(\mathbf{Mashin}\) with symmetric monoidal structure.

4.1 Tensor Product↩︎

Given morphisms \(f : A \to \mathrm{itree}\;\mathrm{DirectiveE}\;B\) and \(g : C \to \mathrm{itree}\;\mathrm{DirectiveE}\;D\), the tensor product \(f \otimes g : (A \times C) \to \mathrm{itree}\;\mathrm{DirectiveE}\;(B \times D)\) is defined as sequential-independent composition:

Definition mashin_tensor {A B C D}
  (f : mashin_morphism A B)
  (g : mashin_morphism C D)
  : mashin_morphism (A * C) (B * D) :=
  fun p =>
    let (a, c) := p in
    ITree.bind (f a) (fun b =>
    ITree.bind (g c) (fun d =>
    ret (b, d))).

The two computations share no state; \(f\)’s effects complete before \(g\)’s begin. This is not true concurrent interleaving, which would require a more complex construction (noted as future work in Section 11).

4.2 Structural Morphisms↩︎

The unit object is \(\mathrm{unit}\). Structural isomorphisms are all pure (no effects):

• Associator \(\alpha : (A \otimes B) \otimes C \xrightarrow{\sim} A \otimes (B \otimes C)\)

• Left unitor \(\lambda : I \otimes A \xrightarrow{\sim} A\)

• Right unitor \(\rho : A \otimes I \xrightarrow{\sim} A\)

• Braiding \(\sigma : A \otimes B \xrightarrow{\sim} B \otimes A\)

Each isomorphism is verified by round-trip lemmas (assoc_iso_lr/assoc_iso_rl, lunit_iso_lr/lunit_iso_rl, runit_iso_lr/runit_iso_rl, braid_iso).

4.3 Coherence Conditions↩︎

All three proofs proceed by unfolding definitions and applying bind_ret_l repeatedly, since the structural morphisms are pure. The proofs are short (under 10 lines each) precisely because purity makes coherence computational rather than coinductive.

4.4 Governance of Tensor Compositions↩︎

5 Algebraic Effects with Governed Handlers↩︎

Standard algebraic effect systems [11], [12] define handlers that interpret effects freely: any function of the right type is a valid handler. In our framework, the governed fragment admits only handlers that carry a machine-checked proof of safety preservation. This is not merely a matter of record packaging; it is a semantic exclusion. A handler that performs I/O without emitting governance checks cannot inhabit the GovernedHandler type, because its interpretation would produce trees violating gov_safe, and the required proof obligation cannot be discharged.

5.1 Capability Sets↩︎

A capability set is a characteristic function \(\mathrm{CapSet}= \mathrm{Capability} \to \mathrm{bool}\) with standard operations:

Definition cap_empty : CapSet := fun _ => false.
Definition cap_singleton (c : Capability) : CapSet :=
  fun c' => cap_eqb c c'.
Definition cap_union (s1 s2 : CapSet) : CapSet :=
  fun c => s1 c || s2 c.
Definition cap_full : CapSet := fun _ => true.

\((\mathrm{CapSet}, \subseteq)\) forms a bounded partial order with \(\emptyset\) as bottom and \(\mathrm{cap\_full}\) as top. Union is join: \(\cap\) is idempotent (cap_union_idem), commutative (cap_union_comm), and associative (cap_union_assoc).

5.2 The within_caps Predicate↩︎

This uses paco1 (parameterized coinduction with one parameter) since the capability set is fixed during the coinduction.

5.3 Primitive Capability Profiles↩︎

Each primitive has a tight capability bound:

5.4 Compositional Closure↩︎

The proof uses pcofix (parameterized coinduction) with case analysis on \(\mathrm{observe}(t)\). The \(\mathrm{Ret}\) case applies weakening from \(\mathrm{caps}_2\) to \(\mathrm{caps}_1 \cup \mathrm{caps}_2\). The \(\mathrm{Vis}\) case applies directive_in_caps_mono for the directive and the coinductive hypothesis for the continuation.

5.5 No Ambient Effects↩︎

A program within the empty capability set can only emit observability directives. It cannot perform LLM calls (llm_not_in_empty), HTTP requests (http_not_in_empty), machine calls (call_not_in_empty), or any other effectful action. This is the algebraic characterization of the “no ambient effects” property: effect capability is not ambient but must be structurally present in the program’s capability set.

5.6 Governed Handlers↩︎

Record GovernedHandler := mk_governed_handler {
  gh_handler : base_handler;
  gh_safe : forall R (t : itree DirectiveE R),
    @gov_safe R false (interp (Gov gh_handler) t)
}.

Handler equivalence (\(\mathrm{gh\_equiv}\)) is an equivalence relation (reflexive, symmetric, transitive). Both \(\mathrm{Gov\_endo}\) and \(\mathrm{Gov\_iter}\) preserve this equivalence (Gov_endo_preserves_gh_equiv, Gov_iter_preserves_gh_equiv).

The structural difference from standard algebraic effect systems [11], [13] is that those systems impose no constraint on what a handler does with an effect. Here, the GovernedHandler record requires a proof that interpretation through \(\mathcal{G}\) satisfies gov_safe. Handlers lacking this proof cannot be used in governed composition. The handler algebra is thus closed under governance-preserving operations but excludes handlers that would bypass governance checks.

6 Capability-Indexed Composition↩︎

6.1 Trust Lattice↩︎

Trust levels form a bounded total order with six elements: \[\mathrm{Untrusted} < \mathrm{Tested} < \mathrm{Evaluated} < \mathrm{Reviewed} < \mathrm{Stdlib} < \mathrm{System}\]

Definition trust_le (t1 t2 : TrustLevel) : Prop :=
  trust_value t1 <= trust_value t2.

The order is reflexive (trust_le_refl), transitive (trust_le_trans), antisymmetric (trust_le_antisym), and total (trust_le_total). \(\mathrm{Untrusted}\) is the bottom (trust_bottom), \(\mathrm{System}\) is the top (trust_top).

Join and meet are computed by comparison of trust values:

Definition trust_max (t1 t2 : TrustLevel) : TrustLevel :=
  if Nat.leb (trust_value t1) (trust_value t2) then t2 else t1.
Definition trust_min (t1 t2 : TrustLevel) : TrustLevel :=
  if Nat.leb (trust_value t1) (trust_value t2) then t1 else t2.

6.2 CapMorphisms↩︎

A \(\mathrm{CapMorphism}\) bundles a morphism with its capability requirement and a proof that the morphism stays within those capabilities:

Record CapMorphism (A B : Type) := mk_cap_morphism {
  cm_morph  : mashin_morphism A B;
  cm_caps   : CapSet;
  cm_within : forall a, within_caps cm_caps (cm_morph a)
}.

The four primitives yield canonical CapMorphisms:

6.3 Composition of CapMorphisms↩︎

6.3.0.1 Sequential composition.

\(\mathrm{cap\_seq\_compose}(f, g)\) has capabilities \(\mathrm{caps}(f) \cup \mathrm{caps}(g)\), following from bind_within_caps.

6.3.0.2 Tensor composition.

\(\mathrm{cap\_tensor}(f, g)\) has capabilities \(\mathrm{caps}(f) \cup \mathrm{caps}(g)\).

6.3.0.3 Branch composition.

\(\mathrm{cap\_branch}(\mathrm{pred}, f, g)\) has capabilities \(\mathrm{caps}(f) \cup \mathrm{caps}(g)\), since either branch may execute.

6.4 Capability Preservation↩︎

Both follow from the algebraic properties of \(\cup\) on CapSets (identity and idempotence).

6.5 Trust-Capability Connection↩︎

The function \(\mathrm{allowed\_cap\_set}(\mathrm{tl}, \mathrm{declared})\) converts a trust level and declared capability list to a CapSet:

6.6 Principal Capabilities↩︎

6.7 The Dual Guarantee↩︎

Capabilities tell you what the program can do; governance ensures it passes through governance checks before doing it. These are independent properties that hold simultaneously. The dual guarantee is preserved by tensor (tensor_dual_guarantee) and sequential composition (seq_dual_guarantee).

7 Trace Semantics and Ledger Connection↩︎

The preceding sections establish governance at the program level (coinductive gov_safe on interaction trees) and the capability level (within_caps on programs). This section derives the trace-level consequences: governed execution produces well-governed traces that map to tamper-evident ledger entries.

7.1 Trace Events and Extraction↩︎

Execution produces a finite trace of governance and I/O events:

Inductive TraceEvent :=
  | TE_GovCheck : GovernanceStage -> bool -> TraceEvent
  | TE_IO : string -> TraceEvent.

The inductive relation \(\mathrm{trace\_of}(t, \mathrm{trace}, r)\) extracts a trace from a governed computation, with constructors for return (empty trace), tau (transparent), governance checks (recorded), and I/O events (recorded).

Traces compose under monadic bind: the trace of a sequential composition is the concatenation of the component traces. The proof proceeds by induction on the derivation of \(\mathrm{trace\_of}\), using \(\mathrm{unfold\_bind}\) and \(\mathrm{bisimulation\_is\_eq}\) at each case.

7.2 Well-Governed Traces↩︎

The empty trace is governed (well_governed_nil). A governance check preserves the property (well_governed_gov_only). A passing check followed by I/O is governed (well_governed_gov_then_io).

7.3 Hash-Chained Ledger↩︎

The LedgerConnection module, parameterized over an abstract hash type and injective hash function, connects traces to tamper-evident ledger entries. The abstraction assumes an ideal injective hash; connecting this to a concrete cryptographic hash function (collision resistance rather than injectivity) requires additional formalization outside the scope of this paper.

Record LedgerEntry := mk_ledger_entry {
  le_event     : TraceEvent;
  le_data      : EventData;
  le_prev_hash : Hash;
  le_hash      : Hash;
}.

The proof follows from injectivity of the hash function and injectivity of event encoding.

The ledger records exactly the trace events, with no omissions and no additions (trace_to_ledger_events).

8 The Coterminous Boundary↩︎

The algebraic capstone combines all preceding results into a single record and theorem.

8.0.0.1 Precise statement of \(E = G\).

We define two sets relative to the formalized execution model:

• \(E\) (expressible): programs constructible from the four primitive morphisms (code, reason, memory, call) via composition in category \(\mathbf{Mashin}\). These are interaction trees of type \(\mathrm{itree}\;\mathrm{DirectiveE}\;R\).

• \(G\) (governed): programs \(t\) such that for all handlers \(h\), \(\texttt{gov\_safe}(\mathrm{false}, \mathrm{interp}(\mathcal{G}(h), t))\).

The coterminous boundary theorem establishes \(E = G\): every expressible program is governed under interpretation, and every governed program is the image of an expressible program under \(\mathcal{G}\). This is a theorem about the modeled execution substrate, not a universal claim about all possible governance mechanisms or all possible programming languages.

8.1 The CoterminousRecord↩︎

8.2 Boundary Equivalence↩︎

The inclusion \(E \subseteq G\) says governance never fails to apply. The inclusion \(G \subseteq E\) follows from the construction: \(\mathcal{G}\) takes \(\mathrm{DirectiveE}\) programs as input; every governed program is the image of an expressible program.

8.3 Conservative Denial↩︎

When governance denies a request, the computation diverges (non-termination). This is one conservative realization of denial: it produces no result at all, rather than an error value or an incorrect result. Alternative designs could model denial as an explicit error effect or a timeout; we chose divergence because it composes cleanly in the coinductive framework (a divergent sub-computation does not corrupt the enclosing computation’s safety properties) and avoids introducing a denial-specific effect constructor. The tradeoff is that divergence complicates refinement arguments and may obscure denial outcomes in practice; the runtime system detects denial via timeout rather than relying on the formal divergence semantics.

8.4 Trace-Level Properties↩︎

The coterminous boundary extends to traces: gov_safe_implies_governed_traces establishes that governed execution produces well-governed traces at the trace level, and gov_check_trace_governed shows that governance checks preserve the well-governed property.

8.5 Algebraic Characterization↩︎

\(\mathcal{G}\) is an endofunctor (Functor.v: Gov_is_endofunctor) that wraps programs with governance. Under permissive governance (all checks pass), governed interpretation is observationally equivalent to ungoverned interpretation (G2, transparency). The gov_permissive_preserves_expressiveness theorem confirms that governance does not reduce the set of expressible computations within the model.

Combined with the dual guarantee (Theorem 21), we obtain the complete picture:

9 Mechanization and Extraction↩︎

9.1 Rocq Development↩︎

The mechanization spans 36 modules ( 12,000 lines) with 454 theorems and zero admitted lemmas. Table 1 summarizes the development.

The dependency structure is layered: foundation modules have no upstream dependencies within the project; each phase builds only on earlier phases. The build takes approximately 45 seconds on a modern laptop.

9.2 Key Proof Techniques↩︎

9.2.0.1 Parameterized coinduction.

The gov_safe and within_caps predicates use paco (paco2 for the two-parameter gov_safe, paco1 for the one-parameter within_caps). The key insight is that the monotonicity lemma (gov_safe_mon, within_caps_mon) enables compositional coinductive reasoning: once proved for the generating functor, the coinductive predicate inherits all properties automatically.

9.2.0.2 Computational coherence.

The pentagon, triangle, and hexagon proofs are each under 10 lines because the structural morphisms are pure: they unfold to \(\mathrm{ret}(\ldots)\), and \(\mathrm{bind}(\mathrm{ret}(x), k)\) reduces to \(k(x)\) by bind_ret_l. Coherence is verified by computation rather than diagram chasing.

9.2.0.3 Dependent destruction.

The bind_within_caps proof requires \(\mathrm{dependent\;destruction}\) on the within_capsF inversion in the \(\mathrm{Vis}\) case, because the directive type \(X\) is existentially quantified in the tree constructor.

9.3 Extraction to OCaml↩︎

Modules with computational content in \(\mathrm{Type}\) or \(\mathrm{Set}\) are extracted to OCaml using Rocq’s extraction mechanism [14], [15]:

The InterpreterSpec module uses Rocq Section variables for the hash type, extracting as an OCaml functor parameterized over a hash signature. The functor is instantiated with a SHA-256 implementation.

The extracted OCaml is compiled to a shared library and linked as a NIF (Native Implemented Function) into the BEAM runtime, with a fallback to the Elixir implementation if the NIF is unavailable.

9.4 Three-Layer Testing↩︎

The system uses three-layer testing:

1. OCaml unit tests: Edge cases on extracted functions, comparing against Compute output from Rocq.

2. NIF round-trip tests: Exhaustive comparison between the NIF and the Elixir implementation for all trust/capability combinations.

3. Three-way property tests: The property-based testing framework generates 70,000+ random directive sequences and verifies agreement among: (a) the Rocq-extracted NIF, (b) the Elixir interpreter, and (c) the Elixir specification interpreter. Zero three-way disagreements across all test campaigns.

The property-based testing methodology follows s2n [16]: a formal specification in a proof assistant, extraction to executable code, and continuous comparison with the runtime implementation. The 188th random input in the original campaign discovered a real capability-tree bug [6], validating the approach.

9.4.0.1 Runtime overhead of proved code.

The extracted governance kernel runs in the BEAM runtime’s directive execution path. Governed execution through a supervised process completes in 0.23 ms median, compared to 0.24 ms for direct ungoverned execution (bypassing all governance). The Rocq-extracted, formally verified code path adds no measurable overhead.¹

10 Related Work↩︎

10.0.0.1 Algebraic effects and handlers.

Plotkin and Pretnar [11], [12] introduced algebraic effects and handlers as a structured approach to computational effects, building on the algebraic theory of Plotkin and Power [17]. Subsequent work developed type systems for effect tracking: Koka’s row-typed effects [13], freer monads [18], and dependently-typed effects in Idris [19]. Our framework differs in constraining the handler algebra itself: only handlers satisfying a governance proof obligation (GovernedHandler) can be used in governed composition. Programs interpreted through ungoverned handlers do not satisfy gov_safe and are excluded from the governed fragment.

10.0.0.2 Monoidal categories in programming languages.

Mac Lane [20] established the coherence conditions for monoidal categories. Joyal and Street [21] developed the theory of braided tensor categories. Applied category theory has been used in programming language semantics [22], [23] and, more recently, as a framework for AI systems [24]. Our contribution is the combination of monoidal structure with governance safety: we verify not only coherence but also that every tensor composition is governed. The interaction tree representation makes coherence proofs computational (pure structural morphisms reduce by \(\beta\)) rather than requiring explicit diagram chasing.

10.0.0.3 Verified systems.

seL4 [25] verified a complete OS kernel; CompCert verified a C compiler [26]; CertiKOS verified concurrent OS kernels [27]; Vellvm formalized LLVM IR semantics using interaction trees [28]. Our work is closest to Vellvm in technique (interaction trees in Rocq) but targets AI workflow governance rather than compiler/OS verification. The scale is smaller ( 12,000 lines vs. Vellvm’s \(\sim\)​50,000) but covers a different domain. Amazon s2n’s continuous verification [16] inspired our specification-driven testing methodology.

10.0.0.4 Effect systems and capability security.

The Gifford-Lucassen effect system [29], [30] introduced static tracking of computational effects. Capability-based security [31], [32] restricts access to resources via unforgeable tokens. Our capability sets function similarly to effect annotations, but with a crucial difference: the gov_safe predicate is a runtime invariant enforced by the governance operator, not just a static type system property. The dual guarantee (Theorem 21) connects the static and dynamic views.

10.0.0.5 AI governance.

RLHF [1] and constitutional AI [2] govern LLM behavior via training signal. NeMo Guardrails [3] provides programmable guardrails for LLM applications. These approaches operate on model outputs (what the model says). Our framework governs the system’s effects (what the system does). Theorem 3 establishes, within our formal model, that a content-governed handler wrapped with \(\mathcal{G}\) satisfies gov_safe, while unmediated I/O does not. The two approaches address different enforcement problems and are complementary: content governance shapes output quality; structural governance ensures effect mediation.

10.0.0.6 Guaranteed safe AI.

Dalrymple et al. [33] propose a framework for guaranteed safe AI comprising a world model, a safety specification, and a verifier. Their framework identifies the right components but provides no mechanized formalization. Our work can be seen as supplying the algebraic semantics and machine-checked proofs for one instance of their architecture: the governance algebra is the safety specification, the interpreter is the verifier, and the governed interaction trees are the world model. The key difference is that their approach targets pre-deployment verification (proving safety before execution), while ours provides execution-time effect governance (ensuring safety structurally during execution). The approaches are complementary but address different points in the deployment lifecycle.

10.0.0.7 Effect verification.

Song, Foo, and Chin [34] develop ESL, an expressive specification logic for verifying programs with unrestricted algebraic effects and handlers. Their work verifies that programs satisfy specifications given arbitrary handlers. Our work constrains the handler algebra itself: non-governed handlers cannot be constructed in the safe fragment (Theorem 15). The direction is reversed: they verify programs against handlers; we constrain handlers to governance. Vistrup et al. [35] develop modular program logics over interaction trees using Iris, sharing our ITree foundation but targeting shared-state concurrency and fine-grained reasoning about heap resources rather than AI governance and effect boundaries.

10.0.0.8 Session types.

Session types [36] govern communication protocols via types. Like our approach, they provide structural guarantees. The difference is scope: session types govern message sequences between parties; our framework governs arbitrary effectful computation. Session types could complement our approach for inter-machine communication patterns.

10.0.0.9 Runtime verification.

Runtime verification [37] monitors execution traces against formal specifications. Our trace semantics (Section 7) formalizes the trace structure, and the ledger connection establishes tamper evidence. The key difference is that our governance is not post-hoc monitoring but structural: the gov_safe predicate is a coinductive property of the governed program tree, guaranteed to hold before any execution begins.

11 Conclusion↩︎

We have presented an algebraic semantics for governed execution, formalized in 36 Rocq modules with 454 theorems and zero admitted lemmas. The central result is that governance, when axiomatized as a three-property algebra over interaction trees, induces compositional structure on programs, effects, and capabilities such that the governed fragment coincides with the expressible fragment in the modeled substrate. Turing completeness is preserved inside governance.

The four contributions are: (1) a parametric GovernanceAlgebra with verified monoidal structure; (2) a governed algebraic effect system where the handler algebra is closed under governance-preserving composition; (3) capability-indexed composition with the dual guarantee; (4) the coterminous boundary within the formal model.

11.0.0.1 Limitations and future work.

The tensor product is sequential-independent, not truly concurrent. Concurrent interleaving would require a more complex construction (possibly using concurrent interaction trees or a process-algebraic extension). The hash chain formalization assumes an abstract injective hash function; connecting this to a concrete cryptographic hash (with collision resistance rather than injectivity) requires additional work. The extraction to OCaml NIF is one-directional: properties proved in Rocq constrain the extracted code, but the NIF wrapper (C bridge between Erlang and OCaml) is not itself verified. The three-layer testing strategy (property-based testing with 70,000+ inputs and zero disagreements, 36 conformance tests mapping to Rocq theorems, and the extraction pipeline itself) establishes the correspondence using the same methodology as seL4 and Amazon s2n.

The GovernanceAlgebra record has three axioms; whether these form a complete axiomatization (every valid governance operator satisfies them) remains open. The coterminous boundary is established for the specific four-primitive execution model; extending it to richer effect signatures or concurrent governance is future work. Denial-as-divergence is one conservative semantic choice; alternative formalizations using explicit denial effects may be preferable in settings where refinement reasoning is needed.

11.0.0.2 Acknowledgments.

Mashin is a product of Mashin, Inc. The Rocq development uses the Interaction Trees library by Xia et al. [9] and the paco library by Hur et al. [10].

12 Rocq Module Index↩︎

Table 2 lists all 36 modules with their primary theorems. All theorem names are valid Rocq identifiers that can be checked in the mechanization.

References↩︎