Lean 4 for the JavaScript and WebAssembly world. Lasm compiles ordinary Lean 4 programs ahead of time to WebAssembly. One Lean code base can become a Node server, a serverless or edge function, a WASI/Fastly module or a browser app. Because it is Lean, you can prove properties of the code you deploy. The flagship example, Conduit, is the RealWorld app with 117 proved theorems. Lasm ships on npm and brings Lean, Lake and its build tools with it; you only need Node (or Bun or Deno).

npm create @lasm@latest my-app -- --template hono # then: cd my-app && npm install && npm run dev

AI agents: this README is complete on its own. llms.txt is the short index, and docs/AI.md lists the rules that save you from wrong turns.

If Lasm is useful to you, I'd appreciate your sponsorship (more below).

Fact Value

Current version @lasm/cli 0.3.5 (release notes); npm view @lasm/cli version

Install npm install -D @lasm/cli (bin: lasm), or no install: npx @lasm/cli …; new project: npm create @lasm@latest

Lean exactly 4.35.0 (lean-toolchain: leanprover/lean4:v4.35.0); Lasm installs it, and you need no elan to build

Develop on Linux x64/arm64 (glibc 2.34+), macOS x64/arm64, Windows x64

Compiler runs on Node ≥ 24 (tested 24.0.0, 24.22.1, 26.12.1); Bun 1.4.4 and Deno 2.9.6 (tested, as the only runtime)

Output dist/ with program.wasm + a JS launcher (Node); or a platform package (--target …)

Node apps run on Node ≥ 24, Linux x64/arm64 (glibc 2.28+ or musl) from any build machine, plus the build machine's own OS; ≥ 512 MB memory

JS/npm interop import Lasm.JS; one @[js "pkg" "export"] line per function you call; no premade bindings (guide)

Frameworks in Lean Lasm.Fetch (HTTP, every server target), Lasm.UI (browser, Elm architecture, proved diff), Lasm.RPC (typed client/server API), Lasm.Web (DOM and web APIs), Lasm.KV

Not available at run time elaboration, #eval-style evaluation, loading .olean, Lean's kernel (exact list); all of these work at build time

License MIT (Lasm); templates, examples and README code samples also MIT-0

Repository / issues https://github.com/Millillion/lasm · report a bug (include npx lasm --version)

Platforms

Every row is tested in CI with the platform's own local runtime, image or emulator. By project policy CI never deploys to a real cloud account (how each is tested).

Node builds have Lean's full runtime (threads, files, processes, sockets). The edge, Bun/Deno, WASI and browser builds run Lean single-threaded, without sockets or processes (and without files, except on WASI); the rest of Lean works.

I want to build… Run Then look at

A command-line program npm create @lasm@latest my-tool examples/hello, examples/wasi-cli

A REST API on Node with an npm framework npm create @lasm@latest my-api -- --template hono (or express, fastify) examples/js-crud (Postgres + JWT, Express and Hono)

A server in pure Lean (no npm) npm create @lasm@latest my-api -- --template fetch (any target) or --template std-http (Node, also native Lean) examples/fetch; the std-http template

A serverless function (Lambda, Vercel, Netlify, Azure, GCF) npm create @lasm@latest my-fn -- --template hono --deploy lambda-zip (or vercel, netlify, azure, gcf, lambda-edge) docs/deploy

An edge function (Workers, Vercel/Netlify Edge, Deno Deploy, Supabase) npm create @lasm@latest my-edge -- --template hono --deploy workers (or fetch) examples/edge-pure, docs/EDGE.md

A Fastly, WASI or Spin service npm create @lasm@latest my-svc -- --template fetch --deploy fastly (or wasi-http, spin, wasi) examples/fetch, docs/WASI.md

A browser app npm create @lasm@latest my-web -- --template web examples/ui (counter, TodoMVC with proofs, feature demo, benchmark)

A complete real-world app (API, browser frontend, SQL, auth) with proofs, on Node, Workers or Bun cd examples/conduit && npm install && npm run build && npm start examples/conduit, the flagship (below)

