The reference · the parts that hold still
The tutorial and the extension explain why; this page is the what — the parts of Kimiya that hold still. The living detail (backends, flags, release notes) ships as a README inside the download below.
get it
Current release — v1.6.0 · pre-stable
One archive, no build step, no account, no network: unzip and run. Python 3.11+ is the only requirement. The mock oracle — a deterministic stand-in for the models, so runs need no network and always reproduce — lets you exercise the whole toolchain — parser, checker, type checker, compiler, a full run with a certificate — before any model is installed.
≈ 110 KB · zip
kimiya-lang.zip ↓
The interpreter and compiler, the examples from these pages, the test suite, and the full README. Pure-stdlib Python — nothing to install.
≈ 2 KB · zip
vscode-kimiya.zip ↓
Syntax highlighting for .kim files — core keywords
in blue, the world extension in magenta, matching these pages.
First run — about a minute, no models, no network
unzip kimiya-lang.zip && cd kimiya-lang python3 -m kimiya check examples/grounded_summary.kim -- static checks only printf 'Deadline moved to Friday.\n' > notes.txt -- the example summarizes notes.txt KIMIYA_MOCK=1 python3 -m kimiya run examples/grounded_summary.kim -- prints a certificate: status COMMITTED, θ (the certified -- reliability, §4), cost, egress: none
The editor extension
unzip vscode-kimiya.zip cp -r vscode-kimiya ~/.vscode/extensions/
Previous versions — the archive
Every release stays in the archive, so a result produced under an old version can be
reproduced under exactly that version (each certificate names the version that made it).
The CHANGELOG lists every version and
flags every break — so far: v1.2.0 (compiled artifacts' model list moved to
--models) and v0.8.0 (locate coordinates changed to image
pixels). Listed here are the milestones; any other release is one predictable address away
(downloads/archive/kimiya-lang-vX.Y.Z.zip).
v1.6.0 (current) · v1.2.0† · v1.0.0 (the 1.0 cut) · v0.8.0† † introduced a breaking change
§1 · the shape of a program
Comments are --; indentation is significant (spaces).
Magenta productions are the
world-effecting extension; everything else is core.
program := (decl | stmt)* decl := pool NAME = STRING | param NAME: (text|num|bool) [= literal] | display NAME: (x11|ssh|monitor = STRING)* | agent NAME: (backend|model|url|key_env|family|vision = …)+ | context NAME: (domain|preserve|allow_loss = …)+ | schema NAME: (field: type)+ -- types: text · num · bool | effect SURFACE.ACTION (irreversible|recoverable) | fn NAME(params): BLOCK | use "lib.kim" | use python "helpers.py" | pyfn name = "pkg.attr" stmt := NAME := rhs | check E | print E | commit(E) | abstain | return E -- inside fn only (K9) | if GUARD: BLOCK [else: BLOCK] | forall NAME in E: BLOCK | explore: BLOCK -- new in v1.3 | retry budget N until GUARD: BLOCK [inv E] [compensate: BLOCK] | act[<ACTOR>] SURFACE.ACTION(args) | settle[<ACTOR>] until GUARD within SECONDS rhs := [memo] gen<SCHEMA>(E [, images=E]) [under CTX] [by POOL] -- memo: v1.3 · images: v1.5 (image observations -- OR screenshots) · a gen with images is a PRICED -- READ: one θ factor under read:<CTX> (v1.6) | select<RECALL>(E, E) [under CTX] [by POOL] | observe (file|image)(E) -- image: new in v1.5 | observe screen[<ACTOR>]([NAME | x,y,w,h]) | retry budget N until GUARD: BLOCK -- assignment form: yields the accepted value; -- exhaustion abstains (✠) | E GUARD := check E | [memo] judge<K,TAU> (E |= E | E ~ E | E contradicts E) under CTX [panel [P,…]] [paraphrase_prompts N] | judge<K,TAU> shows(E, E) under CTX [panel [P,…]] [paraphrase_prompts N] E := NUMBER | STRING | true | false | null | NAME | NAME(E, …) | E.NAME | E[E] | [E, …] | -E | not E | E (+|-) E | E (==|!=|<|>|<=|>=) E | E (and|or) E | observe … -- observe is itself an expression: a fresh -- reading may sit inside any E — including a -- settle guard, which then re-observes per poll BLOCK := NEWLINE INDENT stmt+ DEDENT -- an indented statement sequence, -- as in Python; it always follows a “:”
Lowercase names (program · decl · stmt · rhs · GUARD · BLOCK) are defined
here; the remaining UPPERCASE names are metavariables: NAME an identifier,
STRING a quoted string, N and
SECONDS numbers, E an expression (its production is
above — note the arithmetic is deliberately just + and
−),
SCHEMA / CTX / POOL /
P / ACTOR the name of a declared schema, context,
pool-or-agent, panel member, or display, RECALL a number in (0, 1]
(K3), and K,TAU the panel size and vote threshold (decoded below).
Reading the declarations
pool A = "llama3.1:8b" names one model on the default local backend. The name is how the program refers to the seat — by A says which instrument performs a gen or select, panel [B, C] convenes seats as voters — and --models overrides the declared models at run time. Seats from different model families are what make cross-provenance panels possible (K2).vision for sighted instruments. A pool line is shorthand for an agent on the local default.act<A> and observe screen<A> index it; each display is its own coordinate space and freshness world (K13).gen must produce — named fields with types — so a draft is at least well-formed before anything judges it (K7).name=value on the command line, resolved and refused before any model runs, and recorded in the certificate.Reading the judged forms
judge<5,4/5> asks five times and accepts on four agreeing. The datasheet cited is that of this exact configuration, panel included.select<0.95> requires an instrument whose measured recall is at least 0.95 — a promise about what was not returned.Surfaces and their effect classes
Two productions above — act SURFACE.ACTION(args) and the
effect declaration — lean on a vocabulary of their own. A surface is
a region of the world a program may touch (with act) and look at (with
observe); the language ships two. Every action on a surface carries an
effect class: recoverable — a later action can walk it back — or
irreversible — nothing can. The class is not decoration; it is what the checker keys on:
K4 bans irreversible actions inside a retry body, and K5 demands a verified gate in front of every
one. The defaults below can be re-declared per program with effect, because
whether an action can be undone is a fact about the application, not about the grammar.
create · append · mkdir recoverable; overwrite · delete irreversible.click · type · paste · key · drag · scroll recoverable; confirm irreversible — the click that commits. Classes can be re-declared per program with effect.Builtins: len contains starts_with lower trim lines join str num hash now
range first last keys file_exists map filter sort_by sum. Functions see only their
parameters; modules (use) are pure declarations; Python extensions
are kernel-grade — trusted like check, certainty 1, no
instrument error — and announced by SHA: the certificate records the extension
file's hash, so an audit can see exactly which trusted code ran.
§2 · what the checker refuses
Every rule rejects a program before any model runs, each with a one-line diagnosis. This table is the checker's contract; the test suite holds one deliberately ill-formed program per rule and asserts it fails with the right message. (Refusal is not the checker's only voice: it also warns without stopping — a declared recall that overclaims the instrument's measurement, or a priced read with no declared purpose, runs with the warning printed and the certificate degraded, not refused.) Rules are numbered in the order they entered the language, which is why the core K14 follows the extension's K10–K13.
J ⋪ C) — one family cannot certify its own output.select recall must lie in (0, 1] — a coverage claim needs a stated recall.check or judged gate must sit immediately before it (the verified gate).inv or compensate — snapshot retry over an external world is unsound.gen schemas must be declared (or the builtins Text/Json).return only inside a function.select over a screenshot must name its instrument (by) and purpose (under) — locating a control is an instrument reading.shows(…) takes a screenshot, and every panel member voting on it must be sighted.display, and only the screen surface has seats.commit and no irreversible act inside explore — exploration's factors are excluded from θ, and a verdict must not rest on unaccounted judgments. (new in v1.3)Beyond the numbered rules: duplicate declarations collide loudly; param
types and defaults must agree; and a gradual type checker catches shape bugs (field typos,
iterating a text, selecting over a non-list) with no false positives.
These are theorems in a checker’s uniform
Several rules enforce proved results, not house style. K2 is the self-judgment impossibility: no datasheet an instrument supplies about itself can rule out generator–judge coupling, so provenance separation is the only fix. K4 and K5 are the verified-gate results: an ungated irreversible act fires on a false premise at the generator’s rate — a number no judge’s sheet bounds — and inside a retry body even a perfect judge cannot help, because the act fires before the verdict lands. K6 is the world-frame premise: drop the invariant-or-compensate declaration and the certified retry bound provably fails. Each of these travels with a machine-checked counterexample showing what the rule prevents.
§3 · driving it
python3 -m kimiya check prog.kim -- parse + discipline + type checks python3 -m kimiya run prog.kim [name=value …] [--models m1,m2] [--replay] python3 -m kimiya compile prog.kim -- standalone prog.py (needs only the bundled -- runtime); same CLI contract as run python3 -m kimiya hl prog.kim -- highlighted source (--html for a page) python3 -m kimiya doctor -- are local models up, and are ≥2 model -- families present? (K2 needs them) python3 -m kimiya calibrate .kimiya -- label judgments; tighten datasheets -- (.kimiya = the run-artifact directory) python3 -m kimiya datasheet sheets.json .kimiya --source "…" -- install a measured instrument python3 -m kimiya --version -- the installed language version
For the search constructs (explore, memo) see
the search essay — they are the newest part of the
language and documented there until they settle.
The instrument lifecycle — what calibrate and datasheet are for
Every judged or locate task starts life at prior-grade: a deliberately conservative
default operating point, used when nothing has been measured — runs work, but certify little.
calibrate is the step up: it walks the trace of your past runs, shows
you each judgment the instruments made, and asks you to mark it right or wrong; your labels
tighten that task's α and β, and the instrument becomes calibrated. The top grade,
measured, comes from a purpose-built campaign: datasheet
installs a JSON file of externally measured operating points — and refuses any sheet without
a --source provenance line, because a number with no origin cannot be
cited. The three grades are exactly what the certificate's instrument
lines report (§4): same program, higher grade, stronger θ.
param — typed, checked, refused before any model runs, and recorded in the certificate. Same spelling for interpreter and compiled artifact.KIMIYA_MOCK=1 offline deterministic oracle · KIMIYA_SCREEN=none record acts, deliver nothing · KIMIYA_SCREEN_FIXTURE[_A] serve a recorded screenshot (per-actor) · KIMIYA_REPLAY=1 replay for compiled artifacts.§4 · what a run hands back
Every run ends in a certificate (printed, and written to
.kimiya/certificate.json) or a visible abstention — never silence.
── certificate ──────────────────────────────
status : COMMITTED
value : "W3 collaboration verified"
θ : 0.8081 (locate:k_ui 0.9746 ×4, shows:k_state 0.9763 ×2,
read:k_read 0.9398 ×1)
instrument locate:k_ui : ρ_r≥0.9746
[measured: GUI-test campaign, 58 runs / 343 locate calls]
instrument read:k_read : β≥0.9398 α≤0.1611
[measured: screen-read campaign, 60+20 rendered trials]
egress : api.anthropic.com (prompts left the machine)
screen : 8 act(s), 4 locate(s) (1 exact-cache)
actor : A → :0 (local) actor : B → user@lab :0 (ssh)
params : name='Ada', times=3.0
image egress : 1 observed image disclosure(s)
memo : 2 reuse(s) — identical readings, factors counted once
⚑ explored : 4 judged/select factor(s) inside explore — excluded from θ
kimiya : v1.6.0
cost : 2 gen, 6 votes, 8 acts, 6 observes, 74.2s
trace : 35 records (.kimiya/trace.jsonl)
commit), ENDED (ran out of program), or ABSTAINED — with the reason. A failed check, an exhausted budget, or a missed replay abstains; it never silently passes.task:purpose ×count: locate:k_ui 0.9746 ×4 reads “four locate calls under the program's k_ui purpose, each contributing its measured 0.9746.” Overclaiming is warned on every run.:0 is an X display number; user@lab :0 (ssh) is that display on another machine.none (observed pixels stayed local). (new in v1.5)explore — the search half of the invoice, so a reviewer sees what gated progress vs what backs the verdict. (new in v1.3).kimiya/trace.jsonl — what calibrate reads to tighten datasheets.How to read θ
Two runs can both commit and not be equal evidence. The same program commits at
θ = 0.047 on prior-grade sheets and θ = 0.86 with a measured datasheet
installed — the certificate is the artifact that says which one you have.
Kernel checks contribute no instrument error: any committing run
satisfies them with certainty.
§5 · where Kimiya sits
Kimiya was designed independently: the core is a program logic worked out on paper and machine-checked in Coq, not derived from any LLM framework — and every extension on these pages was added out of necessity, to enable one concrete capability the work at hand demanded. But no idea grows in a vacuum, and several technologies share a piece of the picture. Naming them precisely is the honest move:
| Neighbor | What we share | What Kimiya adds |
|---|---|---|
| DSPy / Assertions | Programs over LM calls, with constraints and backtracking retry. | Constraints are calibrated instruments, not pass/fail asserts: measured α/β enter a multiplicative certificate, and self-judgment is a type error. |
| LMQL · Guidance · BAML · PDL | A language/DSL for LLM calls with typed, structured output. | They structure the output; Kimiya warrants the claim — purposes, grade separation, θ, abstention. |
| LLM-as-judge calibration work | Judges as measurement instruments with error rates — shared intellectual ground, actively studied. | The rates live in the language semantics: datasheets install with provenance and multiply into each run's certificate. |
| Sagas · BPEL · Temporal | Compensation and retry over effects you cannot roll back. | The same discipline made epistemic: world-frame retry carries invariant obligations, and an ungated irreversible act is rejected at check time. |
| Playwright · Robot Framework | Deterministic UI scripts; auto-waiting resembles settle. |
Calibrated perception with a measured datasheet, and a verdict that never rests on perception alone. |
| Proof-carrying code | The idea that a program ships with its certificate. | Certificates of measured instrument reliability, not of formal proof — the honest grade for semantic steps. |
| Conformal prediction | Distribution-free guarantees on model outputs. | Composition: guarantees that flow through control flow, retries, and world effects into one number. |
scope
Status, plainly
Kimiya is under active development and versioned
(MAJOR.MINOR.PATCH; currently v1.6.0, pre-stable — the surface may
change between MINOR versions until 2.0). Every run's certificate records the version
that produced it (kimiya : v1.6.0), so results are always
attributable to a language state. Compiled artifacts are version-stamped and gate
themselves across incompatible MAJOR versions; every break is recorded in the
CHANGELOG, and every release stays
downloadable in the archive above.
Only the stable core is promised here: the grammar, the rules, the certificate's meaning — the rules table is the checker's contract. Backends, model names, flags under active development, and release notes live in the README inside the download — for those moving parts the README is the living reference, and where the two disagree on them, it wins.
Start here instead?
← The tutorial
Purposes, the three verbs, verified retry, the reliability invoice, and where Kimiya came from — the why behind everything on this page.