开发者发布 Lasm：用 Lean 编写可形式化验证的 Web 应用
Show HN: Lasm – Write formally verified webapps in Lean for Node/serverless/edge
开发者 lastmjs 发布 Show HN 项目 Lasm，可将 Lean 语言带到浏览器、Node、serverless 和 edge 环境，支持从前端到后端用 Lean 编写并形式化验证 Web 应用，例如运行在 Cloudflare Workers 上并对其规格做形式化验证的 Express 或 Hono 服务器。
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.
来源：Hacker News · 首页 · news.ycombinator.com