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

Lasm is an npm-distributed tool from Millillion that compiles Lean 4 programs to WebAssembly for Node, serverless and edge platforms, WASI, and browsers. Its flagship example is a Lean implementation of the RealWorld app with 117 proved theorems; the project says those proofs cover properties including authorization and pagination, while the compiler, runtime, and parts of the data and transport layers remain trusted or tested rather than proved.