# Governed Metaprogramming for Intelligent Systems: Reclassifying Eval as a Governed Effect

arXiv: https://arxiv.org/abs/2605.05248 · HTML: https://mlsanity.com/paper/2605.05248/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 3 of its 24 references that are in the map.
- First posted on arXiv 5 May 2026.

## Builds on (most cited first, 3 of 3)

- [NeMo Guardrails: A Toolkit for Controllable and Safe LLM Applications with Programmable Rails](https://mlsanity.com/paper/2310.10501/) (2023)
- [Interaction Trees: Representing Recursive and Impure Programs in Coq](https://mlsanity.com/paper/1906.00046/) (2019)
- [Mechanized Foundations of Structural Governance: Machine-Checked Proofs for Governed Intelligence](https://mlsanity.com/paper/2604.27289/) (2026)

## Abstract (arXiv)

AI systems increasingly synthesize executable structure at runtime: LLMs generate programs, agents construct workflows,self-improving systems modify their own behavior. In classical homoiconic and staged languages, the transition from code representation to execution is unrestricted. eval is a language primitive, not a governed operation. We argue that in governed intelligent systems, this transition is an authority amplification: it converts symbolic structure into executable authority and must be mediated like any other effect. We present governed metaprogramming, a language design where program representations (machine forms) are first-class values, form manipulation is pure computation, and materialization (the transition from form to executable machine) is a governed effect subject to structural inspection. The governance system analyzes the proposed program's capability requirements, policy compliance, and resource estimates before permitting execution. We formalize two judgments: pure form evaluation (which emits no directives) and governed materialization (which emits exactly one governed directive). We prove three properties: purity of form manipulation, the no-bypass theorem, and boundary preservation. We implement the design in mashinTalk, a DSL for AI workflows compiling to BEAM byte code, and report on integration with 454 existing machine-checked Rocq theorems. The central contribution is reclassifying eval from a language primitive into a governed effect.
