Lasm es una herramienta de compilación que permite traducir programas en Lean 4 a WebAssembly, facilitando la ejecución en entornos JavaScript y WebAssembly. A diferencia de otros compiladores, Lasm genera código ahead-of-time que puede desplegarse como servidores Node.js, funciones serverless, módulos WASI o aplicaciones para navegadores. Su principal ventaja técnica es la capacidad de demostrar propiedades formales del código antes de su despliegue, garantizando la corrección lógica de la aplicación final.
El proyecto, disponible en npm, incluye Lean 4, Lake y sus herramientas de construcción, requiriendo solo Node.js, Bun o Deno para su ejecución. La versión actual es 0.3.5, compatible con sistemas operativos Linux, macOS y Windows, y soporta compilación en Node.js 24 y superior, así como en Bun y Deno. El ejemplo insignia, Conduit, es una aplicación RealWorld que incluye 117 teoremas probados, demostrando la viabilidad de la verificación formal en aplicaciones complejas.
Lasm ofrece plantillas para frameworks como Hono, Express y Fastify, y soporta despliegue en múltiples plataformas, incluyendo AWS Lambda, Vercel, Netlify, Cloudflare Workers y Fastly Compute. La interacción con JavaScript se realiza mediante importaciones directas, sin necesidad de bindings predefinidos. El proyecto mantiene una licencia MIT y está diseñado para desarrolladores que buscan integrar la verificación formal en sus flujos de trabajo de desarrollo web.