Cairn
Docs
Claims
Blog
Packages
Try it
Try a Cairn app
Three of Cairn's example apps, in the browser, with nothing to install. Every control shows its claim (cairn_examples^N) and the evidence the build has for it.
- CounterA bar, Increment, and Reset when there is something to reset. The smallest app.
- BasicsA text field, Add, and a list to check off and delete from.
- TodoTodoMVC: add, complete, edit by double-click, filter, clear.
What you are looking at
A Cairn app is pure Lean: its state, what it draws and what each input does. Ahead of time, the app's own step and frame ran headless from its first frame: every control in each frame was acted on (pressed, double-clicked, or for a text field, typed into with the texts its flows type), and every new frame was kept, up to a bound. These pages replay those recorded frames. The page decides nothing: a click follows the edge the app produced.
Each control carries its claim id, the same cairn_examples^N the code, the proofs and the claim pages use, and reads as its evidence does, the way the claim pages read it. The apps are the example apps, in their own package.