# Cairn docs > How to build a Mac app in Cairn, where everything a person can do is a claim with a durable id and machine-checked evidence. Cairn apps are written in Lean 4. The app's state, its view, its layout, its hit testing and its text editing are pure Lean functions, and every thing a person can do is a **claim**: an id like `^2`, a sentence saying what happens, a formal statement, and a proof that the code meets it. A thin Swift host runs the app on macOS and paints it with Metal. These docs are young. Pages that today's code supports are written; the one that isn't says what it will cover and what has to land first. Every code sample is included from a source file that `make check` compiles, so a sample can't drift from the code it shows. > **What works today.** Cairn is research, and its API has no stability promise before 1.0. It is a package, though: an > app lives in its own repository and depends on a tagged release (the latest is `v0.5.2`), and > the `cairn` tool starts, builds, checks, bundles and documents it. The example apps are built that > way. The lint, axiom audit and kernel replay have no `cairn` command yet; see > [the cairn tool](https://cairn.iamnbutler.workers.dev/docs/reference/cairn-tool.md). ## Guides
Building an appFrom a first window to effects and shipping, one chapter at a time. Apps on CairnThe example apps: packages of their own, each with its claims. Try an appCounter, Basics and TodoMVC in the browser, every control with its claim id and evidence.
## Reference
API referenceEvery module, declaration and claim in Cairn, generated from the code by cairn doc. The cairn toolStarting, building, checking, bundling, documenting and publishing a package. ClaimsEvery claim kind, what each generates, and what the build checks. The evidence ladderProved, fuzzed, tested, seen, assumed: how sure we are of each claim. How much to trust a claimWhat each kind of evidence rules out, what it still trusts, and a bug the tests miss. The trusted baseWhat the proofs rely on but can't prove, and how each piece is checked. Release notesWhat changed in each version, and what an app can rely on across them.
## Evidence
Claim pagesEvery claim each package makes, grouped by place, with its proofs, generated from what it published.
## Contributing
The host protocolThe two byte buffers between Lean and Swift, and the threads around them. Writing host effectsAdding something the host does for an app, with its assumption and fuzz check. Profiling against a referenceMeasuring an app against the one it replaces, with Apple's own tools. ContributingThe rules every change follows.
From https://cairn.iamnbutler.workers.dev/docs/. All of Cairn's docs for language models: https://cairn.iamnbutler.workers.dev/llms.txt