Stability Before Behavior: A Lean 4 Certified Control Layer for Language-Model Agents

Large language models cannot be formally verified, and the field's compensations, evaluation, alignment, and perimeter hardening, are empirical by nature. We invert the object of verification. We present a certified stability layer for AI agents: a small closed-form control system around the model whose dynamics are machine-proven stable in Lean 4, with input-to-state stability, bounded-input bounded-output behavior, and a compositional certificate; an automated identity check that pins the shipped code to the proofs; and an empirical envelope search over the runtime. The model writes the words; the certified layer bounds the state that governs them. We report the architecture at property level and its observed conduct in two deployments sharing the core but not a domain: a relational companion live with pilot users, evaluated independently under adversarial pressure and against responsible-AI governance criteria by two unrelated parties who converged on three of the same findings, and a five-model research crew run governed and ungoverned under identical measurement, where the ungoverned arm shipped defective claims into the shared workspace (19 of 57) and repeated violations at 72 percent, and the governed arm shipped none (0 of 45) with repeat conduct below the clean baseline. Stability is proven; safety is demonstrated; the distinction is maintained throughout, together with the observed limit that containment did not persist when the enforcement loop was removed. The certified constants, operator forms and per-layer theorems summarised here are published in full in the related whitepaper editions listed below. The two independent evaluations are reported in full in the related case study.New in this version. The account of the independent governance review is corrected to describe a preliminary stress test across three categories. The scope word is the evaluator's own and keeps the description accurate to what that round covered. No result, measurement or conclusion changed.