Lasm compila Lean 4 a WebAssembly para Node y edge

Lasm: Lean 4 compilado a WebAssembly, con pruebas incluidas

Lasm es un proyecto de código abierto que compila programas de Lean 4 a WebAssembly de forma anticipada (ahead of time). La propuesta es directa: una sola base de código en Lean puede convertirse en un servidor Node, una función serverless o de edge, un módulo WASI/Fastly o una app de navegador. Y como el lenguaje es Lean, se pueden demostrar propiedades del código que efectivamente se despliega.

La versión actual es @lasm/cli 0.3.5 y el proyecto fija Lean en la versión exacta 4.35.0. Se instala desde npm con npm install -D @lasm/cli o directamente con npx @lasm/cli, y el propio paquete trae Lean, Lake y sus herramientas de build: solo se necesita Node (o Bun o Deno).

Para un founder técnico, la pregunta relevante no es si Lean es elegante, sino cuánto cuesta adoptarlo. Lasm intenta bajar esa barrera al máximo: npm create @lasm@latest my-app -- --template hono genera un proyecto listo para desarrollo.

¿Y esto cómo se aplica en tu negocio?

Dueños de negocio de Latinoamérica y España usan un agente de IA para ganar más y recuperar su tiempo. El Kit «tu mano derecha con IA» te muestra cómo en un video de 11 minutos, con una ficha para armar el tuyo. CAR está cerrada por ahora; al anotarte, te avisamos cuando abra.

👥 Quiero el Kit →

¿Qué se puede probar y qué queda fuera de la prueba?

El ejemplo insignia es Conduit, una implementación de la app RealWorld (un clon de Medium) escrita enteramente en Lean: la API REST, el frontend renderizado en servidor y las pruebas formales. Acumula 117 teoremas sobre el código que realmente corre, verificados sin sorry y usando solo los axiomas estándar de Lean.

Esos teoremas cubren cosas concretas y útiles para un producto:

Autorización: solo los autores pueden modificar sus artículos y comentarios.
Slugs que nunca colisionan y paginación que no salta ni repite elementos.
Validación compartida entre cliente y servidor: la app nunca envía lo que el servidor rechazaría.
Seguridad de enlaces en Markdown y round trips de JSON.

La honestidad del README es un punto a favor: aclara qué no está probado. Quedan fuera de la demostración la correspondencia entre cada sentencia SQL y su modelo, la capa de texto JSON, la concurrencia entre requests, y el propio compilador y runtime de Lean, Lasm y JavaScript. La conformidad con la especificación completa de RealWorld se testea, no se prueba. Esa distinción importa: confundir "probado" con "testeado" es el error clásico al evaluar herramientas de verificación formal.

Los números medidos: ¿aguanta producción?

El proyecto publica benchmarks tomados en un runner gratuito de GitHub (4 CPU AMD EPYC, Linux x64). Son cifras concretas y vale la pena mirarlas con ojo crítico:

Cold start de una app Hono con handler en Lean hasta la primera respuesta HTTP: 159 ms.
Throughput: 24.911 req/s con p99 de 4,2 ms, frente a 103.134 req/s de un http de Node puro (es decir, 0,24×).
Express con handler en Lean: 18.678 req/s.
Tamaño: el program.wasm comprimido con brotli pesa 166 KiB; el dist/ completo, 8,5 MiB más 1,4 MiB de node_modules.
Memoria: 148 MiB RSS en reposo y 329 MiB bajo carga.
Costo de interoperabilidad: cada llamada de Lean a JavaScript cruza de hilo y cuesta unos 24 µs (p50).
Cloudflare Workers: bundle de 1,40 MiB, 245 KiB gzip (el límite de la plataforma es 64 MiB).
Navegador: la app contador transfiere 152 KiB brotli y pinta el primer frame en 30 ms en Chromium.
Build: 4,7 s una compilación limpia y 2,0 s un rebuild de desarrollo tras cambiar una línea.

