Mythos and the Unverified Cage:Z3-Based Pre-Deployment Verification for Frontier-Model Sandbox Infrastructure

COBALT: Formal verification of arithmetic vulnerabilities in AI containment infrastructure (Z3 SMT, validated on NASA cFE, wolfSSL, Mosquitto, F Prime) I built COBALT, a Z3 SMT engine that formally verifies CWE-190/191/195 arithmetic vulnerability patterns in C/C++ infrastructure before deployment. Validated on four production codebases with reproducible encodings, concrete SAT witnesses, and acknowledged security outcomes. The broader argument: AI containment stacks need formal pre-deployment verification, not just behavioral safeguards.