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

> On main since rc2: Nine typechecker holes closed, three machine-checked proofs, and a cloud control plane.

Source: https://kern-lang.eu/releases/typechecker-holes-and-machine-checked-proofs

On main since rc2

## Release notes

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.