NATIVE APPS · WRITTEN IN LEAN 4

Write the app in Lean.
Prove what matters.

LeanNative builds iPhone, iPad and Mac apps from ordinary Lean 4. The functions you test and prove are the ones that run in the app, drawn by a shared UIKit shell, with Mac Catalyst on the Mac. No Swift.

View on GitHub Try native-demo

Open source. Formerly ElmLean. Early and moving fast: see what is done and what is not.

Illustration of the example further down the page.

One model, from proof to pixels

An app is a Lean package with the Elm shape: a Model, the Msgs it can receive, an update and a view. Effects are explicit commands. Everything else is the framework.

Write the app and its invariants in Lean.Typed views can only emit messages update handles. You state the properties you need and prove that every message preserves them.
Lean checks the proofs and compiles to C.The same update and view run in headless tests and in the app. An axiom gate fails the build if a theorem leans on anything unexpected.
The shell makes it an app.A generic Objective-C shell, printed from Lean and checked against the view grammar as it builds, renders the tree with UIKit and offers the platform: authentication, Keychain, HTTPS, CloudKit, Bluetooth LE, background tasks.
Xcode builds one app for iPhone, iPad and Mac.XcodeGen project, Lean's runtime retargeted for the platform, a check that no Swift was compiled, linked or bundled.

A whole app, and a proof about it

This compiles against the framework today. The theorem is the one claim it makes; the framework turns it into a guarantee about every session the app can reach.

structure Model where
  count : Nat

inductive Msg where
  | inc
  | reset

def update : Msg → Model → Model
  | .inc, m => { count := min (m.count + 1) 10 }
  | .reset, _ => { count := 0 }

def view (m : Model) : Html Msg :=
  .col [ .text s!"Count: {m.count}" .title
       , .row [ .button "+1" .primary (some .inc)
              , .button "Reset" .plain (some .reset) ] ]

def app : App Model Msg :=
  { init := { count := 0 }, update, view }

/-- The count never passes 10,
    in any session the app can reach. -/
def spec : Spec app where
  Inv m := m.count ≤ 10
  Target _ _ := True
  init_inv := by decide
  update_inv := fun msg m _ => by
    cases msg <;> simp [app, update] <;> omega
  view_sat := fun _ _ =>
    Html.Sat.of_forall (fun _ => trivial) _

-- from the framework, for every app:
-- Spec.reachable_inv : S.Inv (Session.reach app rs).model

Three obligations: the invariant holds at the start, every message keeps it, and every control the view offers produces a sensible message. From those the framework proves the invariant after any sequence of events.

That is a statement about the state transitions. It says nothing about how UIKit draws them; that part is tested, not proven.

What an app gets

The framework stays small. Platform services are optional modules an app imports when it needs them.

Native interfaces

Lists, navigation, tabs, sheets, toolbars, text input, pickers, QR codes and share sheets, drawn by UIKit. On the Mac, resizable windows, sidebar tabs and popovers.

Typed platform clients

Device authentication, Keychain, HTTPS with SOCKS5, CloudKit and Bluetooth LE as typed requests and results. Denied, cancelled, unsupported, malformed and failed are different answers.

Background work done right

A background run that starts, expires and completes exactly once, drains its work before it reports, and cannot report success after it has been expired.

Scoped effects

Tokens that go stale when the thing they belong to ends, so a late reply never updates the wrong state, including across an authentication prompt.

UI tests and evidence

An XCTest helper kit for the real controls, and an exporter that turns a test run into screenshots, a recording and a provenance manifest that cannot call a failed run a pass.

CI for an app

A reusable GitHub workflow: build once, run tests in parallel, build for the simulator and device, check for Swift, run the UI tests with a screen recording.

Where it stands

Updated 29 October 2026. LeanNative has just moved to its own home; the pieces below are being extracted from a real app, Winnow, a Bitcoin wallet written in Lean.

Piece	Status	Notes
Core: views, sessions, `Spec`, proofs	Working	Axiom-gated theorems about dispatch, sessions and invariants.
UIKit shell and capabilities	Working	iOS simulator and Mac Catalyst (arm64 and x86_64) build and run. Physical devices are not covered yet.
Background run	Merged	Race-tested with controllable gates. Winnow moves onto it next.
Typed platform clients	Merged	Tested against independent wire fixtures and the real shell. Adds an atomic create-only Keychain operation.
Test evidence exporter	In review	Records the tested revision when the tests run, not when you export.
XCTest helper kit	In progress	Exercised against native-demo's real controls on iOS; Catalyst gestures are separate.
Scoped effects and authentication	In progress	Builds on the two merged pieces above.
Winnow on LeanNative	Planned	After the pieces above pass their gates. Winnow keeps its own repository and identity.
Versioned rename of the `ElmLean` identifiers	Not scheduled	The package, modules and C symbols keep their old names so existing apps build unchanged.

Progress and the full list of tickets are in the issue tracker.

What is proven, and what is only tested

Writing an app in Lean does not make it correct. A proof covers the property it states, under its assumptions.

Proven by Lean

The framework's theorems about views and sessions: a control is advertised exactly when dispatching it yields a message, and the session always shows the view of its model.
Any invariant you prove your update preserves holds after every reachable event sequence.

Trusted and tested

The UIKit renderer, the capabilities and the C shim, driven in the simulator and under Mac Catalyst.
Lean's compiler and runtime, UIKit, iOS and macOS.
The runtime integration is experimental: Lean's macOS libraries are retargeted by rewriting their platform metadata, which Lean does not support as cross-compilation.
Typed clients check the shape of what the platform answers, not that the platform did the right thing.

There is no AppKit renderer and no web target; the Mac app is a Mac Catalyst app. Background tasks do not run under Mac Catalyst.

Write the app in Lean.Prove what matters.