the problem
The world is not a tidy variable
Why the core is not enough
Inside the core language, state is data the program owns: you can read it, overwrite it, and — crucially —
reset it. The real world offers none of that. The moment a program has to act on something outside itself,
three things break at once:
no undoYou cannot un-click a button. A click that landed wrong may have opened a dialog, joined a call, or written a row — and the next attempt inherits it.
it movesThe world keeps changing while the model thinks — and thinking takes seconds. You may judge a screen that is already gone.
act ≠ knowDoing something to the world tells you nothing about the result. You must look again, separately, to find out what actually happened.
The root of it
The core’s retry works by re-running from a saved starting state — fine
when the state is yours to snapshot. You cannot snapshot a live desktop, a production database, or another
person’s browser. So the extension is not new logic; it is the discipline for touching something
you cannot take back.
the fix
Four new verbs
Core idea
The extension keeps the entire core unchanged and adds a small vocabulary for touching the world
(shown in a different colour, because it really is a
new layer):
actPerform an effect — a click, a keystroke, an upload. Its datasheet is a delivery promise (“did it land?”), never a claim about the resulting state.
observeTake a fresh reading of the world — a screenshot, a database row, a waveform — the thing a judge or check then runs on.
settle … withinKeep looking until the state you want appears — or a real-time deadline passes. A principled wait, not a blind fixed sleep.
world retryA retry that must declare what re-running is allowed to disturb, or carry a compensate that cleans up first (below).
Why act promises so little
It looks strangely modest: act’s datasheet says only “the click landed,” never
“it worked.” That modesty is the extension’s first discipline, and it exists because of how agent code
fails in the wild: somewhere between two lines, “I sent the request” silently becomes
“the request succeeded.” Kimiya makes that inference unwritable. Doing and knowing are severed
by the grammar itself: after an act, the only way to learn what happened is to
observe and then judge or check the observation — at that instrument’s measured
rates, like every other claim in the language.
The one door
That makes observe the only door through which world-truth enters a
program. No construct reads the world directly; the world is sampled into an observation, and every
judgment runs on the sample. Two rules keep the door honest. Freshness: the moment you act on
a surface, every earlier observation of it is stale — and using one (say, clicking coordinates found
on an old screenshot) is a type error, caught before any model runs. Attribution: an
observation carries its origin, so a certificate can always say which reading a claim rests
on. Look, then touch, then look again — the grammar will not let you skip the third step.
in code
Find, act, then settle
A single interaction — click a button and wait for the result to appear — reads like this:
a := observe screen<A>() -- fresh pixels + their origin
hits := select<0.97>("the Create Group button", a) under k_ui by L
b := first(hits) -- centre, absolute coords
act<A> screen.click(b.x, b.y) -- delivery verified
settle<A> until check group_exists("W3 Harness Group") within 12
a2 := observe screen<A>() -- look again, after the world moved
if judge<3,2/3> shows(a2, "a success view with a join code") under k_state panel [J1, J2]:
…
Reading it
Observe the screen; find the button with select — which must now name
which model looked (by L) and under what purpose, because
locating a control is an instrument reading, not a string match; click it with act;
then settle — wait, eyes open, until a kernel fact confirms the group exists, giving up after
12 seconds rather than guessing a fixed pause. Only then take a fresh observation and put the
judged question to it, with a sighted two-model panel. Every one of the old verbs is still doing its
job exactly as before — the new verbs only decide when and how the world is touched and
looked at. And this is not pseudo-syntax: the lines above are the language as it runs today.
the hard part
Retry, when you cannot undo
The trickiest verb is retry. In the core, a failed attempt is simply erased and re-run from the start. In
the world, a failed click may have already changed something, and the next attempt starts from that mess.
So a world-frame retry must declare one of two things about its body:
invariantRe-running leaves the world within a stated boundary: trying twice is as safe as trying once (“idempotent up to” that boundary).
compensateOr the body carries a clean-up action that restores the boundary before the next try — the formal version of “leave the call, then rejoin.”
Key insight
A body that quietly mutates the world outside its declared boundary is a type error
— caught when you write the program, not a surprise in production. That is the same spirit as the core’s
ban on silent equality: the dangerous move is made impossible to do by accident.
What the premises buy — and what dropping them costs
Here is the remarkable part, and it is a theorem, not a design hope: pay those premises, and the
certified reliability of a world-touching retry is the exact same formula as the core’s retry —
the world adds premises, not penalty. And the premises are load-bearing, which is also machine-checked,
by counterexample: take a program that satisfies every condition except cleaning up between
attempts, and its certificate claims a 3-in-4 success rate while the program actually delivers 1-in-2 —
each failed try wrecks the ground the next one stands on, and the arithmetic quietly assumes it didn’t.
The declarations are not paperwork. They are exactly the price of a world without undo — no more, and
provably no less.
and time
Never judge a state that has already gone
The model takes seconds to look; the world keeps moving. Judge a screen mid-animation, or while audio is
playing, and you read a state that no longer exists. That is what settle … within δ
is really for: keep observing and judging until the state holds still, or a real-time deadline passes —
with the deadline counted as a genuine cost, right beside the call budget.
The mechanism — verdicts arrive late
Watch the clock closely and the problem sharpens. A judgment samples the world when it starts
looking, and its verdict lands seconds later — so every verdict speaks about the past. Usually
that is fine: the dialog you judged is still there when the “yes” arrives. But now imagine a state that
flickers faster than the judge can look — gone by the time each verdict lands. Give that judge a
perfect datasheet: it never misreads a sample, α = 0, β = 1. It will accept
every time, and be wrong about the present every time: error 0 on the sheet, error 1 in
the world. No datasheet can save you, because the datasheet speaks about sample time and the claim is
about verdict time. (This, too, is machine-checked — perfect instrument and all.)
Its obligation is therefore a stability promise: only settle on a state the world will hold
for at least as long as the judgment takes. Under that promise, two more things are theorems rather
than hopes: a settle can never go silent — it commits or visibly abstains within its deadline,
by construction — and a verdict-time error is priced at the instrument’s measured rate, like every
other claim in the language. No amount of judging can certify a claim about a state that vanishes
before the judgment finishes — so the construct forbids you from trying.
no longer a proposal
The verbs grew hands
What changed
When this page was first written, the extension was a careful design. It is now an implemented
language: an interpreter and a compiler run everything above against a real desktop — clicks
delivered by OS-level input, screenshots read by a vision model, certificates computed rather than
derived by hand. Implementation forced the design to say several things more precisely:
click · confirmWhether a click can be undone depends on whether the pixel under it says Cancel or Delete forever — no grammar can know. So the program states its own claim: screen.click is recoverable, screen.confirm is the same click declared irreversible — and the checker then demands a verified gate in front of every confirm, before any model runs.
type · pasteTwo ways to enter text: type synthesizes keystrokes (ASCII-safe, quietly drops some accents), paste goes through the clipboard so UTF-8 arrives verbatim — the one side effect being that it replaces the clipboard, which the program must own up to.
delivery, verifiedThe first live run found why a delivery rate is not enough: on an L-shaped multi-monitor desktop, a click sent into the dead corner is silently moved by the display server to the nearest valid pixel — delivered, somewhere. So every pointer move is read back, and divergence is refused, not averaged.
actorsDeclared seats: display A: names a monitor, another X server, or another machine over ssh; act<A> and observe screen<A>() index them. Each seat is its own coordinate space and its own freshness world — a box found on B's screen cannot produce a click on A's.
sighted judgesA select over a screenshot must name its instrument and purpose; a judge panel voting on a screenshot must be able to see it. A text-only model on a vision panel is a type error — it would answer about an image it never saw.
exact · replayCached locates come in two honesty grades. An exact hit (same screenshot bytes) is a reading of this very image — free, silent. A replay (pixels changed, coordinates reused) is an assumption the certificate counts and discloses — sound only because a locate gates progress, never the verdict.
observe imagePhotographs, scans, and diagrams enter the same way screens do: as content-addressed observations (SHA, dimensions, decoder), re-verified before every model call — a file that changed after observation aborts, never silently ships stale pixels. A raw path handed to a model is a type error; pixels pass through the observation door or not at all. (v1.5)
the screen-readScreenshots feed gen directly — gen<Reading>("Read the join code shown", images=[observe screen<A>()]). Reading a value off the display, the last construct of the original design still on paper, is now a declared, vision-gated generation over an explicit observation; routed to a remote generator, the certificate discloses whose seat's pixels left the machine. (v1.5)
the priced readA reading the program goes on to use is a claim about the world, so it must be paid for. A gen that consumes images now contributes one θ factor at its instrument sheet's conservative end, under a declared purpose — gen<Reading>(…) under k_read; leave the purpose off and the read is priced at the untrusted prior grade, and the checker says so. Text-only gen stays factor-free. Programs that read screens now certify at a lower θ than before — which is the direction an error bar should move when a cost was being ignored. (v1.6)
the measured readA price needs a measurement behind it. The screen-read was put through a campaign over the real path — observe screen → gen → the vision model — against rendered screens with kernel-grade ground truth: 60/60 exact reads, 0/20 false reads on screens with nothing to read (β ≥ 0.9398, α ≤ 0.1611 at 95% confidence; median 6.6 s). The result ships as an installable datasheet with its provenance — model, seed, date, every trial — embedded in the sheet itself. (v1.6)
The number that moved
The same two-user program, run twice: against prior-grade instrument sheets it commits at
θ = 0.047, warning that the declared recall overclaims what the instrument has been
shown to do. Install the testing tool's measured datasheet — one command, which refuses a
sheet with no provenance — and the identical program commits at θ = 0.86. Both runs
pass. They are not equally strong evidence, and the certificate is the artifact that says
so.
One more disclosure the implementation insists on: a screenshot shipped to a remote model is not a
prompt the program composed — it is whatever happened to be on the display. Programs that capture the
screen and use remote agents announce, before anything runs, that those captures will leave the
machine.
the payoff
The guarantee half is untouched
Key insight
Only how you touch the world is new; how you prove reliability is exactly the
core. Purposes, the judge-versus-check grade split, the reliability invoice, abstaining (✠) when
the budget runs out — all identical. A program that drives a live cloud still hands you the same auditable
certificate as the summariser from the tutorial.
That is why the extension can be small: it adds a way to reach into the world, and changes nothing about how
trust is accounted for once you are there.
a true story
Built without the theory — and it was the theory
Φ built a testing tool that drives a real, deployed app — a
desktop program, two live browsers under different logins, real audio across a voice-chat mesh, a dying
network, and a production cloud — all from one fixed script, with a vision model used only to
perceive, and hard database and audio checks at the end.
On eighteen tests it found ten real bugs that a normal 65-test suite had missed — three of
them invisible on screen: a counter that lied, a feature with no code behind it, and a database failure
returning an error to every logged-in user.
The twist: it was built without knowing Kimiya — and then turned out to be a Kimiya
program. Its element-finder was select; its screen-checks were
judge under implicit purposes; its database and audio oracles were the trusted
check kernel; its flaky-interaction handling was world-frame retry with compensation,
improvised by hand.
Why it almost never lied
The theory even explained the tool’s safety record: because every test ended in a check, a
mistaken glance could only waste a retry — it could never fake a green. That grade separation, discovered
by engineering instinct, is exactly Kimiya’s central safety property.
a real program · not a toy
A whole afternoon of a life, as one script
Here is a program in the running language that drives a live browser across four sites — watching
videos, following accounts, posting a tweet, logging a film review — the way a person would. It is a
function library plus a data-driven driver: to run a different day, you edit the lists at the bottom.
Two of its functions cross the line of no return (a public tweet, a public review); the rest are
recoverable. Watch how the language keeps the two apart.
A recoverable action — no gate needed
-- follow an account: clicking Follow can be undone, so no confirm.
fn follow(handle):
-- … open the X tab, navigate to the profile …
s1 := observe screen("eDP-1")
bs := select<0.95>("the Follow button", s1) under k_ui by L
if check(len(bs) > 0): -- degrade gracefully: no button, skip
b := first(bs)
act screen.click(b.x, b.y) -- a plain click; nothing to gate
return "followed"
else: return "skip: already following"
An irreversible action — the gate is mandatory
-- post a tweet: a public artifact that cannot be un-posted.
fn post_tweet(text):
-- … open X, click the composer, paste the draft …
s2 := observe screen("eDP-1")
ps := select<0.95>("the blue Post button", s2) under k_ui by L
if check(len(ps) > 0):
p := first(ps)
if judge<3,2/3> shows(s2, "a non-empty typed draft")
under k_state panel [J1, J2]:
act screen.confirm(p.x, p.y) -- fires ONLY past the judge
return "posted"
else: return "abstain: composer empty"
else: return "skip: no Post button"
The driver — edit these lists to run a different day
follows := ["perfumegenius", "100gecs"]
tweets := ["no thoughts only akerman", "réveil 14h je suis détruit"]
forall h in follows: print follow(h)
forall x in tweets: print post_tweet(x)
What the language is enforcing here
The recoverable follow ends in an ordinary click. The
irreversible post_tweet ends in confirm — and the
checker will not compile the program unless that confirm sits behind a gate, here a two-judge
shows that the draft is really there. Because both judges are the same model
that could have written the text, the panel is self-referential (J ⋪ C
is violated), so every posting judgment is stamped UNCERTIFIED in the invoice — the
program runs, but it never pretends the check was independent. And every function
degrades gracefully: a missing button returns "skip:…" rather than
aborting the batch, because a world-effecting program has no clean resume.
case studies · the extension on real problems
Two problems that need these verbs
honest status
Newer than the core
One straight answer, in the spirit of the rest of Kimiya: the core language is machine-checked in Coq —
and now, so is this layer. Every obligation on this page is a theorem: the world-frame retry certifies at
exactly the same reliability expression as the core's retry; settle can never go silent (its
deadline totality is proved, not promised) and its verdict-time error is priced at the instrument's rate;
the gate bounds an irreversible act's false firing by the guard's grade; the read costs one factor,
priced once. Each theorem travels with a machine-checked counterexample showing its premise is
load-bearing — drop the compensation, the stability, the gate, or the price, and a perfect
instrument fails — and the constructs are then integrated into one extended proof system with a single
soundness theorem. What remains younger here is maturity, not grade: the extension's instrument model is
newer and less battle-tested than the core's, and remote-machine seats are tested only up to the point of
the command they would send. Say plainly what is proved, what is enforced, and what is neither.
Back
← Return to the tutorial
The core language: purposes, the three verbs, verified retry, the reliability invoice, the
Goodhart boundary, and where Kimiya came from.