pith. sign in

arxiv: 2605.01030 · v2 · submitted 2026-05-01 · 💻 cs.AI · cs.LO· cs.PL

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

Alan L. McCann This is my paper

Pith reviewed 2026-05-09 19:22 UTC · model grok-4.3

classification 💻 cs.AI cs.LOcs.PL
keywords AI governanceInteraction Treessemantic transparencycomputational expressivityworkflow architecturesformal verificationdecidability boundaryeffect mediation
0
0 comments X

The pith

Effect-level governance can be imposed on AI workflow architectures without reducing their internal computational expressivity or changing permitted behaviors.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a machine-checked formal model of AI workflows in Rocq using Interaction Trees and defines a governance operator that controls all effects such as memory access, external calls, and oracle queries. It proves that this form of governance leaves the underlying computation fully intact for executions that satisfy the governance rules. A central result is semantic transparency: permitted runs produce exactly the same observations as the ungoverned version, aside from the governance events themselves. This separation shows that effect constraints and expressive power can be treated as independent dimensions in the design of governed AI systems.

Core claim

The authors define a governance operator G that mediates every effectful directive in Interaction Trees. They establish seven properties: governed Turing completeness, governed oracle expressivity, a decidability boundary separating total governance predicates from undecidable program properties, goal preservation on permitted paths, expressive minimality of the five primitive capabilities, strict subsumption of content-level filtering, and semantic transparency under which permitted executions are observationally equivalent to their ungoverned counterparts.

What carries the argument

The governance operator G on Interaction Trees, which intercepts and filters all effectful actions while leaving the internal tree structure and permitted computations unchanged.

If this is right

  • AI workflows remain Turing complete and oracle-expressive once the governance operator is applied.
  • Governance predicates stay decidable and closed under Boolean operations even while full semantic properties of the programs remain undecidable.
  • Structural effect governance strictly contains and improves upon simpler content-level filtering approaches.
  • Permitted executions under governance are observationally identical to ungoverned executions.
  • The five primitive capabilities suffice to express any governed workflow without loss of minimality.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same governance construction might be lifted to other effectful models such as process calculi or distributed actor systems.
  • Implementations could wrap existing LLM agents with effect boundaries while preserving their original reasoning traces on allowed inputs.
  • The decidability boundary implies that automatic safety monitors can be added without solving the general halting problem for the governed programs.
  • If the model scales, governance layers could be composed without forcing designers to simplify internal computation logic.

Load-bearing premise

The Interaction Trees model together with the defined governance operator accurately captures every relevant effectful behavior of real AI workflow architectures, including oracle queries.

What would settle it

A concrete AI workflow execution in which the governed version produces a different final state or observable output than the ungoverned version on the same permitted input, beyond any governance-only events.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The paper claims to provide a machine-checked formalization in Rocq of effect-transparent governance for AI workflow architectures using Interaction Trees. It defines a governance operator G that mediates all effectful directives and proves seven properties: governed Turing completeness (P1), governed oracle expressivity (P2), a decidability boundary (P3), goal preservation (P4), expressive minimality (P5), subsumption asymmetry over content filtering (P6), and semantic transparency (P7) where permitted governed executions are observationally equivalent to ungoverned ones. The overall thesis is that governance and computational expressivity are orthogonal.

Significance. If the formal results hold, this work is significant as it offers a rigorous, machine-verified demonstration that structural governance can be added to AI systems at the effect level without sacrificing expressivity or altering the semantics of permitted computations. The complete Rocq development with 454 theorems and no admitted lemmas provides strong evidence for the claims within the formal model, potentially informing the design of verifiable and governable AI architectures.

major comments (1)
  1. [Abstract (and the definition of the governance operator G)] The central claims P1, P2, and P7 rely on the Interaction Trees effect signature together with G exhaustively mediating all relevant effectful behaviors in AI workflows, including memory, external calls, and oracle/LLM queries. The manuscript asserts mediation of 'all effectful directives' but does not appear to provide an explicit argument or proof that the signature is complete and that no effects can occur outside G's mediation (e.g., untyped side effects or dynamically introduced effects). This is load-bearing for the semantic transparency and orthogonality results to transfer beyond the model.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful and constructive review. The major comment identifies a point of exposition that we agree merits explicit clarification in the manuscript. We address it below and will revise accordingly.

