Show HN: Lasm – Write formally verified webapps in Lean for Node/serverless/edge

Category: devtools

Tags: lean4, webassembly, formal-verification, serverless, edge-computing

Score: 8.5/10 (Innovation: 9, Technical: 9, Documentation: 9, Utility: 7)

Lasm compiles Lean 4 programs ahead-of-time to WebAssembly, enabling formally verified web applications that can deploy to Node, serverless, edge, and browser targets. Its flagship RealWorld app demonstrates 117 proved theorems covering authorization, data integrity, and pagination, with conformance tests across multiple platforms.

Target audience: backend devs, devops, researchers interested in formal verification

Repository: https://github.com/Millillion/lasm · C · MIT · 21 stars

View on Hacker News