Nine typechecker holes closed, three machine-checked proofs, and a cloud control plane

A parallel bug hunt found nine expression positions where the typechecker never called check_expr at all. The most critical: a while condition bypassed the entire type and security model, so while db_query(...) compiled without Cap<Db> and while personal_data leaked without consent; f(x = __builtin_cap_fs_root()) could forge a capability past E0402. Eight more positions followed: default parameters, struct and union field defaults, assignment target indices, spawn lambda bodies and match patterns.

All are now enforced, and make check-enforcement-positions gates 26 positions per commit. In the same wave, three trust-critical properties became machine-checked in Rocq with zero admits: capability enforcement (every ambient authority in the model is a provable error), the lexer bisimulation (both directions, including the comment token class) and flow-analysis soundness (tainted data reaching a sink is provably detected). All three re-check per commit via make check-formal-proofs.

The honest remainder: these proofs cover the rules, and nothing yet proves src/typechecker.kern implements them; the correspondence grid is empirical, not formal. Separately, a full cloud control plane landed: multi-tenant with HA standby failover, SSO/OIDC, org-scoped tenants, WAF policies, an S3-compatible object store, load balancers, cordon/drain/fence, metered usage from the tamper-evident chain, scheduled workloads, capacity admission, and a typed client behind kern cloud.

VM capabilities extended to GPU passthrough (VFIO behind an IOMMU, guest PCI bus, interrupt emulation proven in two halves), live migration (snapshot and restore an SMP guest, transport it, resume), and virtio-rng. Five adversarial security criticals from the rc2 scan were closed. The GC nursery shipped earlier was found to lose reachable objects and is now refused; the other performance work (list append, sort, string leaves) stands.