Lasm 发布可将 Lean 4 代码编译为 WebAssembly 的全栈框架并支持形式化验证

Lasm 是一个开源工具，允许开发者使用 Lean 4 编写 Web 应用程序，并在构建时将其编译为 WebAssembly，从而在 Node.js、Serverless、Edge、WASI 及浏览器环境中运行。其核心特性在于利用 Lean 的类型系统和定理证明能力，在代码部署前对业务逻辑进行形式化验证，确保运行时行为符合数学证明。旗舰示例 Conduit（一个 RealWorld 标准的 Medium 克隆）包含 117 个经过严格证明的定理，覆盖了授权、分页、数据验证等关键功能，且所有证明均无 sorry 占位符。

该工具通过 npm 分发，依赖 Node 24+、Bun 或 Deno 作为运行时环境，无需安装 elan 即可自动管理 Lean 4.35.0 工具链。它支持多种部署目标，包括 AWS Lambda、Vercel、Cloudflare Workers、Fastly Compute 和 Supabase Edge Functions 等，每个平台均有独立的 CI 测试覆盖。性能方面，Node 环境下 Hono + Lean 处理器的冷启动耗时约 159 毫秒，吞吐量约为原生 Node 的 24%，内存占用在负载下约 329 MiB。Lean 与 JavaScript 的互操作通过 @[js] 注解实现，每次调用跨线程开销约 24 微秒，建议减少细粒度调用以提升效率。

事实层面，Lasm 目前版本为 0.3.5，仅支持 Lean 4.35.0，且部署后的程序无法在运行时动态加载模块、执行 #eval 或调用编译器内核。推断上，这种架构适合对安全性要求极高的金融、医疗或基础设施类应用，但可能因构建复杂度和性能损耗而不适合快速迭代的消费级产品。猜测部分，随着 WebAssembly 生态成熟，未来可能出现更多基于形式化验证的中间件或框架，但目前 Lasm 仍处于早期阶段，社区规模和文档完善度尚待观察。