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

Lasm is a project that brings the Lean programming language, which supports formal verification, to the browser, Node, serverless, and edge environments. It allows developers to write formally verified web applications, including front-end to back-end development, and provides a unified codebase that can be compiled to different platforms such as Node servers, serverless functions, and browser apps. Lasm uses Lean 4 and compiles ordinary Lean 4 programs ahead of time to WebAssembly, enabling developers to prove properties of their code. The project is open-source and available on npm, with a flagship example, Conduit, a Medium clone with 117 proved theorems.