Lasm：用 Lean 4 编写可形式化验证的 Web 应用，编译到 WebAssembly

面向 JavaScript 和 WebAssembly 世界的 Lean 4。Lasm 将普通的 Lean 4 程序提前编译为 WebAssembly。一个 Lean 代码库可以变成 Node 服务器、 无服务器或边缘函数、WASI/Fastly 模块或浏览器应用。因为它是 Lean，你可以证明所部署代码的性质。旗舰示例，Conduit，是 RealWorld 应用， 包含 117 个已证明的定理。Lasm 在 npm 上发布，并自带 Lean、Lake 及其构建工具；你只需要 Node（或 Bun 或 Deno）。

npm create @lasm@latest my-app -- --template hono    #然后：cd my-app && npm install && npm run dev

AI 智能体：本 README 自身即完整。llms.txt是简短 索引，而docs/AI.md列出了能让你避免走错路的规则。

如果 Lasm 对你有用，我将感谢你的赞助（更多见下文）。

快速事实

平台

每一行都在 CI 中使用平台自带的本地运行时、镜像或模拟器进行测试。 按项目政策，CI 从不部署到真实云账户 （每个平台如何测试）。

Node 构建拥有 Lean 的完整运行时（线程、文件、进程、套接字）。边缘、Bun/Deno、WASI 和浏览器构建以单线程运行 Lean，不支持套接字或进程（除 WASI 外也不支持文件）；Lean 的其余部分正常工作。

从这里开始

每个示例都有 README，提供一条命令即可运行；examples/README.md列出了全部示例。

旗舰示例：Conduit，包含 117 个已证明的定理

examples/conduit是Conduit，即 RealWorld 应用（一个 Medium 克隆），完全用 Lean 编写：REST API、服务端渲染的浏览器应用以及证明。

• 117 个定理关于实际运行的代码，经检查不使用sorry且npm run proofs仅使用 Lean 的标准公理（；lists each one in plain English). They cover authorization (only authors change their articles and comments), follows and favorites, slugs that never collide, pagination that never skips or repeats, validation shared by client and server (the app never sends what the server would reject), JSON round trips and Markdown link safety. The endpoints are written against aStoreof functions, and the proofs run that same code on a model of the tables.
• What is trusted, not proved:that each SQL statement does what its model says, the JSON text layer, concurrency between requests, and Lean, Lasm and the JavaScript runtime. Conformance to the whole RealWorld spec is tested, not proved.
• API:the official RealWorld API suite passes unmodified (13 of 13 files, 154 requests) on Node (node:sqlite), Cloudflare Workers (D1) and Bun (bun:sqlite). Each target has one hand-written@[js]binding module.
• Frontend: Lasm.UIon RealWorld's official templates, with server-side rendering, hydration and Markdown parsed in Lean. The official Playwright end-to-end suite passes with no retries on Node with Chromium, Firefox and WebKit, and on Workers and Bun with Chromium.

All of this runs in CI (conduit.yml, run 40615274657, with@lasm/cli0.3.4).

cd examples/conduit
npm install                                   #@lasm/cli, Hurl and Playwright (the official suites' runners)
npm run build && npm start                    #http://localhost:3000: the app and its API on Node
npm run proofs                                #check all 117 theorems
npm test                                      #the official API suite (also test:workers, test:bun)
npx playwright install chromium && npm run test:e2e   #the official end-to-end suite
npm run build:workers && npx wrangler dev     #Cloudflare Workers with local D1
npm run build:bun && npm run start:bun        #Bun with bun:sqlite

60-second start

A single file needs no project. Save this complete program asMain.lean:

def main : IO Unit := do
  IO.println s!"Hello from Lean! 2 + 3 = {2 + 3}"

npx @lasm/cli Main.lean          #builds and runs: Hello from Lean! 2 + 3 = 5
npx @lasm/cli build Main.lean    #writes dist/; run it with: node dist/main.mjs

The first build on a new machine fetches Lean and the build tools once (about 250–275 MB; 19 s for that first build on the Linux CI runner). Later dev builds of a one-line change take about 1–2 s.

Recipes

