The Invariant Gate: Checks That Run, Prose That Gets Judged

Every codebase has rules that live in prose. Ours live in CLAUDE.md — “no fallbacks,” “emit for, never while,” “a claim stamp stays honest” — and until recently they were enforced the way prose rules always are: by a reviewer who happened to be paying attention, or by nobody.

std/invariants already took the first step out of that arrangement: a rule stops being a comment and becomes a declaration — a name, tags, the prose itself, and an optional check: field, enumerable by koruc:

import std/invariants

std/invariants:inferred {
  "name": "comment-language",
  "tags": ["git-gate"],
  "rule": "Comments are written in English, not Norwegian."
}

The declaration is data in the AST, not a step in the flow — it costs the program nothing and cannot execute. The disposition is carried by the name itself: inferred means permanently reader-checked, so growth is healthy; aspirational means the rule intends to become executable, so growth is debt. Nothing but the name distinguishes them, and nothing else needs to:

A gate is a consumer, not a subcommand

The listing command takes no arguments, and that refusal is the doctrine: koruc <file> invariants gate is rejected, because a gate is a consumer of the listing — a script over enumerable rows — never a flag the compiler knows about:

This week that consumer landed, at the commit boundary: invariants/gate.py, wired into the pre-commit hook. It reads the listing, and each row chooses its own execution strategy off the declaration itself — check: means a deterministic checker exists and runs; its absence means the rule is judgment-class and goes to a reader. The decidable get scripts; the readable get a model.

The judgment class finally has an executor

All three deterministic invariants already carried check: fields — and two of them were effectively orphaned: declared, executable, and run by nothing. The prose-only invariant space was empty for the same reason: nothing could execute a judgment-rule until koru/odds existed. A real judgment row looks like this — the rule text written to be the question, diff-scoped and verdict-shaped:

std/invariants:inferred {
    "name": "no-fallbacks",
    "tags": ["git-gate"],
    "rule": "Does this diff introduce a fallback — a degraded path a reader
        would mistake for the real surface working? A fallback is: a default
        value substituted for a failed fetch or computation, placeholder
        output standing where real content belongs, a swallowed error
        converted into a silent skip or empty result, or a second code path
        labeled 'for now', 'minimum', 'if X fails', or 'fallback'. Designed
        states are NOT fallbacks: an empty state that says it is empty, a
        documented default parameter, an idle pose, a named and tested
        degraded mode. Answer yes ONLY if the diff adds or keeps a
        substitute output that hides the real path's failure or absence."
}

A second row, claim-stamps-stay-honest, covers std/rules: claim stamps (proven, measured, inferred, aspirational) are inline in the diffed source, so “did this diff weaken a declared claim silently?” is diff-decidable — a flag for a claimed declaration edited away from its evidence. A direct claims/assumes census consumer remains the deeper version if the question proves too shallow.

The judge program is nine lines

The reader is a compiled Koru program — invariants/gate.k — that takes a question and a state on argv and prints exactly one verdict line:

import koru/odds
import std/args
import std/io

std/args:get(index: 1)
| arg q |> std/args:get(index: 2)
    | arg s |> koru/odds:judge(budget: 3): j |> koru/odds:feels(j, text: s, question: q)
        | yes p |> std/io:print.ln("VIOLATION p={{ p:f }}")
        | no p |> std/io:print.ln("CLEAN p={{ p:f }}")
        | exhausted |> std/io:print.ln("UNJUDGED fuel exhausted")
        | err e |> std/io:print.ln("UNJUDGED {{ e.msg:s }}")
    | out-of-bounds |> std/io:print.ln("UNJUDGED missing state arg")
| out-of-bounds |> std/io:print.ln("UNJUDGED missing question arg")

The whole judgment contract is the one that already exists: feels is the noul — | yes f64 | no f64 — and the branch names are the answer space. judge issues a live judge against the model, and it is the only backend the library ships: an earlier draft of the gate could swap in judge.mock, a deterministic hash wearing the same *Judge<greedy> type, and we cut it — a mock in a library is a wart, and a hash verdict that reads like a judgment is exactly the substitute surface the gate exists to refuse. Offline, the honest answer is UNJUDGED, not a verdict-shaped hash. Testing an odds consumer needs no library mock at all — the language already has the seam: test() blocks substitute any invocation with a branch constructor (koru/odds:feels => yes 0.9), so the judge’s issue–ask–retire lifecycle runs real and only the network ask is scripted. UNJUDGED is the load-bearing verdict: no key, no fuel, no args — the loud form of “the gate could not judge,” never a silent pass. The runner treats it accordingly: advisory normally, blocking under GATE_BLOCK=1, because enforcement mode cannot let an unjudgeable row slide.

Real output — the gate judging its own commit, the hook’s first production run:

