Lasm: running proven Lean code on Node

The problem

Web app tests check the code only on the inputs you choose. They cannot show that a rule such as "only the author can edit a post" holds for every request.

In the README, the maker compares Lasm’s performance with Node’s plain http server. The official TypeScript handbook says the type system allows some operations that cannot be known to be safe at compile time. TypeScript types check the shape of values, but they cannot state rules about a function’s results.

How it solves it

Lasm was posted on Hacker News as a Show HN on October 30, 2026. You write the server code in LeanLeanA programming language and proof assistant. You write functions together with theorems about them, and the compiler checks the proofs.. In the same project, you state its rules as theorems and prove them. At build time Lean checks the proofs, and Lasm compiles the checked code to WebAssembly ahead of time.

The output becomes a Node server, a serverlessserverlessA way to deploy code without running your own server. A cloud provider runs your function for each request. function or a browser app. The Lean compiler and build tools come in npm packages, so you only install Node. You call npm packages such as the web framework Hono from Lean by declaring a bindingbindingA declaration that links a function written in another language to a name and type in this language, so you can call it. for each function.

What is different

The first difference is how the rules are checked. In Lasm, Lean checks proofs that the rules hold for every input. A wrong proof fails the build, so that code cannot be deployed. The README’s example, Conduit, is a blog app modeled on Medium. The maker says it proves 117 theorems, including one that says only the author can edit a post. But according to the README, the proofs do not cover whether each SQL statement matches the model of the tables used in the proofs. They also do not cover JSON parsing and printing, or concurrent requests. The proofs assume that Lean, Lasm and the JavaScript runtime are correct.

The second difference is how the code runs. TypeScript compiles to JavaScript, which Node runs directly. Lasm compiles Lean to WebAssembly, so proven code runs inside a JavaScript runtime and can call npm packages. According to the README, Lean code on Node runs in WebAssembly threads and crosses a thread boundary each time it calls JavaScript. The tradeoff is lower throughput than a plain Node http server. The README also says to give each app at least 512 MB of memory.

How it was built

• The repository has 1,180 commits from September 17 to October 28, 2026. Of these, 605 have a Co-authored-by trailer for Claude.
• The README points AI agents to separate guide files (llms.txt and docs/AI.md).
• The numbers in the README’s performance table were measured on a free 4-CPU GitHub runner. The table names the CI run behind each number, so you can look up its log.

Running it

With Node 24, I followed the README’s commands to create the Hono template app, and built and ran it.

1. Install. npm create @lasm@latest app -- --template hono and npm install finished in 20 seconds. node_modules was 674 MB.
2. Build. The first npm run build took 50 seconds and left a 2.7 GB cache in .cache/lasm in the home folder. After I deleted dist, a rebuild took 1.6 seconds. program.wasm was 783 KB.
3. Run. It took 292 ms from starting the server process with node dist/main.mjs to its first response. /hello/Ada returned the Lean function’s greeting as JSON. POST /echo sent Korean text back in JSON without changing it.
4. Proof. I added two theorems about the greet function to App.lean, and the build passed in 9 seconds. One says greet "Ada" returns a fixed greeting, and the other says the greeting has the same format for every name. A false theorem that put Bob in place of Ada failed the build in 0.8 seconds.
5. Throughput. I ran autocannon with 50 connections for 8 seconds, and the server handled 10,058 requests per second. A plain Node http server I wrote handled 64,510 on the same machine. So Lasm had 0.16 times the throughput of the plain server. The README reports 0.24. The maker ran the server and the load generator on separate cores. Today the load generator ran on the server’s 4-core machine without assigned cores. I did not check whether this affects both servers equally.
6. Memory. Under load, the server used 358 MB, less than the 512 MB minimum the README gives.

App.lean:11:67: error: Tactic `decide` proved that the proposition
[lasm] Build failed. Fix the error above and run the command again.

Not checked

• The 117 theorems in Conduit. Run npm run proofs in the example folder and compare the theorems with the descriptions in PROOFS.md.
• Other targets. Build the same app with --target workers and --target bun, and check that it answers on Cloudflare Workers and Bun.

Verdict

It works. The server written in Lean answered, and a false theorem failed the build. But its throughput was far below that of a plain Node server. It is worth trying if you want to prove server logic such as permission rules.