Each recipe is complete: create, develop, build, deploy. Lasm never installs or starts a platform's own CLI (wrangler,vercel,fastly, …); you run those.npm run devislasm dev: it rebuilds about 2 s after each save and restarts the server, and keeps the last good build running when there is a type error.

Node server (Hono; alsoexpress,fastify,std-http,fetch).

npm create @lasm@latest my-api -- --template hono
cd my-api && npm install
npm run dev                                   #http://localhost:3000/hello/Ada
npm run build && npm start                    #dist/ 只需要 Node 24+
docker build -t my-api . && docker run -p 8080:8080 my-api   #生成的 Dockerfile

AWS Lambda / Vercel / Netlify / Azure / Google Cloud Functions。

npm create @lasm@latest my-fn -- --template hono --deploy lambda-zip   #或 vercel、netlify、azure、gcf、lambda-edge
cd my-fn && npm install
npm run build:lambda                          #dist/ 和 lambda.zip（handler 为 lasm-lambda.handler）
#用 AWS 控制台、aws CLI 或 SAM 部署 lambda.zip；操作指南：docs/deploy/lambda.md

Cloudflare Workers（以及 Vercel Edge、Netlify Edge、Deno Deploy、Supabase）。

npm create @lasm@latest my-edge -- --template hono --deploy workers
cd my-edge && npm install
npm run build:workers                         #workers/（wrangler.toml 来自 lasm init）
npx wrangler dev                              #本地 workerd；用 npx wrangler deploy 发布

Fastly Compute、WASI、Spin。

npm create @lasm@latest my-svc -- --template fetch --deploy fastly --deploy spin
cd my-svc && npm install
npm run build:fastly && fastly compute serve  #Viceroy 运行在 http://127.0.0.1:7676
npm run build:wasi-http && spin up            #或：wasmtime serve wasi-http/main.wasm

浏览器应用。

npm create @lasm@latest my-web -- --template web
cd my-web && npm install
npm run dev                                   #http://127.0.0.1:5173，实时重载
npm run build                                 #dist/：可部署到任意主机或 CDN 的静态站点

全栈（服务端 + 浏览器 + 经过验证的 API）。

npm create @lasm@latest my-app -- --template fullstack
cd my-app && npm install
npm run dev                                   #单一 URL：http://127.0.0.1:3000
npm run build && npm start                    #Node；另有 build:workers、build:bun、build:deno

编辑器。运行npx lasm editor每个项目一次；lasm init，lasm dev和lasm build也要这样做。随后 Lean 编辑器（VS Code 的 Lean 4 扩展）会解析import Lasm.*（详情）。

整个技术栈都用 Lean 编写，并经过验证

该fullstack模板是一个 Lean 项目，包含一个服务端（Lasm.Fetch）、一个浏览器应用（Lasm.UI）以及两者之间的 API（Lasm.RPC）。请求必须满足的规则只编写并证明一次，位于Shared.lean，双方都会导入它（templates/fullstack）：

--Shared.lean
@[irreducible] def checkTitle (title : String) : Except String Unit :=
  let n := (clean title).length
  if n = 0 then .error "请先写点内容。"
  else if n > maxTitle then .error s!"请保持在 {maxTitle} 个字符以内。"
  else .ok ()

/-- 只证明一次，在浏览器和服务端都成立。 -/
theorem checkTitle_ok {title : String} (h : checkTitle title = .ok ()) :
    0 < (clean title).length ∧ (clean title).length ≤ maxTitle := by
  unfold checkTitle at h
  by_cases h0 : (clean title).length = 0
  · simp [h0] at h
  · by_cases h1 : (clean title).length > maxTitle
    · simp [h0, h1] at h
    · omega

def addTodo : Endpoint NewTodo Todo := { name := "addTodo", validate := fun r => checkTitle r.title }

--Server.lean：存储 todo 要求提供其标题通过检查的证明，
--而 `addTodo.serve` 在重新验证后把该证明（`ok`）交给处理函数。
def Store.add (s : Store) (title : String) (_ : checkTitle title = .ok ()) : Store × Todo :=
  let t := { id := s.next, title := clean title, done := false }
  ({ todos := s.todos.push t, next := s.next + 1 }, t)

  addTodo.serve fun req ok => do
    let (s, t) := (← load kv).add req.title ok
    save kv s
    return .ok t

