

















Abstract: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.
| Comments: | 15 pages. Companion proofs: this https URL. Project: this https URL. v2: corrected cross-reference identifiers for companion papers. License updated |
| Subjects: | Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO); Programming Languages (cs.PL) |
| ACM classes: | D.2.4; D.3.1; F.3.1; I.2.0 |
| Cite as: | arXiv:2605.01030 [cs.AI] |
| (or arXiv:2605.01030v3 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2605.01030 arXiv-issued DOI via DataCite |
From: Alan McCann [view email]
[v1]
Fri, 1 May 2026 18:52:47 UTC (14 KB)
[v2]
Tue, 5 May 2026 10:41:41 UTC (14 KB)
[v3]
Tue, 26 May 2026 12:30:21 UTC (14 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理,仅供阅读参考。 原文来自 — 版权归原作者所有。