Lasm - Write formally verified web apps in Lean for Node, serverless and edge
Show HN: Lasm – Write formally verified webapps in Lean for Node/serverless/edge
Lasm compiles ordinary Lean 4 programs ahead of time to WebAssembly, so a single Lean codebase can become a Node server, a serverless or edge function, a WASI/Fastly module, or a browser app. Because it is Lean, you can actually prove properties of the code you deploy. Its flagship example, Conduit, is the RealWorld app with 117 proved theorems covering authorization, pagination, slugs, and shared validation. Lasm ships on npm and bundles Lean, Lake, and its build tools — you only need Node, Bun, or Deno. Run `npm create @lasm@latest my-app` to start.
One Lean code base can become a Node server, a serverless or edge function, a WASI/Fastly module or a browser app — and because it is Lean, you can prove properties of the code you deploy.
- alexhixon
Interesting! Would've loved to see more frontend proofs, for example you have proofs about behavior but none on layout or design.
- orsorna
> I'm an agentic engineer with an emphasis in software engineering
This is odd. You wouldn't consider yourself a software engineer with an emphasis in...agentic engineering, or something like that? What is your background?
- sroerick
I think this is very interesting, but what are you specifying when you build a website?
I feel like this is the new "test driven development", which is totally a good idea, but also not totally useful for the actual process of building web apps, where most of your failure modes are weird CSS, JS, or server issues.
I would be happy to be proven wrong though