--Client.lean：一个关于浏览器应用的定理：它永远不会发送无效标题。
theorem add_invalid (m : Model) (e : String) (h : checkTitle m.draft = .error e) :
    (update .add m).2.effects = [.msg (.added (.error (.invalid e)))] :=
  addTodo.call_invalid { title := m.draft } Msg.added "" e h

证明存放在哪里，以及如何检查。

未证明、改为在 CI 中测试的部分：客户端与服务器之间的 JSON/HTTP 传输、将补丁应用到真实 DOM 的 JavaScript、Lasm 编译器和运行时，以及浏览器。Lean 自身的编译器受信任，与任何 Lean 程序一样（UI.md、RPC.md）。

从 Lean 调用 JavaScript 和 npm

每个调用的 JavaScript 函数用一行声明；Lean 类型说明值如何转换。一个完整程序（Node 的全局fetch）：

import Lasm.JS
open Lasm.JS

/-- `await fetch(url, init)`（Node 的全局 fetch）-/
@[js"globalThis" "fetch"] opaque fetch : String → Data → IO Value

def main : IO Unit := do
  let response ← fetch "https://example.com" (obj [])
  IO.println s!"{← response.get"status"Nat}: {(← response.callMethodAwait"text"#[] String).length} characters"

编写绑定的规则：

• @[js "module" "export"] opaque name : A → B → IO R绑定module.export。该"marked"模块是一个 npm 包（"node:fs"）、一个 Node 内置模块（"globalThis"），或"new Hono"用于全局变量。""调用构造函数，而
• 是该IO R模块自身的值。Async R类型以Async结尾表示立即返回的值，以
• 结尾表示Stringpromise。一个Nat绑定会被等待，而不占用 Lean 线程。Int使用Float、Bool、ByteArray、Array、List、Option、Data、Value、get元组、callMethod（任意 JS 数据）或callMethodAwait（一个 JS 对象引用：deriving ToJS, FromJS、
• Function.ofFn、Function.ofFnReply）。你自己的结构体用hono转换。express/fastify将 Lean 函数转换为 JS 回调。
• npm install框架处理器会使用它们（见lasm build、Lasm.JS binding check failed: … export "x" is missing和dist/node_modules模板）。
• lakefile 旁边的包。

会针对已安装的包检查每个绑定（pg），并将生产依赖复制到jose。fetch每次调用都会从 Lean 线程跨越到 Node 的主线程（约 24 µs），因此优先使用一次粗粒度调用，而不是多次小调用。完整指南，包含 Express、Hono、、

和

示例以及智能体检查清单：docs/JS_BINDINGS.md。

在 Node 上使用 Lean 需要为 WebAssembly 及其线程付出代价。冷启动受 CPU 限制，因此在小份额的无服务器 CPU 上会变大，而且每次 JavaScript 调用都要跨线程。纯 LeanStd.Http在 Node 上很慢（1,290 req/s），所以生产 HTTP 请使用 Hono、Express、Fastify 或Lasm.Fetch。对数千位数字进行算术运算比原生 Lean 慢（没有 GMP）。

已知限制

• 仅支持提前编译。已部署的程序无法在运行时展开、求值或编译 Lean，无法加载模块数据或插件，也无法使用 Lean 的 C++ 编译器/内核（确切列表）。证明、策略、宏和#eval像往常一样在编译时运行。
• 严格为 Lean 4.35.0。其他lean-toolchain版本会被拒绝并给出
• 消息。Node：-l为应用至少分配 512 MB；它会预留约 22 GB 虚拟地址空间。预构建的原生库（
• 、共享库）无法链接；包内自带的 C 源码会为你编译。Edge、Bun/Deno、浏览器、WASI：--suspend jspi单线程 Lean；没有套接字、进程或信号；除 WASI 外没有文件。在浏览器中，阻塞等待会使应用停止，除非它针对带 JSPI 的浏览器用Async构建；请使用
• 。没有预制的绑定Lasm.Web用于 npm 包；
• 覆盖核心 Web 平台。 Lasm.*编辑器：npx lasm editor导入在编辑器中的
• （见上文）之后解析。平台：

