This paper formalizes a governance layer for AI workflows and proves it can constrain effects like memory access and LLM calls without reducing internal expressivity. The machine-checked Rocq development should interest builders working on agent runtimes, control, and verifiable orchestration.
arXiv:2605.01030v2 Announce Type: new 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…