LeanNative

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. Winnow, a Bitcoin wallet written in Lean, runs on it. Early and moving fast: what is left is in the issues.

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.

  1. 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.
  2. 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.
  3. 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.
  4. Xcode builds one app for iPhone, iPad and Mac.A project generated from the app's Lean manifest, which refuses a capability without its usage text or entitlement; 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.

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.