El propio README es explícito sobre el costo: Lean sobre Node "paga" por WebAssembly y sus hilos. El cold start es intensivo en CPU, así que empeora en shares pequeños de CPU serverless, y cada llamada a JavaScript cruza hilos. También advierte que un Std.Http puro en Lean es lento (1.290 req/s) y recomienda Hono, Express, Fastify o Lasm.Fetch para HTTP en producción.

Plataformas soportadas y límites conocidos

La matriz de despliegue es amplia y cada fila se testea en CI con el runtime local de la plataforma. Cubre Node (Docker/Kubernetes, Cloud Run, Fly.io, Railway, Render, Heroku, DigitalOcean), AWS Lambda en .zip y en contenedor, Lambda@Edge, Vercel Functions y Vercel Edge, Netlify Functions y Netlify Edge, Azure Functions, Google Cloud Functions gen2, Cloudflare Workers, Deno Deploy, Supabase Edge Functions, Bun, Deno, Fastly Compute, WASI, wasi-http (wasmtime serve, Spin) y navegadores.

Hay una diferencia importante según el destino: los builds de Node tienen el runtime completo de Lean (hilos, archivos, procesos, sockets), mientras que los builds de edge, Bun/Deno, WASI y navegador corren Lean en un solo hilo, sin sockets ni procesos (y sin archivos, salvo en WASI).

Los límites declarados:

Solo ahead of time. Un programa desplegado no puede elaborar, evaluar ni compilar Lean en tiempo de ejecución. Las pruebas, tácticas, macros y #eval corren al compilar.
Lean 4.35.0 exactamente. Otras versiones de lean-toolchain se rechazan con un mensaje.
Node: hay que darle al menos 512 MB a la app, y reserva alrededor de 22 GB de espacio de direcciones virtual.

¿Qué significa esto para tu startup?

La verificación formal dejó de ser un tema exclusivamente académico, pero sigue siendo cara en tiempo de ingeniería. Lo interesante de Lasm no es que Lean sea poderoso —lo es—, sino que reduce la fricción de adopción a un npm create y despliega en las plataformas que ya usas.

Dicho eso, la decisión no es binaria. El propio proyecto muestra el trade-off: pagas rendimiento y memoria a cambio de garantías. Para un equipo pequeño, el cálculo razonable es acotado.

Dos acciones concretas:

Aísla la lógica crítica, no todo el backend. No reescribas tu API en Lean. Identifica las reglas donde un bug cuesta dinero o confianza —validación de montos, permisos, reglas de facturación, invariantes de inventario— y prueba solo esa capa. El patrón de Conduit es replicable: un Store de funciones con pruebas que corren sobre un modelo de las tablas.
Mide antes de comprometerte. Levanta un endpoint real con el template hono y corre tus propias pruebas de carga contra tu baseline en Node puro. Los benchmarks del proyecto son de un runner de CI; tu tráfico, tu cold start y tu presupuesto de memoria son otros.

Un tercer punto de higiene: lee FUNDAMENTAL_LIMITATIONS.md y IO_LIMITATIONS.md antes de prometer nada a un cliente. Saber qué no está probado es tan valioso como saber qué sí lo está.

Conclusión

Lasm es una apuesta poco común: llevar Lean 4 al mundo JavaScript y WebAssembly sin obligar al equipo a abandonar npm ni a operar infraestructura nueva. Con 117 teoremas en su app de referencia y una matriz de despliegue que cubre desde Node hasta Cloudflare Workers, ofrece un camino concreto para probar propiedades del código en producción.

El costo está declarado sin adornos: menos throughput que Node puro, más memoria y una versión de Lean fijada. Para startups con lógica de negocio donde un error es caro, ese intercambio puede tener sentido. Para el resto, sigue siendo una herramienta a observar de cerca.

No se encontraron datos adicionales verificables en la búsqueda web para complementar esta nota; todo lo anterior proviene del repositorio oficial del proyecto.