Lasm 发布：用 Lean 4 编写可形式化验证的 Web 应用并编译至 WASM
Lasm 是一个将 Lean 4 程序编译为 WebAssembly 的工具，支持构建 Node、Serverless 及边缘计算环境下的 Web 应用。其核心优势在于允许开发者对部署代码进行数学层面的形式化验证（如旗舰案例 Conduit 包含 117 个已证明定理），且通过 npm 分发，仅需 Node/Bun/Deno 即可运行。
报道正文
本文目录2 个章节
Lasm
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 devAI 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 |
| Lambda@Edge | lambda-edge | lambda-edge.zip | 0.1.0 |
| Vercel Functions | vercel | .vercel/output | 0.1.0 |
| Netlify Functions | netlify | netlify/functions/lasm | 0.1.0 |
| Azure Functions | azure | azure-functions/ | 0.1.0 |
| Google Cloud Functions (gen2) | gcf | gcf/ | 0.1.0 |
| Cloudflare Workers | workers | workers/ | 0.2.0 |
| Vercel Edge | vercel-edge | api/lasm.mjs, api/_lasm/ | 0.2.0 |
| Netlify Edge | netlify-edge | netlify/edge-functions/lasm.mjs | 0.2.0 |
| Deno Deploy | deno-deploy | deno/main.mjs | 0.2.0 |
| Supabase Edge Functions | supabase-edge | supabase/functions/<name>/ | 0.2.0 |
| Bun (≥ 1.3.14) / Deno (2.x) | bun / deno | bun/main.mjs / deno/main.mjs | 0.2.0 |
| Fastly Compute | fastly | bin/main.wasm, pkg/<name>.tar.gz | 0.3.0 |
WASI (wasmtime, wasmer, node:wasi) | wasi | wasi/main.wasm | 0.3.0 |
wasi-http (wasmtime serve, Spin) | wasi-http | wasi-http/main.wasm | 0.3.0 |
| Browsers (Chrome, Edge, Firefox, Safari) | browser (or the Vite plugin @lasm/cli/vite) | dist/ static site | 0.3.0 |
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.
（注：更多技术实现细节与完整 API 文档请查阅原项目 README）
作者发帖说明（HN）：
Lasm has been my dream for a good part of 2026. I firmly believe that formal verification is the next evolution of software engineering and programming languages. This next wave will largely be enabled by the incredibly intelligent LLMs that understand formal verification and its programming languages.
Lean is one of the most popular languages that allow for formal verification, and to me is incredibly powerful because it is a general purpose programming language with formal verification built directly into it.
You can build general purpose software in Lean, and formally verify it in Lean. Amazing.
Lasm brings Lean to the browser, Node, serverless, and edge environments (and more). The idea is that you can now write web apps, frontend to backend, in Lean and formally verify these apps.
Imagine an Express server or Hono server, running on Cloudflare Workers, with formal verification of its specification.
I'm an agentic engineer with an emphasis in software engineering, and Lasm was built mostly by Claude Opus 5.5 with my high-level direction.