Intent-Driven Computing: A Computational Model for Governed Autonomous Systems
arXiv cs.PL | May 2026
IDC Defines intent-driven computing: a programming model where programs produce intents (finite data values describing proposed actions) rather than directly executing effects. A governed runtime examines each intent against a decidable policy language, records every decision in a tamper-evident ledger, and only then realizes the effect. Yields emergent properties: event sourcing by construction, governance simulation via intent replay, structural audit completeness, and improved human comprehensibility. Verified in Rocq (454 theorems, 36 modules, zero admitted lemmas). Property-based testing (70,000+ random inputs, zero disagreements).
The Two Boundaries: Why Behavioral AI Governance Fails Structurally
arXiv cs.AI | April 2026
TB Formal analysis of the structural gap in AI effect governance. Every effectful system has two boundaries (expressiveness and governance) that are almost never identical. Rice's theorem proves the gap is permanent for Turing-complete systems. Proposes coterminous governance as testable criterion.
Mechanized Foundations of Structural Governance: Machine-Checked Proofs for Governed Intelligence
arXiv cs.AI | April 2026
MFSG Five foundational results mechanized in Rocq 8.19 with zero admitted lemmas. ~12,000 lines across 36 modules, 454 theorems. Establishes Governed Cognitive Completeness as capstone. Extraction to OCaml NIF for the BEAM runtime governance kernel.
Effect-Transparent Governance for AI Workflow Architectures: Semantic Preservation, Expressive Minimality, and Decidability Boundaries
arXiv cs.AI | May 2026
GCC Machine-checked formalization proving effect-level governance can be imposed without reducing computational expressivity. Establishes seven properties including governed Turing completeness and subsumption asymmetry.
Algebraic Semantics of Governed Execution: Monoidal Categories, Effect Algebras, and Coterminous Boundaries
arXiv cs.AI | May 2026
AS Algebraic semantics for governed AI execution. Defines GovernanceAlgebra (three axioms) and shows it gives rise to a symmetric monoidal category with verified coherence. All mechanized in Rocq with extraction to verified OCaml NIF.
Certified Purity for Cognitive Workflow Executors: From Static Analysis to Cryptographic Attestation
arXiv cs.CR | May 2026
CP Certified purity architecture converting governance enforcement from runtime convention to structural capability boundary. Four mechanisms: restricted WASM compilation, purity certificates, runtime verification gate, remote attestation.
Cryptographic Registry Provenance: Structural Defense Against Dependency Confusion in AI Package Ecosystems
arXiv cs.CR | May 2026
CRP Cryptographic distribution provenance system addressing dependency confusion attacks. Three components: registry identity (Ed25519), dual-signature model, authoritative namespace binding. Comparison across eight ecosystems.
Governed Metaprogramming for Intelligent Systems: Reclassifying Eval as a Governed Effect
arXiv cs.PL | May 2026
GH Introduces governed homoiconicity: code-as-data manipulation is pure computation, data-as-code materialization is a governed effect. Machine forms are first-class values subject to structural inspection before materialization.