没有 Windows ARM64，也没有 Alpine/musl 构建机（构建出的应用可在 Alpine 上运行）。托管平台使用其本地工具进行测试，从不使用真实账户。

• 文档 开始：入门指南·所有文档·面向 AI 智能体·
• llms.txt 指南：服务器与 npm 互操作无服务器与容器·边缘·Bun 和 Deno·浏览器和Lasm.UI·全栈（Lasm.RPC）·Lasm.Fetch·WASI 和 Fastly·编辑循环
• 证据： 基准测试·应用运行在哪里·语言覆盖范围·兼容的 Lean 包·决策

支持 Lasm

如果 Lasm 对你有用，或者你希望看到它成功，我会感谢你的赞助：github.com/sponsors/lastmjs。它支持我以及 Lasm 和其他Millillion项目的工作。我的第一个目标是每月 250 美元，足够为 Lasm 提供一个专用的 Claude Code 账户。你也可以通过给仓库加星、试用它，以及报告出现的问题来提供帮助。

参考

以下所有内容都是精确的约定：每一条命令和选项、支持的机器和平台，以及部署后的 Lean 程序确切不能做什么。

CLI 参考

在项目中安装npm install -D @lasm/cli（可执行文件是lasm），或者不安装直接运行：npx @lasm/cli Main.lean。npm create @lasm运行lasm init相同@lasm/cli版本的Main.lean，参数保持不变。使用快速开始中的

npx lasm Main.lean                          #构建（开发配置）并运行：Hello from Lean! 2 + 3 = 5
npx lasm build Main.lean                    #写入 dist/（发布配置）
npx lasm --version                          #版本、Lean、运行时和平台（用于缺陷报告）
node dist/main.mjs                          #运行部署产物：只需要 Node
npx lasm build Main.lean --target lambda    #dist/ 和一个 AWS Lambda zip

--rebuild以及--verbose可与 run 和 build 一起使用。--output和--target仅用于构建；其后的参数--仅用于 run。应用程序的退出状态会被保留。npx lasm --version（-v）打印版本、Lean 发行版、JavaScript 运行时和平台（请将其包含在错误报告中）。没有 install、clean 或 uninstall 子命令。

构建配置。两者使用相同的库链接同一个程序，且具有确定性。release（lasm build，lasm Main.lean --release）：完整的 Binaryen 大小优化；字节级可复现；用于部署的版本。dev（lasm Main.lean，lasm dev，lasm build --dev）：省略这些优化步骤，并以-O1编译你的模块；行为相同，构建快几秒，其program.wasm大约大 15–20 %。dev 重新构建会从项目之前的构建开始，因此其字节可能依赖于该构建。build-info.json记录"profile"。lasm package和lasm build --dev --target <platform>会拒绝 dev 构建，除非你传入--allow-dev。

环境变量（均为可选）：

其他LASM_*源码中的变量是维护者诊断用的，不是受支持的接口。

安装。 npm install @lasm/cli通过你自己的 registry、代理和缓存，将 Lean 和构建工具作为精确固定版本的@lasm/…npm 包引入你的平台。Lake/Lean-import 数据，且仅对含 C 代码的 Lake 项目，引入 C 层（@lasm/lean-c-<platform>）在首次使用时通过你的 npm 获取。终端会显示进度；后续构建会复用已验证的工具和未变更的输出。在新机器上，如果没有下载，首次 Hono 构建在 CI runner 上耗时 25.7 秒（Linux x64）、27.8 秒（Linux arm64）、44.4 秒（Windows）、58.7 秒（Apple Silicon）和 141.9 秒（Intel Mac）（构建时间，运行 40131930601）。缓存位置与恢复：NODE_SUPPORT.md、INSTALLATION_HARDENING.md。Git仅在带有 Git 或 Reservoir 依赖的 Lake 项目中需要；Lasm 使用你git上的PATH，并在缺失时说明如何安装。