check ok    emit-for-not-while
check ok    call-valued-index
judge ok    no-fallbacks  CLEAN p=0.97
judge ok    claim-stamps-stay-honest  CLEAN p=0.99
gate: 4 row(s), advisory — clean

The same diff had read CLEAN p=0.98 minutes earlier at staging — live judgments float slightly, which is exactly why the verdict carries a probability rather than a boolean.

Two properties of the enforcing posture are worth stating plainly, because they are the strangest true things in this post. You cannot commit without an API key. Every commit in every repo that compiles Koru requires a live judgment path — no key, no fuel, a dead endpoint → UNJUDGED → refused. That is either the point or the insanity, and it is the same thing: the discipline costs a live model call per commit, paid or blocked. And git commit --no-verify is part of the design, not a loophole — Jev is a harsh judge, not an infallible one, so the human override exists and is loud by its absence: a commit that bypassed the gate lands with no verdict in its history at all. A gate that could not be bypassed would teach people to remove it; a gate that can be, teaches you when it was wrong.

The gate found work for the compiler

Wiring the gate meant making the declared checks actually pass — and emit-for-not-while was red: twenty flagged sites plus three stale exemptions whose fingerprints still pointed at store.kz after part splits had moved the code. The check did its job twice over — it caught both the drift and its own rotting exemptions.

Clearing it converted three counted while emissions to for: kernel’s parallel-worker loops, io’s chunked writer, and supervisor’s bounded restart: N loop. The supervisor conversion surfaced two honest constraints in the generated code. A for range bound must be usize, so the emitted loop casts the budget — safe, because restart is enforced a positive literal at the transform. And the loop must not fall through: the __left countdown guarantees a return by the final iteration, but Zig cannot see that — so the emission ends in unreachable, which is not a fallback but the assertion TigerStyle prescribes for a loop that cannot legitimately exit:

var __left: i64 = 3;
var __arg_n = n;
for (0..@intCast(__left)) |_| {
    const __r = main_module.worker_event.handler(.{ .n = __arg_n, });
    switch (__r) {
        .ok   => |v| return .{ .ok = v },
        .boom => |f| {
            __left -= 1;
            if (__left <= 0) { return .{ .boom = f }; }
            __arg_n = f + 4;
        },
    }
}
unreachable;

A reader who finds that unreachable firing has found a real bug — which is the point of writing it down instead of letting the function’s end imply one. The payload-argument supervision path that exercises this emission is pinned by 320_154_supervised_transform_payload_args, green in the suite.

Rows can live in the files they guard

A git-gate row judges the whole staged diff. A git-gate-local row is colocated — declared inside the file it guards — and fires only when that file is staged, judged against that file’s hunks alone. The scoping needs no new syntax: the listing already prints each row’s loc, and a declaration’s location names the file it guards for free.

std/invariants:inferred {
    "name": "single-judgment-surface",
    "tags": ["git-gate-local"],
    "rule": "Does this diff add a second judgment implementation to
        koru/odds — a deterministic, hash-derived, canned, or otherwise
        offline path that emits verdict-shaped output without a live ask?
        ... Answer yes ONLY if the diff adds or restores a substitute
        judgment path inside the package."
}

That row lives inside koru-libs/odds/index.kz — in a different repository. The gate resolves each local row’s file to its own repo and reads that repo’s staged diff, so the odds package carries its own guard against mock backends returning, and it fires on koru-libs commits. A local row whose file is not staged did not fire: local skip, never UNJUDGED. And the manifest guards itself — manifest-stays-enforceable asks whether the diff weakens the declared discipline, judged exactly when the manifest changes. Both rows measured live on their own commits: CLEAN p=1 and CLEAN p=0.99 on the diffs that added them.

What is still open

The honest residue. The posture flipped to enforcing early — the gate now runs GATE_BLOCK=1 in the pre-commit of every repo that compiles Koru (koru, koru-libs, orisha, koru-examples, korulang_org), which makes UNJUDGED blocking too: a dead judgment path stops a commit rather than advising past it, and the key provisions from one canonical file outside every repo. What that buys in discipline it pays in exposure — a false-positive now halts work, so the hit rate gets measured in commits refused, not advisories ignored. The model string floated with the judge release — it now pins typesafe/jev-1.13-20260917, so “gated by Jev” names which Jev. And the third question-source is designed but unwritten: judging added comments for checkable claims — prose that states a fact about the system a test or declaration could carry — with aspirational and owed as the discharge path it routes into.

What is not open is the shape. The interesting thing here was never “a model reviews commits” — it is that the rule corpus was already declared, enumerable, and dispositioned. Jev plugs in as the missing executor for the judgment class, and the same runner finally gave the deterministic checks a voice. The rules stopped being prose a reviewer had to remember. They are rows now, and rows get read.