read point-by-point responses

  1. Referee: The central claims P1, P2, and P7 rely on the Interaction Trees effect signature together with G exhaustively mediating all relevant effectful behaviors in AI workflows, including memory, external calls, and oracle/LLM queries. The manuscript asserts mediation of 'all effectful directives' but does not appear to provide an explicit argument or proof that the signature is complete and that no effects can occur outside G's mediation (e.g., untyped side effects or dynamically introduced effects). This is load-bearing for the semantic transparency and orthogonality results to transfer beyond the model.

    Authors: We agree that an explicit statement on signature completeness strengthens the presentation. In the Rocq development the effect signature is defined as a closed inductive datatype Effect whose constructors are exactly the primitive effects for memory access, external calls, oracle/LLM queries, and observability. The governance operator G is defined by exhaustive case analysis over every constructor of this datatype; the ITree type is parameterized by Effect, so every well-typed itree can emit only events from this signature. Untyped side effects and dynamic introduction of new effect types are outside the Interaction Trees framework and are not modeled. We will add a short subsection 'Effect Signature Exhaustiveness' (new Section 3.2) that states this design choice, quotes the Rocq definition, and notes that the orthogonality results hold inside this model. This revision makes the scope of the claims explicit without changing any theorems. revision: yes

Circularity Check

0 steps flagged

No circularity: machine-checked Rocq formalization derives properties from explicit definitions

full rationale

The paper defines the Interaction Trees model and governance operator G explicitly, then proves P1-P7 (including Turing completeness, oracle expressivity, and semantic transparency) via 454 theorems in 36 modules with zero admitted lemmas. No equations reduce outputs to inputs by construction, no parameters are fitted to data and relabeled as predictions, and no self-citations or prior author results are invoked as load-bearing uniqueness theorems. The derivation chain is self-contained within the stated formal semantics; the completeness of the effect signature is an explicit modeling assumption rather than a hidden reduction, so the proofs do not collapse to their own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The central claim rests on the standard semantics of Interaction Trees and the definition of the governance operator G; no free parameters are fitted to data.

axioms (2)
  • standard math Interaction Trees provide a compositional semantics for effectful computations including memory, external calls, and oracle queries.
    Invoked as the base model for defining the governance operator G and proving observational equivalence.
  • domain assumption All effectful directives in the workflow are mediated through the governance operator.
    Required for the claim that governance constrains the effect boundary without internal changes.
invented entities (1)
  • governance operator G no independent evidence
    purpose: To mediate all effectful directives while preserving semantics and expressivity.
    Newly defined construct in the formalization; no independent evidence outside the Rocq development is provided.

pith-pipeline@v0.9.0 · 5547 in / 1406 out tokens · 31131 ms · 2026-05-09T19:22:44.790950+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

