In September 2026 a computer-checked proof of Fermat’s Last Theorem and a Lean-formalizedproof of blowup in the forced Navier—Stokes equations were announced within days of each other,and both are believed because a kernel checked them. This paper applies that discipline at theother end of the scale. A Calculus of Constructions micro-kernel with no axioms, is given an imperative language—assignment, branches, bounded loops, and while with an explicit variant—compiled by symbolic execution into kernel terms. Contracts are decidable propositions, Holds b := Eq Bool b true, about the very expression a runtime check would evaluate. A while loop raises four obligations, one of them the soundness of its own lowering, and termination is proved for every starting state. Records and a state invariant give a model of an seL4-style OS whose routing layer carries contracts that hold for every input. A bridge to Crust, a self-contained C/C++/Rust toolchain, settles its source-level contracts in the kernel; building it found two of Crust’s passes reading one contract two ways. Finally a certificate changes generated code: a SIMD kernel’s scalar remainder is omitted on it, and a contract proven at every call site downgrades 80% of the memory-safety checks in a leaf initializer while the check it leaves still catches an overflow.