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

Researchers formalized governed execution as a symmetric monoidal category with three axioms (safety, transparency, properness) in Rocq, mechanizing 12,000 lines across 454 theorems, where capability-indexed composition and algebraic effect handlers enforce that only governance-preserving operations compose and programs in the empty capability set provably emit only observability directives.