Alan L. McCannによる論文「Effect-Transparent Governance for AI Workflow Architectures: Semantic Preservation, Expressive Minimality, and Decidability Boundaries」が注目を集めている。本論文は、Rocq 8.19における相互作用木（Interaction Trees）を用いて、AIワークフローアーキテクチャに対する構造化された効果レベルのガバナンスの機械検証された形式化を提案する。ガバナンス演算子Gは、メモリアクセス、外部呼び出し、オラクル（LLM）クエリを含むすべての効果的命令を仲介する。この形式化は36のモジュール、約12,000行のRocqコード、454の定理から構成され、未証明の補題は一切ない。
論文の核心は、ガバナンスと計算表現力が直交する次元であることを証明することにある。具体的には、7つの特性が確立されている：（P1）ガバナンス下でのチューリング完全性、（P2）ガバナンス下でのオラクル表現力、（P3）決定可能性境界：ガバナンス述語は全域でブール結合の下で閉じているが、意味的プログラム特性は非自明でガバナンスでは決定不能である、（P4）許可された実行における目標保存、（P5）プリミティブ能力（計算、メモリ、推論、外部呼び出し、観測可能性）の表現最小性、（P6）包摂非対称性：構造的ガバナンスがコンテンツレベルのフィルタリングを厳密に包含する、（P7）意味的透明性：ガバナンスが許可するすべての実行において、ガバナンスされた解釈は（ガバナンスのみのイベントを除いて）ガバナンスされていない解釈と観測的に等価である。これらの結果は、ガバナンスがプログラムの効果境界を制約する一方で、内部計算に対して意味的に透明であることを示している。
この研究は、AIシステムの安全なガバナンスの理論的基盤を提供し、計算能力を犠牲にすることなくAIワークフローに対するきめ細かい効果制御を可能にする。論文の正式版はarXiv（識別子：2605.01030）で入手可能である。