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

Alan L. McCann's new paper tackles a fundamental challenge in AI safety: how to enforce governance on AI workflows (like agentic systems calling LLMs and tools) without crippling their computational power. The work provides a machine-checked formalization in Rocq 8.19 using Interaction Trees, a coinductive data structure for representing effectful computations. The development compiles with zero admitted lemmas across 36 modules, totaling ~12,000 lines of Rocq and 454 theorems. McCann defines a governance operator G that mediates all effectful directives—including memory access, external calls, and oracle (LLM) queries—and proves seven key properties about the resulting architecture.

Among the most striking findings are (P1) governed Turing completeness (governed systems remain as powerful as ungoverned ones), (P2) governed oracle expressivity (LLM calls still work under governance), (P3) a decidability boundary where governance predicates are total and decidable while semantic program properties remain non-trivial and undecidable, and (P7) semantic transparency: for any execution where governance permits, the governed interpretation is observationally equivalent to the ungoverned one (modulo governance events). The paper also shows that structural governance strictly subsumes content-level filtering (P6) and that the minimal primitive capabilities (compute, memory, reasoning, external call, observability) are expressively minimal (P5). These results imply that governance and computational expressivity are orthogonal dimensions: you can impose strict effect boundaries on AI workflows without fundamentally limiting what they can compute.