Lasm

At a glance

Lasm is a compiler, installed from npm, that turns ordinary Lean 4 programs into WebAssembly ahead of time. It can package the result as a Node server, a serverless or edge function, a WASI or Fastly module, or a static browser app. Because the source is Lean, theorems about the code you deploy are checked when you build, and a broken proof fails the build. Version 0.3.5 is MIT licensed.

Good fit

Lean users who want their proofs to cover code that actually ships to JavaScript hosts. The fullstack template proves a validation rule once and imports it on both the server and the browser. The Conduit example, a Medium clone, carries 117 checked theorems about authorization, pagination and slugs, and it passes the official RealWorld API and end-to-end suites in the project's CI.

Consider something else when

You need top HTTP throughput, a Lean version other than exactly 4.35.0, or evaluation of Lean code at run time. The project's own CI benchmark puts a Hono server with a Lean handler at about a quarter of plain Node's throughput. There are no premade npm bindings, so you declare each JavaScript function you call yourself.

Start here

With Node 24 or newer, save the two-line hello program from the README as Main.lean and run npx @lasm/cli Main.lean. If it works, it prints "Hello from Lean! 2 + 3 = 5". The first build downloads Lean and its tools once, about 250 to 275 MB. Next, run npm create @lasm@latest my-app -- --template hono, then cd my-app, npm install and npm run dev, which serves on localhost port 3000.

Cost and requirements

Lasm is free under the MIT licence, and the starter code is MIT-0. To build, you need Node 24+ (or Bun or Deno) on Linux x64 or arm64, macOS, or Windows x64. Windows ARM64 and Alpine are not supported as build machines. Expect about 400 MiB installed plus a 2.5 GB tool cache after the first build. Deployed Node apps need Node 24+ and at least 512 MB of memory. Hosting costs depend on your platform.

Limits to know

CI tests every cloud target with local emulators and runtimes only, never a real cloud account. Edge, browser and WASI builds run Lean on a single thread, without sockets or processes. Node builds reserve about 22 GB of virtual address space, so hosts that cap virtual memory refuse them. Prebuilt native libraries such as OpenSSL or libpq cannot be linked. The project is young, and 0.1.0 was its first npm release. The repository lists three contributors: Jordan Last, Claude and a GitHub Actions bot.

Still unclear

• How quickly Lasm will support new Lean releases, given that it accepts exactly one toolchain version, 4.35.0.