Quick start

Encapp is a proven-app framework. Instead of testing a workflow after you ship it, you write a Workflow value, and Encapp checks that value as a theorem at build time. If your logic drifts, the build fails before you commit.

This page gets you from cloning to seeing one proof verified in the Lean compiler.

Prerequisites

See Installation for the toolchain setup. You'll need:

• elan (Lean v4.15.0) — checks the proofs
• Lake — the build driver
• Node.js v20+ — for the test replayers
• impl-foundation as a sibling directory — the framework's layer foundation

Clone the layout

Encapp and Foundation must sit side by side:

dev/
├── impl-encapp/         (this repo)
└── impl-foundation/     (sibling, required)

The lakefile.lean in impl-encapp declares:

require «foundation» from ".." / "impl-foundation"

Path-based dependency resolution, so no symlink tricks needed. Just check both out at the same level.

Build the framework

cd impl-encapp
~/.elan/bin/lake build

This is not just a compile. Every theorem in the repository is proven here — the refinement proof, the replay laws, the bridge to Foundation, and every workflow's proof by native_decide.

If the build is red, a theorem failed. That is the difference between a test failure in CI and a proof failure at the compiler level.

Emit the hello app to all three platforms

~/.elan/bin/lake exe helloapp

The helloapp executable compiles the hello example to three deployment targets:

dist/index.html           the web SPA (no bundler, no server)
dist/native/app.cjs       React Native module
dist/desktop/main.cjs     Electron entry point (+ preload.cjs, package.json)

All three interpret the same Lean app. The logic layer Encapp.Examples.Hello.helloApp is unchanged; only the renderer differs (DOM via AppGen.emit for web, React Native for mobile, Electron bridge for desktop).

Run it

Open dist/index.html in a browser. No server, no bundler. You'll see three screens:

• /connect — the entry page, asking for a wallet
• /feed — a message list and composer
• /my_posts — a filtered view of your own posts

Type in the composer, click "Post", navigate. The app state flows through the logic layer proof-checked at build time.

One workflow proof

Now look at what you just proved. Open Encapp/Examples/HelloWorkflow.lean:

def helloWorkflow : Workflow where
  name   := "hello-post"
  users  := ["alice"]
  steps  := [ .fire "connect" (.atom (.str "79be667ef9dcbbac")),
              .input "draft" (.str "hello from node:test"),
              .fire "submit" (.atom .null) ]
  checks := [
    .scalarEq "identity" (.str "79be667ef9dcbbac"),
    .scalarEq "path" (.str "/feed"),
    .scalarEq "draft" .null,
    .tableLen "messages" 1,
    .rowField "messages" 0 "body" (.str "hello from node:test") ]
 
theorem helloWorkflow_holds : helloWorkflow.holds helloReflected = true := by native_decide

This workflow:

1. Steps — click "Connect" with a wallet ID, type a message, post it (three interactions)
2. Checks — after those steps, assert:
   • the identity scalar equals the wallet ID
   • the path switched to /feed
   • the draft was cleared to null
   • the messages table has exactly 1 row
   • that row's body field is the exact message you typed

The theorem helloWorkflow_holds is proven by native_decide — the Lean compiler runs the app through its logic layer with those steps, then checks all five assertions. If any check fails, compilation fails.

The aha moment: change a check and watch the build fail

Try this. Open Encapp/Examples/HelloWorkflow.lean and change the last check from:

.rowField "messages" 0 "body" (.str "hello from node:test")

to:

.rowField "messages" 0 "body" (.str "goodbye")

Save. Then:

~/.elan/bin/lake build

The build will fail. The native_decide proof evaluates the app with those steps, finds that the message body is "hello from node:test" (not "goodbye"), and stops the proof in its tracks.

This is not a test that failed. This is a theorem that did not discharge. The build is red until you fix the check to match the actual app behaviour.

Change it back:

.rowField "messages" 0 "body" (.str "hello from node:test")

~/.elan/bin/lake build

Green again. That cycle — write a property, see it fail, fix the property or the app — is how proofs work in Encapp. Unlike a test suite that runs after you deploy, the proof is part of the build. You cannot ship without it.

Recap

• Encapp and Foundation sit side by side by path-based dependency resolution.
• lake build proves every theorem, including each workflow's native_decide.
• lake exe helloapp emits the same app to web, native, and desktop.
• A Workflow is both a proof and a test corpus — define once, run everywhere.
• Changing a check makes the build fail if the app behaviour no longer matches.

Next steps

• Thinking in Encapp — how to design an app as a proven state machine
• Tutorial 1 — write your own app step by step, from logic to view to proof