A language where safety is proved by construction, not tested. Z3 verification, arena memory, and MLIR codegen that matches or outperforms C on every verified benchmark.