Show HN: Lasm – Write formally verified webapps in Lean for Node/serverless/edge
Lasm compiles Lean 4 programs to WebAssembly, enabling formally verified web applications for various environments. It supports Node servers, serverless/edge functions, WASI/Fastly modules, and browser apps. Lasm ships on npm, including Lean and its build tools, requiring only Node (or Bun or Deno). It allows deployment to platforms like AWS Lambda, Vercel, Netlify, Cloudflare Workers, and Deno Deploy, with different runtime capabilities depending on the target.
时间与来源
时间显示为 UTC
显示时区：UTC
本地时区尚不可用，暂时显示 UTC。
发布当时偏移：UTC+02026年10月30日 02:05 UTC
收录当时偏移：UTC+02026年10月30日 03:00 UTC
- 发布
- 2026年10月30日 02:05
- 收录
- 2026年10月30日 03:00
- 来源类型
- 开发者社区
- 档位
- 社区
- 信源状态
- 正常
档位是按信源手工设定的编辑判断，不是逐条打分。
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 ).
Quick facts
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 ).
Deploy to lasm build Main.lean --target … Output Since
Node server or program (any host, Docker/Kubernetes, Cloud Run, Fly.io, Railway, Render, Heroku, DigitalOcean) node (default) dist/ → node dist/main.mjs 0.1.0
AWS Lambda (.zip, nodejs24.x) lambda lambda.zip 0.1.0
AWS Lambda (container image) lasm init … --deploy lambda Dockerfile.lambda 0.1.0