Lasm：用 Lean 编写正式验证的 Web 应用

Lasm 将 Lean 4 编译为 WebAssembly。您用 Lean 编写应用程序，证明应用程序的关键部分，并在 Node.js、Bun、Deno、Cloudflare Workers、Vercel、Netlify、Deno Deploy、Supabase、AWS Lambda、Azure Functions、Google Cloud Functions、Fastly Compute、WASI 运行时和浏览器上运行。旗舰示例 Conduit 是用 Lean 编写的 RealWorld 应用程序，有 294 个已证明的定理。它在下表中的每个平台上都通过了 RealWorld 的官方 API 和浏览器测试套件。如果 Lasm 对您有用，我将不胜感激（更多内容见下文）。它运行的平台和证据

下表中的每个平台都在 CI 中进行了测试，使用平台自己的运行时、容器镜像或本地模拟器。CI 从不部署到真实的云帐户，因此“测试”意味着平台的本地工具，而不是生产环境（详细信息）。

平台 Build with --target Tested in CI with SinceNode.js 24+ (Linux, macOS, Windows; Docker, Kubernetes, Cloud Run, Fly.io, Railway, Render, Heroku) node (default) Node 24 and 26 on Linux (x64, arm64), macOS (x64, arm64) and Windows x64; Docker images, read-only, 512 MB 0.1.0Bun / Deno bun / deno Bun 1.4.4 and Deno 2.9.6 on the same five platforms 0.2.0Cloudflare Workers workers wrangler dev (workerd), Free-plan budgets enforced 0.2.0Vercel Functions / Vercel Edge vercel / vercel-edge vercel build offline; Lambda Node 24 image; Vercel's edge-runtime 0.1.0 / 0.2.0Netlify Functions / Netlify Edge netlify / netlify-edge netlify build and netlify dev , offline 0.1.0 / 0.2.0Deno Deploy deno-deploy Deno 2.9.6 0.2.0Supabase Edge Functions supabase-edge Supabase's edge-runtime image 0.2.0AWS Lambda (.zip or container) / Lambda@Edge lambda / lambda-edge public.ecr.aws/lambda/nodejs:24 via the Runtime Interface Emulator, x86_64 and arm64; sam local 0.1.0Azure Functions azure Azure Functions Core Tools func start 0.1.0Google Cloud Functions (gen2) gcf Functions Framework; Google Cloud's buildpacks image 0.1.0Fastly Compute fastly Viceroy 0.21.1 0.3.0WASI / wasi-http / Spin wasi / wasi-http wasmtime 49 ( run , serve ), wasmer 7.4, node:wasi , Spin 4.2 0.3.0Browsers browser (or the Vite plugin) Playwright: Chromium, Firefox and WebKit (Linux and macOS) 0.3.0Node builds have Lean's full runtime (threads, files, processes, sockets)。

其他目标以单线程运行 Lean，没有套接字或进程（WASI 除外，WASI 可以使用文件）； Lean 的其他部分仍然可用。

快速事实

事实 值当前版本 @lasm@cli 0.3.7 ( release notes ); npm view @lasm@cli version安装 npm install -D @lasm@cli (bin: lasm ), 或不安装: npx @lasm@cli …

; 新项目: npm create @lasm@latest Lean exactly 4.35.0 ( lean-toolchain : leanprover/lean4:v4.35.0 ); Lasm 安装它，您不需要 elan 来构建开发在 Linux x64/arm64 (glibc 2.34+), macOS x64/arm64, Windows x64编译器在 Node ≥ 24 (测试 24.0.0, 24.22.1, 26.12.1); Bun 1.4.4 和 Deno 2.9.6 (测试，作为唯一的运行时)输出 dist/ with program.wasm + a JS launcher (Node); 或一个平台包 ( --target …

)Node 应用程序在 Node ≥ 24, Linux x64/arm64 (glibc 2.28+ or musl) 从任何构建机器，加上构建机器自己的 OS; ≥ 512 MB 内存JS/npm 互操作 import Lasm.JS ; 一个 @[js "pkg" "export"] 行每调用一个函数; 没有现成的绑定 ( guide )Lean 中的框架 Lasm.Fetch (HTTP, 每个服务器目标), Lasm.UI (浏览器, Elm 架构, 证明 diff), Lasm.RPC (类型化的客户端/服务器 API), Lasm.Web (DOM 和 Web API), Lasm.KV不可在运行时 elaboration, #eval -style 评估, 加载 .olean , Lean 的内核 (确切列表); 这些都在构建时工作许可证 MIT (Lasm); 模板、示例和 README 代码样本也 MIT-0仓库 / 问题 https://github.com/Millillion/lasm · 报告一个错误 (包括 npx lasm --version )从这里开始我想构建…

运行 然后看一下一个命令行程序 npm create @lasm@latest my-tool examples/hello , example