A full-stack app with a verified API npm create @lasm@latest my-app -- --template fullstack templates/fullstack

To call npm packages or fetch from Lean add import Lasm.JS and one @[js] line per function examples/js-fetch, JS bindings

To run on Bun or Deno bun create @lasm my-app --template hono / deno run -A npm:@lasm/create my-app --template hono docs/BUN_DENO.md

Every example has a README with a one-command run; examples/README.md lists them all.

examples/conduit is Conduit, the RealWorld app (a Medium clone), written entirely in Lean: the REST API, the server-rendered browser app and the proofs.

All of this runs in CI (conduit.yml, run 40615274657, with @lasm/cli 0.3.4).

cd examples/conduit npm install # @lasm/cli, Hurl and Playwright (the official suites' runners) npm run build && npm start # http://localhost:3000: the app and its API on Node npm run proofs # check all 117 theorems npm test # the official API suite (also test:workers, test:bun) npx playwright install chromium && npm run test:e2e # the official end-to-end suite npm run build:workers && npx wrangler dev # Cloudflare Workers with local D1 npm run build:bun && npm run start:bun # Bun with bun:sqlite

60-second start

A single file needs no project. Save this complete program as Main.lean:

def main : IO Unit := do IO.println s!"Hello from Lean! 2 + 3 = {2 + 3}"

npx @lasm/cli Main.lean # builds and runs: Hello from Lean! 2 + 3 = 5 npx @lasm/cli build Main.lean # writes dist/; run it with: node dist/main.mjs

The first build on a new machine fetches Lean and the build tools once (about 250–275 MB; 19 s for that first build on the Linux CI runner). Later dev builds of a one-line change take about 1–2 s.

Each recipe is complete: create, develop, build, deploy. Lasm never installs or starts a platform's own CLI (wrangler, vercel, fastly, …); you run those. npm run dev is lasm dev: it rebuilds about 2 s after each save and restarts the server, and keeps the last good build running when there is a type error.

Node server (Hono; also express, fastify, std-http, fetch).

npm create @lasm@latest my-api -- --template hono cd my-api && npm install npm run dev # http://localhost:3000/hello/Ada npm run build && npm start # dist/ needs only Node 24+ docker build -t my-api . && docker run -p 8080:8080 my-api # the generated Dockerfile

AWS Lambda / Vercel / Netlify / Azure / Google Cloud Functions.

npm create @lasm@latest my-fn -- --template hono --deploy lambda-zip # or vercel, netlify, azure, gcf, lambda-edge cd my-fn && npm install npm run build:lambda # dist/ and lambda.zip (handler lasm-lambda.handler)

deploy lambda.zip with the AWS console, aws CLI or SAM; recipes: docs/deploy/lambda.md

Cloudflare Workers (and Vercel Edge, Netlify Edge, Deno Deploy, Supabase).

npm create @lasm@latest my-edge -- --template hono --deploy workers cd my-edge && npm install npm run build:workers # workers/ (wrangler.toml came from lasm init) npx wrangler dev # local workerd; npx wrangler deploy to publish

Fastly Compute, WASI, Spin.

npm create @lasm@latest my-svc -- --template fetch --deploy fastly --deploy spin cd my-svc && npm install npm run build:fastly && fastly compute serve # Viceroy on http://127.0.0.1:7676 npm run build:wasi-http && spin up # or: wasmtime serve wasi-http/main.wasm

Browser app.

npm create @lasm@latest my-web -- --template web cd my-web && npm install npm run dev # http://127.0.0.1:5173, live reload npm run build # dist/: a static site for any host or CDN

Full stack (server + browser + verified API).

npm create @lasm@latest my-app -- --template fullstack cd my-app && npm install npm run dev # one URL: http://127.0.0.1:3000 npm run build && npm start # Node; also build:workers, build:bun, build:deno