现有 Lake 项目使用项目目录中的npx lasm build Main.lean进行构建。在leanprover/lean4:v4.35.0中固定lean-toolchain；其他版本会被拒绝并提示Unsupported Lean toolchain … Lasm supports Lean v4.35.0。一份按包划分的兼容性列表涵盖 Batteries、Cli、LSpec、Plausible、Aesop、Qq、leansqlite、UnicodeBasic、MD4Lean、lean-zip、lean4-parser、lean-redis 等；不在列表中的包未经测试。

支持的环境

使用 Lasm（编译器）构建的机器：

Node 24 或更新版本（已测试：24.0.0、24.22.1、26.12.1）。无引擎标志。确切测试过的产物：NODE_ACCEPTANCE.md。

支持的平台

一个 Nodedist/需要Node 24 或更新版本（Node 22 及更早版本会停止并提示This application requires Node 24.0.0 or newer）以及至少 512 MB 内存。它可在 Linux x64 和 arm64（glibc 2.28+，或 musl/Alpine）上运行，来自任意受支持平台上的构建，也可在构建机器自身的平台上运行。复制所有dist/；那里不需要 Lean 源码、npm install 或构建工具。下面每个平台都已在 CI 中测试使用本地运行时、镜像或模拟器进行测试；没有任何一项使用真实的云账户。完整矩阵：DEPLOYMENT.md。

一个dist/在 Windows 上构建并复制到 Linux，若非通过docker build需要chmod 755 dist/host/native/process/linux-*。Node 的--jitless无法工作（它会禁用 WebAssembly）。限制虚拟内存的主机（ulimit -v，vm.overcommit_memory=2）会拒绝 Node 构建，因为它预留了约 22 GB 的地址空间。Node 26 的官方二进制需要libatomic1在最小镜像上，它们会自行安装 tarball。

Lean 支持与限制

构建会强制执行提前执行（ahead-of-time execution）。支持普通函数、递归、闭包、归纳类型、模式匹配、类型类、依赖类型以及编译后的 IO。导入、宏、精化（elaboration）、策略（tactics）、派生（deriving）、证明以及#eval运行在编译期间在受管理的原生 Lean 中。初始化器算作运行时依赖：一个宽泛的import Lean可以保留编译器；当只有宏或策略需要它时使用meta import Lean，而对运行时数据库使用更窄的导入（import Lean使用Lean.Json，以及deriving ToJson, FromJson，构建并运行）。每次拒绝都会得到解释：Lasm 会打印从你的代码到编译器代码的链路，并且当宽泛导入是原因时，还会打印你的代码所使用的更窄模块。部署的程序会遵守LEAN_ABORT_ON_NONLINEAR=1，正如原生 Lean 所做的那样。各平台结果：语言覆盖范围。

部署的应用程序不能使用：

构建会检查可达的运行时依赖，包括导入的库和间接调用；可达的禁止调用会被拒绝，即使你的输入不会走那个分支，并且被链接器移除的死代码不计入。启动器还会在加载应用程序之前拒绝缺失、过期或不兼容的能力记录（这是一项一致性检查，不是安全沙箱）。没有大型兼容性回退。

Lake 包。仅为编译而导入的模块（例如策略、精化器，例如 Aesop、Qq 或import Lean对于宏）不会在部署中保留 Lean 的编译器。Lasm 仅在程序使用某个模块所定义或注册的内容时，或者当这些初始化器是程序自身执行 IO 或调用 C 的代码时，才运行该模块的初始化器（--verbose显示跳过了多少个）。包所捆绑的 C 源码（extern_lib，moreLinkObjs，例如 leansqlite 的 SQLite）使用 Lean 自带的 clang 编译，作为 C 层一次性获取（39–52 MB）；不需要系统 C 编译器（macOS 需要 Xcode Command Line Tools SDK 来提供 C 库头文件）。预构建的原生库（共享库、-l选项：libcurl、OpenSSL、libpq、BLAS）无法链接；构建过程会指出该库和所属包。

