alt Hacker NewsShow HN: Lasm – Write formally verified webapps in Lean for Node/serverless/edge
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.
Comments
Oh boy! My favorite thing about vibe coding is when agents write tests that assert whether certain strings exist in the codebase. Now we can formally verify that they do!
This is wild, I had no idea Lean could be used for things like this.
> 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?