Lasm compiles Lean 4 programs to WebAssembly for Node, serverless, edge and browser targets

Lasm, a new MIT-licensed toolchain, has reached the front page of Hacker News with an unusual pitch: write your web application in Lean 4, prove theorems about how it behaves, then ship that same verified code to almost every mainstream JavaScript or WebAssembly runtime.

According to the project's README on GitHub, Lasm takes regular Lean 4 source and compiles it ahead of time to WebAssembly. One codebase can then be packaged as a Node server, an AWS Lambda function, a Cloudflare Worker, a Fastly Compute or WASI service, or a static browser app. The current release is @lasm/cli 0.3.5.

Lean arrives as an npm package

Instead of asking developers to install Lean tooling by hand, Lasm ships on npm and bundles Lean, its build tool Lake and everything else needed to compile. The only prerequisite is Node 24 or newer, or Bun or Deno. The toolchain pins Lean to exactly version 4.35.0, and no separate elan installation is required. New projects start with npm create @lasm@latest, with templates for APIs built on Hono, Express or Fastify, pure-Lean servers, browser apps and full-stack apps.

Builds produce a dist folder containing program.wasm plus a JavaScript launcher for Node, or a platform-specific package when a --target flag is passed. Because compilation happens ahead of time, Lean's interactive layer stays behind at build time: the README notes that elaboration, #eval-style evaluation, .olean loading and the Lean kernel are all unavailable at runtime.

A wide deployment matrix

The README documents targets covering Node on any host (Docker, Kubernetes, Cloud Run, Fly.io and others), Lambda in both zip and container form plus Lambda@Edge, functions on Vercel, Netlify, Azure and Google Cloud, edge runtimes including Cloudflare Workers, Vercel Edge, Netlify Edge, Deno Deploy and Supabase, plus Bun, Deno, Fastly Compute, WASI, wasi-http and the four major browsers. Each row is exercised in CI against the platform's local runtime, image or emulator, and by project policy CI never deploys to a real cloud account.

Capabilities differ by target. Node builds get Lean's full runtime, including threads, files, processes and sockets. Edge, Bun/Deno, WASI and browser builds are single-threaded and drop sockets and processes, plus file access everywhere except WASI.

Frameworks written in Lean

Lasm also provides its own libraries: Lasm.Fetch for HTTP on every server target, Lasm.UI for browser interfaces using an Elm-style architecture with a proved diff algorithm, Lasm.RPC for typed client/server APIs, Lasm.Web for the DOM and web APIs, and Lasm.KV for key-value storage.

Interoperability with npm is opt-in rather than automatic. After importing Lasm.JS, each JavaScript function you want to call needs a single @[js] annotation; there are no premade bindings, and the Conduit example uses just one hand-written binding module per target.

Conduit: 117 proved theorems

The flagship example is Conduit, the standard RealWorld Medium-style clone, written entirely in Lean: REST API, server-rendered frontend with hydration, and proofs. The README reports 117 proved theorems about the deployed code, verified with no sorry placeholders and only Lean's standard axioms. They establish that only an article's author can edit it or its comments, that slugs never collide, that pagination never drops or duplicates entries, and that client and server share one validator, so the front end never submits what the back end would reject, alongside JSON round-trip and Markdown link-safety guarantees.

The README is frank about what remains trusted rather than proved: the assumption that each SQL statement matches its model, the JSON text layer, concurrency between requests, and Lean, Lasm and the JavaScript runtime itself. Conformance to the full RealWorld specification is tested, not proved. The official API suite passes unmodified — 13 of 13 files, 154 requests — on Node, Cloudflare Workers and Bun, and the official Playwright end-to-end suite passes without retries on Node across Chromium, Firefox and WebKit.

Why it matters

Formal verification rarely escapes research and safety-critical niches, largely because proof-capable languages have had no story for ordinary deployment. Lasm's bet is that WebAssembly can supply one: if verified Lean code runs natively on every major server and browser platform, the practical cost of writing verified web services falls sharply. Conduit shows both the ceiling and the floor — real invariants like authorization rules get proved, while SQL semantics, concurrency and the runtime stay trusted. Even so, compressing the unverified surface into a short, documented list would be a meaningful upgrade for web development, where today that surface is essentially everything.