# Algebraic Semantics of Governed Execution: Monoidal Categories, Effect Algebras, and Coterminous Boundaries

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 37 references that are in the map.
- First posted on arXiv 1 May 2026.

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

- [Training language models to follow instructions with human feedback](https://mlsanity.com/paper/2203.02155/) (2022)
- [Constitutional AI: Harmlessness from AI Feedback](https://mlsanity.com/paper/2212.08073/) (2022)
- [NeMo Guardrails: A Toolkit for Controllable and Safe LLM Applications with Programmable Rails](https://mlsanity.com/paper/2310.10501/) (2023)
- [Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems](https://mlsanity.com/paper/2405.06624/) (2024)
- [Interaction Trees: Representing Recursive and Impure Programs in Coq](https://mlsanity.com/paper/1906.00046/) (2019)
- [Handling Algebraic Effects](https://mlsanity.com/paper/1312.1399/) (2013)
- [Mechanized Foundations of Structural Governance: Machine-Checked Proofs for Governed Intelligence](https://mlsanity.com/paper/2604.27289/) (2026)
- [The Two Boundaries: Why Behavioral AI Governance Fails Structurally](https://mlsanity.com/paper/2604.27292/) (2026)

## Built on by (most cited first, 1 of 1)

- [Cryptographic Registry Provenance: Structural Defense Against Dependency Confusion in AI Package Ecosystems](https://mlsanity.com/paper/2605.03309/) (2026)

## Abstract (arXiv)

We present an algebraic semantics for governed execution in which governance is axiomatized, compositional, and coterminous with expressibility. The framework, mechanized in 32 Rocq modules (~12,000 lines, 454 theorems, 0 admitted), is built on interaction trees and parameterized coinduction. A three-axiom GovernanceAlgebra record (safety, transparency, properness) induces a symmetric monoidal category with verified pentagon, triangle, and hexagon coherence, where every tensor composition preserves governance. An algebraic effect system constrains the handler algebra so that only governance-preserving handlers can be constructed in the safe fragment; programs in the empty capability set provably emit only observability directives. Capability-indexed composition bundles programs with machine-checked capability bounds, and a dual guarantee theorem establishes that within_caps and gov_safe hold simultaneously under all composition operators. The capstone result is the coterminous boundary: within our formal model, every program expressible via the four primitive morphism constructors is governed under interpretation, and every governed program is the image of such a program. Turing completeness is preserved inside governance; unmediated I/O is excluded from the governed fragment. Governance denial is modeled as safe coinductive divergence. The governance algebra is parametric: any system instantiating the three axioms inherits all derived properties, including convergence, compositional closure, and goal preservation. Extracted OCaml runs as a NIF in the BEAM runtime, with property-based testing (70,000+ random inputs, zero disagreements) confirming behavioral equivalence between the specification and the runtime interpreter.