Semántica algebraica para ejecución gobernada de LLMs

Doce mil líneas de código Rocq verificado, 454 teoremas y cero lemas admitidos sin demostrar. Ese es el resultado que presenta el paper Algebraic Semantics of Governed Execution, publicado esta semana en arXiv (cs.AI). No es un ejercicio académico menor: sus autores proponen un marco formal en el que la gobernanza de un programa no es una capa externa de validación, sino una propiedad estructural que se preserva por composición.

La pregunta que intenta responder es deceptivamente simple: ¿se puede garantizar que un agente de IA, al encadenar operaciones, no salga nunca del espacio de comportamientos permitidos? La respuesta habitual en la industria es «más o menos, con suficientes tests». La respuesta de este paper es un teorema.

Qué propone el paper

El núcleo del trabajo es una `GovernanceAlgebra` con tres axiomas: safety (seguridad), transparency (observabilidad) y properness (corrección estructural). A partir de ahí, el sistema construye una categoría monoidal simétrica —con coherencia pentagon, triangle y hexagon verificada— en la que cada composición tensorial preserva la gobernanza. Dicho en términos más llanos: si dos piezas de un programa están gobernadas, su combinación también lo está, y esto está demostrado formalmente, no asumido.

El sistema de efectos algebraicos añade una segunda garantía: solo los handlers que preservan la gobernanza pueden construirse en el fragmento seguro. Los programas con un conjunto de capacidades vacío producen únicamente directivas de observabilidad. Es decir, un agente sin capacidades declaradas no puede actuar; solo puede reportar.

El resultado que los autores denominan «coterminous boundary» es el más ambicioso: dentro del modelo formal, todo programa expresable mediante los cuatro constructores morfismo primitivos está gobernado bajo interpretación, y todo programa gobernado es expresable. Expresabilidad y gobernanza coinciden en el mismo límite.

Por qué importa para el ecosistema Claude

Este trabajo no menciona Claude ni MCP directamente, pero sus implicaciones son inmediatas para cualquier sistema de agentes que encadene herramientas con permisos diferenciados —exactamente lo que hace Claude Code con sus subagentes, hooks y servidores MCP.

Hoy, cuando un desarrollador construye un pipeline con varios subagentes en Claude Code, la garantía de que ningún subagente excede sus capacidades declaradas es, en gran medida, contractual: confías en que la implementación respeta los límites. El marco del paper propone algo distinto: capability-indexed composition, donde los programas llevan asociadas cotas de capacidad verificadas mecánicamente, y el teorema de garantía dual asegura que `within_caps` y `gov_safe` se mantienen bajo todos los operadores de composición.

Si este tipo de semántica se integrara —o al menos se tomara como referencia— en la especificación de MCP o en los mecanismos de hooks de Claude Code, dejaría de ser necesario confiar en la corrección de cada servidor MCP individual. La gobernanza sería una propiedad del protocolo de composición, no de cada implementación.

Para quién es relevante

En primer lugar, para equipos que construyen agentes de alto riesgo: automatización de infraestructura, pipelines con acceso a sistemas financieros, o cualquier escenario donde un subagente descontrolado tenga consecuencias reales. El paper ofrece un lenguaje preciso para especificar y auditar límites de capacidad.

En segundo lugar, para quienes trabajan en la especificación de MCP. El protocolo ya define scopes y permisos, pero no cuenta con una semántica composicional verificada. Este framework podría informar versiones futuras.

Finalmente, para desarrolladores de plugins y skills en Claude Code que quieran ofrecer garantías formales a sus usuarios empresariales: la `GovernanceAlgebra` proporciona un vocabulario de certificación que va más allá de los tests unitarios.

Lo que queda por resolver

El paper trabaja dentro de un modelo formal. La distancia entre ese modelo y una implementación real en Claude Code o en un servidor MCP arbitrario es considerable. Los 32 módulos Rocq demuestran propiedades del modelo, no del software desplegado. Además, la expresividad del sistema está acotada a cuatro constructores morfismo primitivos: un lenguaje real de agentes es más rico y desordenado.

Nada de esto invalida el trabajo. La verificación formal en IA sigue siendo un área donde los fundamentos teóricos van varios años por delante de la adopción práctica. Pero papers como este son los que eventualmente cambian qué se considera «suficiente» a la hora de certificar un agente.

---

Desde EP, valoramos que la investigación en verificación formal empiece a hablar el mismo idioma que los sistemas de agentes actuales. Que el resultado principal tenga nombre propio —«coterminous boundary»— y esté completamente mecanizado es una señal de madurez metodológica que merece seguimiento.