kern v1.0.0, the release line is stable

What "1.0.0" is, exactly

The implementation reached 1.0 grade at rc1 in June: it self-hosts, the full suite is green, the concurrency model is race-free, the build is reproducible. The -rc suffix stayed on for three candidates because the headline goal, verifiable trust, was mid-roadmap and the release gates had only just become CI enforcement. What makes 1.0.0 the stable line is a contract, not a feature.

docs/stability.md enumerates the stable surface: the grammar, the type system, the taint rules (PersonalData, Untrusted, Secret), the capability model, overflow-checked arithmetic, every error and warning code; every pub fn and pub type in the stdlib index; the CLI verbs and their --json schemas; the kern.toml keys. A program that builds on 1.a builds on 1.b with at most new warnings. Nothing on that surface is removed without the cycle: @deprecated in a minor release naming the replacement, warning W0004 at every call site for the rest of the major line, removal only in 2.0. Where the replacement is a drop-in, @deprecated(replace: ...) lets kern fix perform the migration mechanically. Every behavioural claim in that document is pinned by a named conformance or negative test, so the contract cannot drift from the compiler silently.

One layer below the language, the systems surface is locked too. Every public declaration in std.cap_vm, std.cap_unsafe, std.arena, std.dma and std.irq is recorded in docs/systems-surface.lock, and a changed or removed line without a recorded reason is a red gate, because a hypervisor outside this repository builds on them.

A release you verify, not download

For a compiler, a downloadable binary is exactly the Trusting-Trust threat the toolchain exists to remove. So 1.0.0 publishes none, by any route. The three secondary publication paths that used to build and upload compiler tarballs by hand are deleted; make release now refuses and explains. What a release is: a tag signed with a key whose public half is pinned in the repository, a release job that refuses to publish from a tag that does not verify, and a bootstrap-verify job that establishes the tag builds from seed by going seed to gen1 to gen2 and running a real program on gen2. The runtime bundle (the C archives, for cross-compiling without rebuilding ~36K lines of C) and the Windows launcher (a static PE32+ that delegates into WSL2) are the only published artefacts, and both are signed offline with a second pinned key. Neither is a compiler.

The install routes agree with that. The one-liner clones the tag and compiles it with your own clang. The Homebrew tap is the repository itself: Formula/kern.rb names the tag's commit and the published seed, so there is no second copy of the formula to fall behind a release. Windows works like Docker Desktop: a native kern.exe in your terminal, the toolchain running inside WSL2, built and tested in the pinned release image rather than on the runner.

Preparing the release found its own defects, and they are in the changelog rather than smoothed over. The old release script copied the same host binary into all four platform tarballs, varying the filename and nothing else. Release signing would have failed the first time a key was configured, invisible because with no key the step exited 0 every run. And a failed asset upload read as a successful release, because the loop printed "Uploaded" whatever the server answered. All three are fixed; the first one is moot because the tarballs no longer exist.

What 1.0 does not claim

The proofs are about models. Capability enforcement, lexer bisimulation and flow-analysis soundness are machine-checked in Rocq with zero admits and re-checked per commit. What that does not establish on its own is that src/typechecker.kern implements the rules those models state. Since rc3 two of the three got a measurement. The lexer model is extracted to OCaml and required to produce the same token stream as the shipped lexer on every .kern file in the tree (2,374 files) and to refuse the same eleven; its first run found the model emitting true and false as keywords where the lexer emits booleans, in 787 files. The taint model's typing judgement got a decision procedure, proved correct, extracted, and run beside kern check on generated programs. For the capability model the evidence is still the probe grid and the negative suite, not a mechanised link. The external third-party audit (ROADMAP Step 12) was removed from the plan by the maintainers in September, so the trust claims are verified by us and by CI, which the live TRUST.md dashboard tracks. And performance is not at Go's on every benchmark cell; the per-cell matrix and ceilings are public.

Since rc3: the type system tightened in four places

Two of these are in the 1.0.0 tag: the clock capability and per-type generics. The other two, implicit flow and the trait-bound fix, landed on main the day after the tag and ship in 1.0.1, the first patch release. They are described here because the 1.0.0 tag is what you install today and main is what you read, and the difference should be stated rather than discovered.

Implicit flow is a compile error (E0331). The taint differential above did its job before it was green. On its first run, 83 of 300 generated programs disagreed between model and compiler, all accepted by the shipped checker and rejected by the model, and every one was an implicit flow: if secret: out = "a" followed by print(out) compiled. Two reasons, each sufficient on its own: pd == q typed as a plain bool, so the operator dropped the tag, and the checker had no program counter. Now an operator's result carries every tag of its operands; if, while, match arms and a for over a tagged iterable run under a program counter; and under a tagged counter a write to an untagged variable, a call to an effectful function, a spawn, an untagged return or a break out of an untagged loop is refused. Measured across every file in the tree before and after: seven new diagnostics, all real. 300 of 300 and 2,000 of 2,000 generated programs agree.

