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

Researchers at arXiv released a machine-checked formal framework for governing AI workflow architectures using Interaction Trees in Rocq 8.19, proving that effect-level governance preserves full Turing completeness and oracle expressivity. The 12,000-line, 454-theorem development with zero admitted lemmas establishes a critical decidability boundary: governance predicates remain total and Boolean-composable while semantic program properties stay provably undecidable by the governor. This directly addresses agentic LLM pipeline safety, offering formally verified guarantees that memory access, external calls, and oracle queries can be controlled without sacrificing computational power. Teams building production multi-agent systems now have a rigorous theoretical foundation that prior policy-layer approaches lacked entirely.