SIGIL: Construction-Level Security for Agent-Authored Code
Large language model (LLM) agents increasingly write, compile, execute, and revise software inside systems that also hold files, credentials, and network authority. In that setting, security cannot depend on human review, external sandboxes, or post-hoc filtering alone: those mechanisms treat generated code as an opaque payload after the agent has already expressed authority, control flow, and data movement in an ambient language. We present SIGIL, a capability-secure programming language and verification pipeline designed for code whose primary author is an LLM. This paper's evaluation concentrates on the ephemeral agent-authored tool: the program an agent writes, runs once, and discards, which is both the most immediate deployment surface and the tightest security envelope. SIGIL layers construction-level security on top of runtime containment: programs still run inside fresh Wasmtime stores with fuel and explicit grants, but authority, effects, taint labels, ring boundaries, and solver-backed proof obligations are visible in source and checked before bytecode exists. The language combines linear capability types, declared effect rows, information-flow taint tracking, two-ring WebAssembly isolation, deterministic certificates, and bounded SMT checks over decidable quantifier-free bitvector and linear integer arithmetic fragments. We evaluate the system with 67 adversarial security cases across 9 documented categories, 10 mechanically-checked CVE retrofits, 214 tools/ programs, 24,699 nonblank lines of SIGIL-authored compiler stages composed into a self-hosted driver whose code-generation path recompiles the compiler's own source to WebAssembly byte-identical to the Rust reference (a self-hosting fixed point), differentially tested against the Rust oracle, and compile-throughput measurements: Z3-heavy fixtures verify in 5-8 ms median time - interactive latency for an agent compile-feedback loop. A mechanized formalization in Lean 4 (lambda-SIGIL) - 160 theorems across 19 modules, with zero sorry and only standard axioms - proves type soundness, capability safety, effect-row confinement and checking, ring isolation, affine ownership, and information-flow taint sink-safety (a noninterference-style trace property). In a live agentic harness, frontier models with no SIGIL in their training data converge on working, verified tools guided only by structured compiler diagnostics: the two strongest models reach 86% and 74% compile success with 95% and 89% all-input behavioral correctness among compiled cells, and compile success across seven models from four vendors spans 6-86%, tracking grammar internalization rather than vendor or security-model friction. These results establish feasibility: construction-level security is practical for interactive agent compile-feedback loops today, without treating runtime containment as obsolete - and the compiler's typed diagnostic surface doubles as a training signal for models that write SIGIL natively, which we identify as the next step.