The clock is authority. time_now_ms, time_now_seconds and time_sleep_ms take Cap<Time>. The ambient twins are confined to std.cap_time and are E0404 anywhere else, exactly as entropy already was. A function that reads the clock without a capability in scope is now visible in kern audit-caps, which is the point.

Trait bounds were dead code. The call-site check looked for a one-letter parameter type name; since a September rename a generic parameter's type carries a marker instead, so the guard was false for every call and a bounded generic accepted any argument. It hid because the two gates that would have caught it ran only in make verify-release, which nothing ran automatically, so v1.0.0 was tagged with both red. Both are release-gates steps now, and a new check fails when any verify-release member is run by nothing in CI.

Generics that compare their own type parameter are compiled once per type. A comparison on two erased generic operands used to segfault for an inline-packed int, so it had been refused as E0330 and the stdlib carried _int twins. The typechecker now records which type each parameter takes at every call and emits one specialisation per binding; every other generic stays erased. any_eq, all_eq, count_eq, list_contains and list_count are generic, and their _int twins are the first deprecations under the new policy, with replace: so kern fix does the rename.

The trusted base got smaller, and is now sorted by kind

The JSON parser left C. 221 code lines out of the protocol class, the hand-written parsing of untrusted bytes that the threat model names as the largest single concentration of risk. It was not a like-for-like port, and refusing to make it one is the result. The C builtin was declared to return a map and returned whatever the top level happened to be, so json_decode("[1,2,3]") parsed and the first map operation walked a list as a map: exit 139, reachable from the network through the service dispatcher. The C fuzz harness had run 97 million executions under AddressSanitizer over that parser and was clean, because it called the function and never used the result as its declared type promised. The Kern decoder is total and strict; the harness is deleted rather than left calling a stub. The multipart parser followed it out.

With that, runtime/TCB_BUDGET stopped being one number. Every trusted C file now declares its dominant role (substrate, protocol, platform, binding, migratable, asm), scripts/tcb_split.sh sums them, and make check-tcb-split fails when a file has no class or the per-class sums stop reconciling with the budget. A hand-rolled HTTP parser reading attacker bytes and a thirty-line wrapper over libsodium used to count as the same kind of trusted; now a reader can see which lines carry risk Kern owns and which carry risk that lives upstream in mbedTLS or libpq.

Also in this cut

• Packages cross repositories. kern-pkg publish packs and uploads from the file, update records a real SHA-256, install checks the checksum, the pinned signature and that the archive names the locked package before moving it into place, and the compiler resolves a dotted import into kern_modules/<name>/src/. None of it had worked before; a gate runs it end to end against a loopback registry.
• Two builds of one program are byte-identical. An adopter reported kern cloud --rebuild produced a different binary every time. The IR was deterministic; the link was not, twice: the pid in a temporary link name, and a macOS link without -g keeping a debug map that pointed at a deleted file. Gate 64 builds twice and compares bytes.
• A signed JWT whose payload was a JSON array never expired. The lookup for exp answered the way an absent claim answers, so a valid signature alone was enough. Found by writing the test that asserts the documented error code for each failure, which is also why every bare error string in the stdlib is now a coded error and the ceiling is zero.
• kern desktop is the Docker Desktop equivalent, served from the one binary on loopback with three independent controls (a loopback Host header, same-origin fetch metadata, a per-run token), because a management port for a container runtime is the most dangerous local port a developer machine opens.
• Rootless containers map the user's subordinate id range, and a non-root host agent holds a container to its disk through a privilege-separated mount helper, the smallest root process that closes that gap.
• The cloud control plane gained four-eyes approval on destructive actions (the self-approval refusal is the feature), durable volumes, snapshots, revocable SSH keys, tenant DNS zones, firewalls on the instance's own bridge port and a web console into a running instance.

By the numbers

• 1,826 tests at 100% pass, 1,423 conformance and 403 negative; both gates CI-blocking
• 50 CI gates, enumerated by make gates-list from the workflow file itself, so the local command cannot fall behind the pipeline
• Ten of eleven trust-roadmap steps done and gated; Step 11 has three fragments proved and the model-to-compiler correspondence open
• 0 compiler binaries published; release tags and artefacts signed with keys pinned in the repository
• 428 stdlib modules, 4,738 public functions, 13 capability modules
• 56,923 lines of Kern in the self-hosted compiler (13 files, all self-hosting), 64K lines in the C runtime, about 40K of it the budget-gated trusted computing base
• EUPL-1.2, hosted on Codeberg, PUA Group (The Hague) as maintainer of record

curl -fsSL https://kern-lang.eu/install.sh | sh