Claims on an app I use every day

2026-10-23Milestone 2, done

Yap is a small dictation app for the Mac: hold a key, talk, and the transcript is typed into the app in front. I use it every day. TodoMVC lived in one window; almost all of Yap lives outside its window, in a global key, the microphone, timers, a network request, files, sounds and typing into another app. The second milestone asked whether claims hold up there.

I rebuilt it on Cairn, signed it, installed it and used it for a day of real work.

What Cairn gained

Effects. The clock and timers, requests the host performs and answers, and outside inputs like a global key and the microphone. Lean decides; Swift captures audio, hears the key, makes the request and types the text, each because Lean asked.
New surfaces: a native menu bar menu built from Lean's view, and an overlay that never takes focus.
Packages. Moving Yap into its own repository made Cairn a package, with a cairn command and claim ids scoped by package. Yap's are yap^N.

What's proved about dictation

A key used in a shortcut never sends.
A transcript is saved before it's typed.
A late reply for an old clip never types.
Every recording ends.

The catch

Each new effect is an assumption about the host, fuzzed with slow, failed, duplicated and out-of-order replies, not proved. Audio and HTTP stay in Swift; Lean only decides what to do with the results.

Progress log

The videos and notes from this milestone as the work landed, newest first.

Try it: TodoMVC in the browser
Every frame is one the app's Lean code drew, explored ahead of time; each control shows its claim id, its reading and a link to its claim page.
2026-10-25a9813e523s
Cairn 0.1.3, on the public registry
Cairn 0.1.3 is out, and it is on the public registry at cairn.registry.nexthub.sh as iamnbutler/cairn, next to 0.1.2. Reading it needs no login: cairn add cairn finds the owner by name and writes the version range, and Lake fetches Cairn from the registry's git (#107, #109). /packages/ now reads the registry itself instead of sample data (#111).
The Cairn library is now only what an app links: 31 modules. Proofs, claims, fuzzing and tools are their own Lake libraries, so libcairn_Cairn.a went from 3.67 to 2.78 MB (#114). Three modules moved so the directories in lean/ have no cycles, and make lint now fails on one; the old names stay as shims until 0.2.0 (#110).
No claim changed, so it is a patch release. Yap moved to it with only its tag changed.
2026-10-24aea142c
Cairn 0.1.2: libraries and apps
Cairn 0.1.2 is out. A package is now a library or an app, as in Cargo: cairn.toml has kind = "lib" or "bin", cairn new asks which, and /packages/ lists apps under their own tab (#103). Nothing can depend on an app.
cairn publish sends no docs. HTML from a publisher would run as the registry's site, so docs will be built from the source instead, as docs.rs does (#98).
The ledger now treats retiring a released claim as a breaking change: it needs a new major version, or a new minor one while at 0.x (#100). No claim changed in 0.1.2, so it is a patch release.
2026-10-24597dea8
Cairn is a package, and Yap moved out
Cairn is now a package. An app lives in its own repository and depends on a tagged release, and one tag pins both halves: the Lean package and the Swift libraries. v0.1.0 is the first release (#80). v0.1.1 fixes cairn doc, which failed in apps because it read its stylesheet from the app (#91).
Yap moved out first. It lives in its own repository, yap-cairn, and depends on Cairn v0.1.0 like any other app would. Its Lean, proofs, fuzzers, Swift host and benches left this repository with it.
Claim ids are now scoped by package. Cairn's are cairn^N and Yap's are yap^N, so “a shortcut never sends” is yap^311. Cairn's claims.lock still lists Yap's old ids, marked moved:yap, so they can never be issued here again.
2026-10-24ea72e75
The cairn command and packages
There is now a cairn command (#79). cairn new starts a package in its own repository with its claim scope set, cairn add depends on another package, and cairn build runs Lake, links the Lean into one library and builds the Swift host. cairn doc writes the package's docs, and cairn publish and cairn login talk to a registry. It has unit tests, and it has been run against a stand-in registry but not a deployed one yet.
The registry is nextpm, a package registry, with a new cairn kind (nextpm #22). It has an index Lake reads natively, the source served over git, and a build cache, so that lake cache get downloads prebuilt Lean. Its claim ledger refuses a version that drops, renumbers or redefines an id. /packages/ shows a registry's packages, and until one is running it shows sample data (#78).
Publishers no longer upload docs. A registry now refuses HTML from a publisher (nextpm #23), and docs will be built from the source by a builder we run, the way docs.rs works (#94).
2026-10-24fb902c0
Developer docs and the API reference
Developer docs are up at /docs, laid out like Rust's bookshelf: the Cairn Book, Cairn by Example, reference pages, and guides to working on Cairn itself (#76). Every code sample is included from a source file that make check compiles, so a sample can't drift from the code it shows. Moving an included region fails the build until the page is fixed.
The API reference at /docs/api/ is generated by cairn doc, Cairn's answer to rustdoc (#77). It reads the Lean environment directly instead of using doc-gen4. On TodoMVC, doc-gen4 took 185 s and wrote 227 MB, almost all of it Lean's own library. Each claim appears on its module's page with its statement, evidence and proofs. A Lean block in a doc comment is a doc test that make check runs.
Every heading on the site also has an id now, and a # that copies a link to it (#72).
2026-10-24d04416c
Yap against the original under Instruments
Yap on Cairn was measured against the original Yap with Apple's Instruments rather than Cairn's own tools (#65). At 60 Hz the two overlays now pace the same, at 59.3 and 59.9 frames a second, with no hitches in either.
While recording, Cairn used 205 ms of CPU a second, against the original's 82. Most of that went to redrawing the menu bar's status item on every frame. Once its properties were written only when they change, an A/B run went from 197 to 98 ms/s.
The overlay now appears only once the microphone is running, as in the original, so a microphone that fails no longer flashes it (#68, yap^349). On a 120 Hz display, Cairn drew 118 frames a second where the original draws 60. It's now capped at 60, and it checks files every 2 s, as the original does (#69). The idle runs and a check on a 60 Hz display are still to do (#70).
2026-10-2440b6863
Yap on Cairn: the overlay
Yap's dictation overlay on Cairn, driven by a synthetic voice: recording with a moving tape waveform and a two-line live preview, then transcribing, then typed. The state, view and layout are Lean; the waveform is a host-drawn paint node running the original's Metal shader.
2026-10-24a83d44711s
Clock: effects
Cairn's first effects. A stopwatch whose time, ticks, sounds and lap file come from the host as replies to requests Lean makes: Lap plays a sound, Save writes the laps to a file, Reset clears them and Load reads them back. Timers fire within 1–2 ms; a click → read file → frame round trip is 1.5 ms (p50).
2026-10-234fc397016s

Claims on an app I use every day

What Cairn gained

What's proved about dictation

The catch

Progress log

Try it: TodoMVC in the browser

Cairn 0.1.3, on the public registry

Cairn 0.1.2: libraries and apps

Cairn is a package, and Yap moved out

The cairn command and packages

Developer docs and the API reference

Yap against the original under Instruments

Yap on Cairn: the overlay

Clock: effects