Algebraic Semantics for Governed Execution of LLMs

Twelve thousand lines of verified Rocq code, 454 theorems and zero admitted lemmas. That is the result presented in the paper Algebraic Semantics of Governed Execution, published this week on arXiv (cs.AI). This is no minor academic exercise: its authors propose a formal framework in which program governance is not an external validation layer, but a structural property preserved through composition.

The question it attempts to answer is deceptively simple: can you guarantee that an AI agent, when chaining operations, never leaves the space of permitted behaviours? The typical industry answer is "more or less, with enough tests." This paper's answer is a theorem.

What the paper proposes

The core of the work is a `GovernanceAlgebra` with three axioms: safety, transparency (observability) and properness (structural correctness). From there, the system constructs a symmetric monoidal category, with pentagon, triangle and hexagon coherence formally verified, in which each tensor composition preserves governance. Put more plainly: if two pieces of a program are governed, their combination is too, and this is formally proven, not assumed.

The algebraic effects system adds a second guarantee: only handlers that preserve governance can be constructed in the safe fragment. Programs with an empty set of capabilities produce only observability directives. That is, an agent with no declared capabilities cannot act; it can only report.

The result the authors call the "coterminous boundary" is the most ambitious: within the formal model, every program expressible using the four primitive morphism constructors is governed under interpretation, and every governed program is expressible. Expressibility and governance coincide at the same boundary.

Why it matters for the Claude ecosystem

This work does not mention Claude or MCP directly, but its implications are immediate for any agent system that chains tools with differentiated permissions, exactly what Claude Code does with its subagents, hooks and MCP servers.

Today, when a developer builds a pipeline with multiple subagents in Claude Code, the guarantee that no subagent exceeds its declared capabilities is largely contractual: you trust that the implementation respects the limits. The paper's framework proposes something different: capability-indexed composition, where programs carry mechanically verified capability bounds, and the dual guarantee theorem ensures that `within_caps` and `gov_safe` hold under all composition operators.

If this kind of semantics were integrated, or at least taken as a reference, in MCP specification or Claude Code hook mechanisms, it would no longer be necessary to trust the correctness of each individual MCP server. Governance would be a property of the composition protocol, not of each implementation.

Who this is relevant for

First, teams building high-stakes agents: infrastructure automation, pipelines with access to financial systems, or any scenario where an uncontrolled subagent has real consequences. The paper offers precise language for specifying and auditing capability boundaries.

Second, those working on MCP specification. The protocol already defines scopes and permissions, but lacks a verified compositional semantics. This framework could inform future versions.

Finally, developers of plugins and skills in Claude Code who want to offer formal guarantees to their enterprise users: the `GovernanceAlgebra` provides a certification vocabulary that goes beyond unit tests.

What remains to be resolved

The paper works within a formal model. The distance between that model and a real implementation in Claude Code or an arbitrary MCP server is considerable. The 32 Rocq modules demonstrate properties of the model, not of deployed software. Additionally, the system's expressivity is bounded to four primitive morphism constructors: a real agent language is richer and messier.

None of this invalidates the work. Formal verification in AI remains an area where theoretical foundations run several years ahead of practical adoption. But papers like this are what eventually change what counts as "sufficient" when certifying an agent.

---

From our perspective, we value that research in formal verification begins speaking the same language as current agent systems. That the main result has its own name, "coterminous boundary," and is fully mechanised is a sign of methodological maturity worthy of attention.