并非发布保证。控制台输出、参数、退出码、本地 Lake 导入以及选定的语言/文件系统测试夹具都有原生与 Node 的对比测试，并且在 0.1.0 之前，Lean 具备运行时能力的上游测试套件和 19 个生态项目已在全部五个平台上运行，相对于上一个被接受的候选版本零回归（0.1.0 门槛）。完整的IO.FS、并发、子进程/信号/终端一致性、每一个第三方库以及完整的上游测试套件并不保证（IO 缺口）。大数（Nat/Int超过 63 位）使用 Lean 自带的任意精度代码而非 GNU MP，因此应用不包含 LGPL 代码；结果与原生 Lean 相同，但在 10,000 位乘法时约慢 5 倍，Nat.gcd在 Wasm 中比使用 GMP 约慢 60 倍数字）。Lake 依赖使用你的系统 Git（系统 Git）。

发布与来源

0.1.0 是首个 npm 发布（说明）；0.2.0 增加了边缘目标和 Bun/Deno（说明）；0.3.0 增加了浏览器、Lasm.UI、全栈应用、WASI/Fastly 以及编辑器支持（说明）；0.3.1 将起始代码置于 MIT-0 之下，并增加了缺陷报告指引（说明）；0.3.2 修复了Std.Internal.UV套接字、定时器和信号（说明）；0.3.3 从未发布，其改动随 0.3.4 一起发布（说明）；0.3.5 更新了 README 和 Conduit 示例（说明）。Lasm 的 npm 包（@lasm/cli、@lasm/create以及@lasm/…工具包）仅由release.yml工作流发布，通过带来源的 npm 可信发布：不存在 npm 令牌。一次发布就是一个提升package.json版本的拉取请求，并且只有在release-checksstatus（五平台候选检查；edge、Bun/Deno、浏览器、Lasm.UI、WASI/Fastly、全栈、单元和开发循环检查；以及对确切包的 npm 预演）已针对发布的提交通过。发现了一个 bug？npx lasm --version会给出该版本行，bug 报告表单所要求的。npm view @lasm/cli@<version>会显示来源，npm audit signatures在项目中对其进行验证。详情：RELEASING.md。

许可证

Lasm 自身的源代码采用MIT 许可证（版权归 Jordan Last）。起始代码——所有lasm init和npm create @lasm放入一个新templates/项目中的内容，examples/，docs/以及本 README 中的代码示例和——同样采用MIT 无署名@lasm/create（MIT-0），在每个@lasm/cli的license字段是一个 SPDX 表达式，涵盖 Lasm 的 MIT、MIT-0 以及它捆绑的每个组件，其文本位于licenses/中。许可证审计列出了每个分发的组件、其许可证以及每项义务是如何满足的。

• 构建dist/。 THIRD_PARTY_NOTICES.txt以 Lasm 的 MIT 声明和 Lasm 修改过的 Lean 文件列表开头，然后是构建所包含内容的许可证：Lean 的运行时和标准库（Apache-2.0）、Emscripten（MIT OR NCSA）、musl、LLVM libc++、libc++abi、libunwind 和 compiler-rt、mimalloc、libuv、koffi 以及 Lasm 的主机（MIT）。应用不包含任何 copyleft 代码。licenses/<package>/保存了编译进program.wasm的每个 Lake 依赖的许可证文件；通过 npmnode_modules/互操作，保存了每个包及其各自的许可证。分发dist/时请保留这些文件。
• Edge、浏览器、WASI、Fastly 和 wasi-http 输出会获得相同的声明，重写以说明其文件包含的内容，自动生成：每个输出目录中的一个THIRD_PARTY_NOTICES.txt、平台捆绑的 JavaScript（edge 胶水代码、浏览器加载器）上的简短/*! … */许可证lasm.notices自定义段，因此它会随每次部署一起传输）、Fastly 包中的文件，以及THIRD_PARTY_NOTICES.lasm.txt在 Vite 构建中。这对你的应用意味着：docs/LICENSING.md。
• 工具包和发布归档。每个@lasm/…工具包都有一个 SPDXlicense字段和归档的许可证文件。Lean 归档包含的 (L)GPL 部分的准确源代码（GNU MP、GNU C 库、GCC 的运行时库、Linux UAPI 头文件、MinGW-w64）以及 Lean 自身的源代码被镜像为发布它们的版本的资产lean-4.35.0-tiers-v2）。Lasm 不附带任何 Git 和 Apple SDK 文件。
• Lean 名称和标识是 Lean FRO 的商标。Lasm 与 Lean FRO 无关联，也未获其认可。