21 extracted references · 12 canonical work pages · 1 internal anchor

  1. [1]

    Constitutional AI: Harmlessness from AI Feedback

    Yuntao Bai, Saurav Kadavath, Sandipan Kundu, et al. Constitutional AI : Harmlessness from AI feedback, 2022. arXiv:2212.08073

    work page internal anchor Pith review Pith/arXiv arXiv 2022

  2. [2]

    Programming with algebraic effects and handlers

    Andrej Bauer and Matija Pretnar. Programming with algebraic effects and handlers. Journal of Logical and Algebraic Methods in Programming, 84 0 (1): 0 108--123, 2015. doi:10.1016/j.jlamp.2014.02.001

    work page doi:10.1016/j.jlamp.2014.02.001 2015

  3. [3]

    Towards guaranteed safe AI: A framework for ensuring robust and reliable ai systems.arXiv preprint arXiv:2405.06624,

    David Dalrymple et al. Towards guaranteed safe AI : A framework for ensuring robust and reliable AI systems, 2024. arXiv:2405.06624

    work page arXiv 2024

  4. [4]

    The power of parameterization in coinductive proof

    Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis. The power of parameterization in coinductive proof. In Proceedings of the ACM on Programming Languages (POPL), 2013. doi:10.1145/2429069.2429093

    work page doi:10.1145/2429069.2429093 2013

  5. [5]

    seL4: formal verification of an OS kernel,

    Gerwin Klein, Kevin Elphinstone, Gernot Heiser, et al. seL4 : Formal verification of an OS kernel. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), 2009. doi:10.1145/1629575.1629596

    work page doi:10.1145/1629575.1629596 2009

  6. [6]

    Formal verification of a realistic compiler,

    Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52 0 (7): 0 107--115, 2009. doi:10.1145/1538788.1538814

    work page doi:10.1145/1538788.1538814 2009

  7. [7]

    Algebraic semantics of governed execution: Monoidal categories, effect algebras, and coterminous boundaries, 2026 a

    Alan Lawrence McCann. Algebraic semantics of governed execution: Monoidal categories, effect algebras, and coterminous boundaries, 2026 a

    2026

  8. [8]

    Mechanized foundations of structural governance: Machine-checked proofs for governed intelligence, 2026 b

    Alan Lawrence McCann. Mechanized foundations of structural governance: Machine-checked proofs for governed intelligence, 2026 b

    2026

  9. [9]

    Cryptographic registry provenance: Structural defense against dependency confusion in AI package ecosystems, 2026 c

    Alan Lawrence McCann. Cryptographic registry provenance: Structural defense against dependency confusion in AI package ecosystems, 2026 c . arXiv preprint (submitted)

    2026

  10. [10]

    Certified purity for cognitive workflow executors: From static analysis to cryptographic attestation, 2026 d

    Alan Lawrence McCann. Certified purity for cognitive workflow executors: From static analysis to cryptographic attestation, 2026 d

    2026

  11. [11]

    The two boundaries: Why behavioral AI governance fails structurally, 2026 e

    Alan Lawrence McCann. The two boundaries: Why behavioral AI governance fails structurally, 2026 e

    2026

  12. [12]

    Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, 1967

    1967

  13. [13]

    Training language models to follow instructions with human feedback

    Long Ouyang, Jeff Wu, Xu Jiang, et al. Training language models to follow instructions with human feedback. In NeurIPS, 2022

    2022

  14. [14]

    O’Brien, Carrie Jun Cai, Meredith Ringel Morris, Percy Liang, and Michael S

    Joon Sung Park, Joseph C. O'Brien, Carrie J. Cai, Meredith Ringel Morris, Percy Liang, and Michael S. Bernstein. Generative agents: Interactive simulacra of human behavior. In Proceedings of UIST, 2023. doi:10.1145/3586183.3606763

    work page doi:10.1145/3586183.3606763 2023

  15. [15]

    Plotkin and Matija Pretnar

    Gordon D. Plotkin and Matija Pretnar. Handlers of algebraic effects. In Programming Languages and Systems (ESOP). Springer, 2009. doi:10.1007/978-3-642-00590-9_7

    work page doi:10.1007/978-3-642-00590-9_7 2009

  16. [16]

    Theory of Recursive Functions and Effective Computability

    Hartley Rogers. Theory of Recursive Functions and Effective Computability. McGraw-Hill, 1967

    1967

  17. [17]

    Seshia, Dorsa Sadigh, and S

    Sanjit A. Seshia, Dorsa Sadigh, and S. Shankararaman Shankar. Towards verified artificial intelligence, 2016. arXiv:1606.08514

    work page arXiv 2016

  18. [18]

    Sumers, Shunyu Yao, Karthik Narasimhan, and Thomas L

    Theodore R. Sumers, Shunyu Yao, Karthik Narasimhan, and Thomas L. Griffiths. Cognitive architectures for language agents. Transactions on Machine Learning Research (TMLR), 2024

    2024

  19. [19]

    Monads for functional programming

    Philip Wadler. Monads for functional programming. In Advanced Functional Programming (AFP). Springer, 1995. doi:10.1007/3-540-59451-5_2

    work page doi:10.1007/3-540-59451-5_2 1995

  20. [20]

    Pierce, and Steve Zdancewic

    Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction trees: Representing recursive and impure programs in Coq . In Proceedings of the ACM on Programming Languages (POPL), volume 4, 2020. doi:10.1145/3371119

    work page doi:10.1145/3371119 2020

  21. [21]

    Modular, compositional, and executable formal semantics for LLVM IR

    Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva, and Steve Zdancewic. Modular, compositional, and executable formal semantics for LLVM IR . In Proceedings of the ACM on Programming Languages (ICFP), volume 5, 2021. doi:10.1145/3473572

    work page doi:10.1145/3473572 2021