Lasm
Write formally verified webapps in Lean for Node/serverless/edge
Get picks like this daily. Today's launch numbers, the top launches, AI and tech news, and a daily opportunity pick, straight to your inbox.
Read the full description
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.
Visit website ↗ Source listing ↗
HN · launched Oct 30, 2026 · 36 upvotes (top 23%)
- Horizontal
- Dev tools
- Developer
- Not AI
- Hobby / open-source project
Similar launches
See all 44 similar launches →Could you build this?
No It requires a compiler or transpiler from Lean to JavaScript for Node, serverless, and edge runtimes, plus a verified web framework. That is research-grade programming-language and formal-methods work.
What it would actually take: The stack would be Lean 4 with its metaprogramming and code generation, a verified or proof-carrying model of HTTP and app state, and a JS backend target. Vibe coding can scaffold surface syntax, but correctness proofs and sound compilation need experts in dependent types and formal verification.
Discussion
20 comments analyzed.
Concerns raised: 'Agentic engineering' misuses the engineering term, Software development not actually solved by AI agents, Unclear who instructs the AI and how non-technical teams would use it, Hype-heavy promotional wording
Feature requests: More frontend proofs covering layout and design
Competitors
Other products that read as similar to this one : 44 launches clear the similarity bar, closest 8 shown.
Attention rank: #16 of 45 (itself plus its competitors, highest first, normalized so YC and Product Hunt are compared fairly).
Launched 363 days after the earliest competitor.
- Talos · hn · 2026-06-18 · 106 upvotes · similarity 0.52
- Formally Verified Leaderless Log Protocol for Kafka · hn · 2026-04-10 · 5 upvotes · similarity 0.46
- LeanCIL · github · 2026-10-14 · 49 upvotes · similarity 0.44
- h5i · ph · 2026-10-24 · 1 upvotes · similarity 0.44
- Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code · hn · 2026-07-28 · 115 upvotes · similarity 0.43
- A malleable and formally verified Web engine · hn · 2026-10-29 · 6 upvotes · similarity 0.40
- An application stack Claude coded directly in LLVM IR · hn · 2026-03-12 · 10 upvotes · similarity 0.40
- LemmaScript, a verification toolchain for TypeScript via Dafny · hn · 2026-04-21 · 5 upvotes · similarity 0.40
Other launches for this product
- No other launches for this product.