Lasm provides a bridge between formal verification and modern web deployment by allowing developers to write applications in Lean 4—a functional programming language and theorem prover—and compile them into WebAssembly (Wasm). Unlike standard web development where logic is verified primarily through unit tests, Lasm enables the use of formal proofs to guarantee that code behaves correctly according to specific rules. This approach allows developers to prove properties such as authorization logic, data validation, and pagination consistency before the code is ever deployed.
The image represents the core functionality of the Lasm toolchain for Lean 4 and WebAssembly.
The toolchain supports a wide range of deployment targets, including Node.js, AWS Lambda, Vercel, and Cloudflare Workers. It handles the complexities of different runtimes by providing specific build targets for each. For instance, while Node.js builds can utilize Lean's full runtime features like threads and sockets, edge and browser builds are optimized to run single-threaded without those specific capabilities. Lasm also provides a set of libraries, such as Lasm.Fetch for HTTP requests and Lasm.UI for browser interactions, to facilitate building full-stack applications while maintaining the ability to verify the underlying logic.
A key feature of Lasm is its ability to share verified logic between the client and the server. By defining a rule once in a shared Lean file, developers can prove that the browser application will never send an invalid request and that the server will only process requests that satisfy that same rule. This eliminates a common class of bugs where the frontend and backend disagree on validation logic. However, the system has defined boundaries: while the logic of the application is formally verified, the underlying JavaScript runtime, the SQL database execution, and the JSON serialization layer remain outside the scope of the formal proofs. This means the system guarantees the correctness of the application's internal logic rather than the absolute reliability of the entire infrastructure stack.