Lean 4 · proven UI · web / native / desktop
Encapp
The framework for user interfaces you can prove. Write the app once as a Lean value; ship it to three platforms.
$ lake build✓ hello_reflected_matches reflected ≡ typed✓ corpus_all_hold 54 workflows✓ refines_sound backend ≡ spec✓ applyEv_idem replay idempotentBuild completed — the proofs are the build.$
Write
Your app is a value
Model, update and view are ordinary Lean data — so the same app that ships is the app you reason about. No codegen step can fail, because there is no code to generate: there is a value to serialize, and one generic interpreter per platform.
def counter : Spec where
init := [("count", 0)]
view := .col [
.button "-" "dec",
.bind "count",
.button "+" "inc" ]
update := [
⟨"inc", "count", .incr⟩,
⟨"dec", "count", .decr⟩ ]
theorem inc_dec_roundtrip :
counter.step "dec"
(counter.step "inc" counter.init)
= counter.init := by decideThe app is data, so facts about it are theorems. Increment-then-decrement being the
identity is not a unit test that ran on Tuesday — it is checked every time the project
compiles, for every state, by decide.
Real apps use the same shape at scale: a Doc of scalars and tables, a
finite handler table, and a typed view tree per page.
Prove
Whole user stories, at build time
A workflow is clicks, typing and post-conditions — one definition that is simultaneously a machine-checked proof and a test the real UI replays. If a handler drifts, the build fails, not the nightly run.
def helloWorkflow : Workflow where
name := "hello-post"
steps := [
.fire "connect" (.atom (.str "79be…")),
.input "draft" (.str "hello!"),
.fire "submit" (.atom .null) ]
checks := [
.scalarEq "path" (.str "/feed"),
.scalarEq "draft" .null,
.tableLen "messages" 1,
.rowField "messages" 0 "body"
(.str "hello!") ]
theorem helloWorkflow_holds :
helloWorkflow.holds helloReflected
= true := by native_decideDefine once, prove once, run everywhere. The interpreter that runs the app is the interpreter that proves the test — then the same workflow, emitted as JSON, is replayed on happy-dom, headless Chromium, React-Native-web and real Electron.
The flagship app proves 54 user stories in one theorem at lake build time.
Ship
One logic artifact, three platforms
The usual multi-platform story generates three codebases and lets them drift. Encapp inverts it: the app never changes shape — what differs is the interpreter, and there is exactly one per platform.
The core state machine is emitted once and shared byte-identically by web and native — a checked gate asserts it. Desktop loads the web artifact unchanged, so its renderer cannot drift by construction. Web · Native · Desktop
Swap
The backend is a proven spec
TEA leaves "the runtime" abstract. Encapp makes it a first-class object and proves the contract most frameworks only assert: an app cannot observe which backend ran it.
theorem refines_sound
(w : World H) (R)
(hr : Refines w R) :
∀ cs h s, R h s →
(w.runAll cs h).2
= (emulator.runAll cs s).2
∧ R (w.runAll cs h).1
(emulator.runAll cs s).1The emulator is the denotational spec — its state is the event log. Any real adapter that refines it emits byte-identical event traces for every command sequence, by a closed simulation argument, not a README promise.
Replay is idempotent and reload equals full replay, proven generically for every app.
Trust
Honest about its limits
A framework that says "formally verified" without saying what is verified transfers confidence it has not earned. Encapp documents its boundary and ships the commands that would refute each claim.
The emitted JS runtime is checked empirically against the Lean interpreter across four replay tiers — it is not related to it by theorem. Crypto is axiomatized. The proof tier is single-instance. The host adapter a deployment writes is ordinary code outside the proof boundary — and the framework's answer is to make it declarable, so deleting a declaration turns a real test red.