# Effect-Transparent Governance for AI Workflow Architectures: Semantic Preservation, Expressive Minimality, and Decidability Boundaries

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 25 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)
- [Generative Agents: Interactive Simulacra of Human Behavior](https://mlsanity.com/paper/2304.03442/) (2023)
- [Constitutional AI: Harmlessness from AI Feedback](https://mlsanity.com/paper/2212.08073/) (2022)
- [Cognitive Architectures for Language Agents](https://mlsanity.com/paper/2309.02427/) (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)
- [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 a machine-checked formalization of structurally governed AI workflow architectures and prove that effect-level governance can be imposed without reducing internal computational expressivity. Using Interaction Trees in Rocq 8.19, we define a governance operator G that mediates all effectful directives, including memory access, external calls, and oracle (LLM) queries. Our development compiles with 0 admitted lemmas and consists of 36 modules, ~12,000 lines of Rocq, and 454 theorems. We establishseven properties: (P1) governed Turing completeness, (P2) governed oracle expressivity, (P3) a decidability boundary in which governance predicates are total and closed under Boolean composition while semantic program properties remain non-trivial and undecidable by governance, (P4) goal preservation for permitted executions, (P5) expressive minimality of primitive capabilities (compute, memory, reasoning, external call, observability), (P6) subsumption asymmetry showing structural governance strictly subsumes content-level filtering, and (P7) semantic transparency: on all executions where governance permits, the governed interpretation is observationally equivalent (modulo governance-only events) to the ungoverned interpretation. Together, these results show that governance and computational expressivity are orthogonal dimensions: governance constrains the effect boundary of programs while remaining semantically transparent to internal computation.