Compile-time verification for your code, and for what people experience.
Every action in a Cairn app is a claim with a proof. If a proof fails, the app doesn't build.
What a claim is
A claim is one statement about the app under one id, with a half for people and a half for the checker. Here is the whole of Reset in Counter, one of the example apps:
move ^2 reset (s : State) "Reset" in ^3 where12 does "Press Reset."3 sees "The count is zero, and Reset disappears." enabled := resetEnabled s45 on press apply := { s with count := 0 }6 post s' := s'.count = 0 ∧ resetEnabled s' = false7 sound := by intro s _; exact ⟨rfl, rfl⟩8- The id Permanent: never renumbered or reused, and what reviews, docs and agents cite. Like a data-testid that can't drift.
- Where it lives
^3is a claim too, a place: Counter's window. - For people
doesandsees, in plain English for reviewers and the claim's page. Lean doesn't check them. - When it's offered The button is proved on screen exactly when this holds, in every state. Playwright's toBeVisible() checks one page load.
- For the checker Everything below. Lean checks it when the app builds.
- What it does A pure copy of
swith the count at 0. - The promise Afterwards the count is zero and Reset is gone. An expect() stated for every state, not asserted on one run.
- The proof Like assert_eq!, except the compiler settles it for every s. No proof, no build.
Because the update is built only from moves, two things hold for every app, proved once in
the framework: an action that no claim owns changes nothing and asks nothing of the host
(update_unclaimed), and every effect the app does ask for comes from a move
(update_effect). Claims shows one running, and what
they buy you.
Ids are the contract
An id is a data-testid that can't drift, and semver for guarantees. ^2 means Reset
for as long as the counter exists: never renumbered or reused, and a claim that goes away is
retired with a reason. claims.lock records every id with a hash of its statement; the
build fails when an id vanishes or changes kind, and warns when a statement's meaning changes. A
repeated control carries a key (^5#12 is ^5 for item 12), and each
package numbers in its own scope (cairn^N for Cairn's own).
Six kinds
| Kind | What it says | Examples |
|---|---|---|
| move | Something a person can do, what follows, and the proof. | ^1 Increment, ^2 Reset |
| flow | A goal and a path of moves that reaches it. Lean checks every step is really answered. | ^4 Count to three, ^5 Start over |
| invariant | A property every move keeps, so it holds in every state the app can reach. | yap^311 A shortcut never sends (Yap) |
| assume | Something the proofs rely on but can't prove. Recorded, and visible in every theorem that uses it. | cairn^7 The host reports clicks where they happen |
| place | A region of the view where moves appear. | ^3 Counter window, in the figure above |
| retire | A tombstone: the claim is gone, the id stays issued. | ^6 No press left in progress: the runtime owns presses now |
How sure we are
Every claim carries its evidence, and its claim page shows which kind. Strongest first:
- Proved. Lean's kernel checked the proof, using only the three standard axioms;
make checkaudits every theorem. - Fuzzed. Random sequences of moves, with the claim checked after every step: property-based testing, like proptest or QuickCheck, over whole sessions.
- Tested. The real app, driven through generated sequences of moves, agrees with the model after every step: an end-to-end suite whose expected values come from the proved model.
- Seen. The claim's control is on a captured frame, and a flow replays click by click.
- Assumed. Recorded, never proved. Theorems that rely on it take it as a hypothesis, so every use shows.
Each one rules out something different and still trusts something: how much to trust a claim says what, with a bug the tests miss and the proof catches.
Every package on the registry gets claim pages: every claim it makes, grouped by place, with its proofs, generated from what it published and nothing written by hand. See the example apps' for Counter, Basics and TodoMVC, and Cairn's for its trusted base.
The idea
A cairn is a stack of stones that marks a trail: placed by hand, built to last, and trusted by
whoever comes next. Here the trails are a product's flows, and the stones are claims about them:
“pressing ^12 clears the completed items”, “^12's button is visible
and on top whenever there's something to clear”. Each claim is backed by a Lean proof, a model
check or a conformance run against the real app.
To make those claims mean something, the code they talk about has to be the code that runs. So the app's state, view, layout, hit testing, focus and text editing are all pure Lean, and the theorems are about exactly those functions.
Main thread Swift, AppKit trustedkept thin
Lean thread owns the state provedclaims are theorems
Render thread Swift, Metal trustedprobes, goldens