Editor. Run npx lasm editor once per project; lasm init, lasm dev and lasm build also do it. The Lean editor (VS Code's Lean 4 extension) then resolves import Lasm.* (details).

The fullstack template is one Lean project with a server (Lasm.Fetch), a browser app (Lasm.UI) and the API between them (Lasm.RPC). The rule a request must satisfy is written and proved once, in Shared.lean, which both sides import (templates/fullstack):

-- Shared.lean @[irreducible] def checkTitle (title : String) : Except String Unit := let n := (clean title).length if n = 0 then .error "Write something first." else if n > maxTitle then .error s!"Keep it under {maxTitle} characters." else .ok ()

/-- Proved once, holds in the browser and on the server. -/ theorem checkTitle_ok {title : String} (h : checkTitle title = .ok ()) : 0 < (clean title).length ∧ (clean title).length ≤ maxTitle := by unfold checkTitle at h by_cases h0 : (clean title).length = 0 · simp [h0] at h · by_cases h1 : (clean title).length > maxTitle · simp [h0, h1] at h · omega

def addTodo : Endpoint NewTodo Todo := { name := "addTodo", validate := fun r => checkTitle r.title }

-- Server.lean: storing a todo demands the proof that its title passed the check, -- and addTodo.serve hands the handler that proof (ok) after re-validating. def Store.add (s : Store) (title : String) (_ : checkTitle title = .ok ()) : Store × Todo := let t := { id := s.next, title := clean title, done := false } ({ todos := s.todos.push t, next := s.next + 1 }, t)

addTodo.serve fun req ok => do let (s, t) := (← load kv).add req.title ok save kv s return .ok t

-- Client.lean: a theorem about the browser app: it never sends an invalid title. theorem add_invalid (m : Model) (e : String) (h : checkTitle m.draft = .error e) : (update .add m).2.effects = [.msg (.added (.error (.invalid e)))] := addTodo.call_invalid { title := m.draft } Msg.added "" e h

Where proofs live and how they are checked.

Not proved, tested in CI instead: the JSON/HTTP transport between client and server, the JavaScript that applies patches to the real DOM, the Lasm compiler and runtime, and the browsers. Lean's own compiler is trusted, as in any Lean program (UI.md, RPC.md).

Declare each JavaScript function you call with one line; the Lean type says how values convert. A complete program (Node's global fetch):

import Lasm.JS open Lasm.JS

/-- await fetch(url, init) (Node's global fetch) -/ @[js "globalThis" "fetch"] opaque fetch : String → Data → IO Value

def main : IO Unit := do let response ← fetch "https://example.com" (obj []) IO.println s!"{← response.get "status" Nat}: {(← response.callMethodAwait "text" #[] String).length} characters"

The rules for writing bindings:

Full guide, with Express, Hono, pg, jose and fetch examples and an agent checklist: docs/JS_BINDINGS.md.

All numbers are from CI on a free GitHub runner (4-CPU AMD EPYC, Linux x64), candidate 0.1.0-experimental.40494203854 (2026-10-27) unless another run is named. Full tables, method and caveats: BENCHMARKS.md.

Lean on Node pays for WebAssembly and its threads. A cold start is CPU-bound, so it grows on small serverless CPU shares, and every JavaScript call crosses threads. Pure-Lean Std.Http on Node is slow (1,290 req/s), so use Hono, Express, Fastify or Lasm.Fetch for production HTTP. Arithmetic on numbers with thousands of digits is slower than native Lean (no GMP).

Ahead of time only. A deployed program cannot elaborate, evaluate or compile Lean, load module data or plugins, or use Lean's C++ compiler/kernel at run time (exact list). Proofs, tactics, macros and #eval run while compiling, as usual.

Lean 4.35.0 exactly. Other lean-toolchain versions are rejected with a message.

Node: give an app at least 512 MB; it reserves about 22 GB of virtual address space. Prebuilt native libraries (-l, shared libraries) cannot be linked; a package's bundled C source is compiled for you.

Edge, Bun/Deno, browser, WASI: single-threaded Lean; no sockets, processes or signals; no files except on WASI. In the browser, blocking waits stop the app unless it is built with --suspend jspi for a browser with JSPI; use Async.

No premade bindings for npm packages; Lasm.Web covers the core web platform.

Editor: Lasm.* imports resolve in the editor after npx lasm editor (above).

Platforms: no Window