# Lasm：用 Lean 4 编写可形式化验证的 Web 应用，编译到 Node、Serverless 与边缘平台

> 原标题：Show HN: Lasm – Write formally verified webapps in Lean for Node/serverless/edge

- 来源：Hacker News 首页
- 发布时间：2026-10-30T02:05:41.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/rsmpt2e1q7332pdqc99j6cnjp
- 原文：https://github.com/Millillion/lasm

## 摘要

Lasm 将普通 Lean 4 程序提前编译为 WebAssembly，同一份代码可部署为 Node 服务器、Serverless 或边缘函数、WASI/Fastly 模块及浏览器应用，并支持对部署代码进行性质证明。