Skip to content
AI News HubLIVE
Original source3 min read

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

Summary

This paper presents a machine-checked formalization of structurally governed AI workflow architectures using Interaction Trees in Rocq 8.19. It proves that effect-level governance can be imposed without reducing internal computational expressivity, establishing seven core properties that demonstrate the orthogonality of governance and expressivity.

SourcearXiv AIAuthor: Alan L. McCann
Effect-Transparent Governance for AI Workflow Architectures: Semantic Preservation, Expressive Minimality, and Decidability Boundaries
Report an error

The correction channel is not available yet. You can copy the article reference below for later.

Correction instructions
Read article

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

Skip to main content

Learn about arXiv becoming an independent nonprofit.

We gratefully acknowledge support from the Simons Foundation, member institutions, and all contributors. Donate

> cs > arXiv:2605.01030

Help | Advanced Search

All fields Title Author Abstract Comments Journal reference ACM classification MSC classification Report number arXiv identifier DOI ORCID arXiv author ID Help pages Full text

Search

GO

quick links

Login

Help Pages

About

-->

Computer Science > Artificial Intelligence

arXiv:2605.01030 (cs)

[Submitted on 1 May 2026 (v1), last revised 5 May 2026 (this version, v2)]

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

Authors:Alan L. McCann

View a PDF of the paper titled Effect-Transparent Governance for AI Workflow Architectures: Semantic Preservation, Expressive Minimality, and Decidability Boundaries, by Alan L. McCann

View PDF HTML (experimental)

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

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.01030v2 [cs.AI] for this version)

https://doi.org/10.48550/arXiv.2605.01030

Focus to learn more

arXiv-issued DOI via DataCite

Submission history

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)

Full-text links:

Access Paper:

View a PDF of the paper titled Effect-Transparent Governance for AI Workflow Architectures: Semantic Preservation, Expressive Minimality, and Decidability Boundaries, by Alan L. McCann

View PDF

HTML (experimental)

TeX Source

view license

Current browse context:

cs.AI

new | recent | 2026-05

Change to browse by:

cs cs.LO cs.PL

References & Citations

NASA ADS

Google Scholar

Semantic Scholar

export BibTeX citation Loading...

BibTeX formatted citation

×

loading...

Data provided by:

Bookmark

Bibliographic Tools

Bibliographic and Citation Tools

Bibliographic Explorer Toggle

Bibliographic Explorer (What is the Explorer?)

Connected Papers Toggle

Connected Papers (What is Connected Papers?)

Litmaps Toggle

Litmaps (What is Litmaps?)

scite.ai Toggle

scite Smart Citations (What are Smart Citations?)

Code, Data, Media

Code, Data and Media Associated with this Article

alphaXiv Toggle

alphaXiv (What is alphaXiv?)

Links to Code Toggle

CatalyzeX Code Finder for Papers (What is CatalyzeX?)

DagsHub Toggle

DagsHub (What is DagsHub?)

GotitPub Toggle

Gotit.pub (What is GotitPub?)

Huggingface Toggle

Hugging Face (What is Huggingface?)

ScienceCast Toggle

ScienceCast (What is ScienceCast?)

Demos

Demos

Replicate Toggle

Replicate (What is Replicate?)

Spaces Toggle

Hugging Face Spaces (What is Spaces?)

Spaces Toggle

TXYZ.AI (What is TXYZ.AI?)

Related Papers

Recommenders and Search Tools

Link to Influence Flower

Influence Flower (What are Influence Flowers?)

Core recommender toggle

CORE Recommender (What is CORE?)

Author

Venue

Institution

Topic

About arXivLabs

arXivLabs: experimental projects with community collaborators

arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.

Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.

Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.

Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)

About

Help

contact arXivClick here to contact arXiv Contact

subscribe to arXiv mailingsClick here to subscribe Subscribe

Copyright

Privacy Policy

Web Accessibility Assistance

arXiv Operational Status

Key points and analysis

Article intelligence

EngineersAdvanced

Key points

  • Formalized governance operator G mediating all effectful directives in Rocq 8.19 with zero admitted lemmas.
  • Proves seven properties including governed Turing completeness, semantic transparency, and expressive minimality.
  • Shows that governance constrains effect boundaries while remaining transparent to internal computation.

Highlights and analysis are generated automatically and may contain errors. Check the original source.