Lasm компилирует Lean 4 в WebAssembly для Node и edge-функций

Lasm, проект, который заранее (ahead of time) компилирует обычные программы на Lean 4 в WebAssembly. Из одной кодовой базы на Lean можно получить сервер на Node, serverless- или edge-функцию, модуль для WASI/Fastly или браузерное приложение. Поскольку это Lean, говорится в README, можно доказывать свойства кода, который вы разворачиваете. Lasm выходит на npm и приносит с собой Lean, Lake и инструменты сборки; из окружения нужен только Node (или Bun, или Deno). Проект создаётся командой npm create @lasm@latest my-app -- --template hono.

Главный пример, Conduit, приложение RealWorld (клон Medium), целиком написанное на Lean: REST API, серверный рендеринг браузерного приложения и доказательства. В нём 117 теорем о коде, который реально выполняется; они проверены без sorry и только со стандартными аксиомами Lean (команда npm run proofs, каждая теорема описана простым языком в PROOFS.md). Теоремы покрывают авторизацию (статьи и комментарии меняют только их авторы), подписки и избранное, слаги без коллизий, пагинацию без пропусков и повторов, валидацию, общую для клиента и сервера (приложение не отправляет то, что сервер отклонит), JSON-круговые преобразования и безопасность ссылок в Markdown. Эндпоинты написаны поверх абстрактного хранилища (Store) из функций, а доказательства прогоняют тот же код на модели таблиц.

Автор прямо разделяет доказанное и принятое на веру. Не доказано, а лишь предполагается: что каждый SQL-запрос делает то, что говорит его модель; текстовый слой JSON; конкурентность между запросами; а также Lean, Lasm и среда выполнения JavaScript. Соответствие всей спецификации RealWorld проверено тестами, а не доказано. Официальный набор тестов API RealWorld проходит без изменений (13 из 13 файлов, 154 запроса) на Node (node:sqlite), Cloudflare Workers (D1) и Bun (bun:sqlite). Официальный сквозной набор Playwright проходит без повторных запусков на Node в Chromium, Firefox и WebKit, а на Workers и Bun, в Chromium. Всё это выполняется в CI (прогон conduit.yml с @lasm/cli 0.3.4).

Разработка: первая сборка на новой машине скачивает Lean и инструменты (около 250-275 МБ; 19 с на Linux-раннере CI), последующие dev-сборки после правки одной строки занимают около 1-2 с. Команда npm run dev (lasm dev) пересобирает проект примерно через 2 с после каждого сохранения, перезапускает сервер и при ошибке типов оставляет работать последнюю удачную сборку. Есть рецепты для Node-сервера (Hono, Express, Fastify, std-http, fetch), AWS Lambda, Vercel, Netlify, Azure и Google Cloud Functions, Cloudflare Workers (а также Vercel Edge, Netlify Edge, Deno Deploy, Supabase), Fastly Compute, WASI и Spin, браузерного приложения и шаблона fullstack. Lasm сам не устанавливает и не запускает CLI платформ (wrangler, vercel, fastly): их запускает пользователь. По политике проекта CI никогда не деплоит в реальный облачный аккаунт, платформы проверяются локальными средами выполнения, образами или эмуляторами.

В шаблоне fullstack сервер (Lasm.Fetch), браузерное приложение (Lasm.UI) и API между ними (Lasm.RPC), один проект на Lean. Правило проверки запроса записано и доказано один раз в Shared.lean, который импортируют обе стороны: сервер при сохранении записи требует доказательство, что заголовок прошёл проверку, а для клиента доказана теорема, что приложение никогда не отправит неверный заголовок. Не доказано, а проверяется в CI: JSON/HTTP-транспорт между клиентом и сервером, JavaScript, применяющий патчи к реальному DOM, компилятор и среда выполнения Lasm и браузеры. Для вызова JavaScript-функций объявляется привязка одной строкой (@[js "module" "export"]); тип на Lean определяет преобразование значений, а lasm build проверяет привязки по установленному пакету. Каждый вызов с потока Lean на главный поток Node стоит около 24 мкс, поэтому лучше делать один крупный вызов вместо многих мелких.

Ограничения перечислены в README. Lean на Node платит за WebAssembly и потоки: холодный старт упирается в процессор и растёт на малых долях CPU в serverless, а Std.Http, целиком написанный на Lean, на Node медленный (1,290 запросов в секунду), поэтому для продакшена советуют Hono, Express, Fastify или Lasm.Fetch. Арифметика над числами с тысячами цифр медленнее, чем в нативном Lean (нет GMP). Только компиляция заранее: развёрнутая программа не может разбирать, вычислять или компилировать Lean. Поддерживается ровно Lean 4.35.0, другие версии отвергаются. Для Node-приложения нужно не меньше 512 МБ памяти (резервируется около 22 ГБ виртуального адресного пространства). Сборки для edge, Bun/Deno, WASI и браузера выполняют Lean в одном потоке, без сокетов и процессов. Готовых привязок к npm-пакетам нет, нет сборок для Windows ARM64 и машин сборки на Alpine/musl (собранные приложения на Alpine работают). Цифры производительности получены в CI на бесплатном раннере GitHub (4-ядерный AMD EPYC, Linux x64) на сборке-кандидате 0.1.0-experimental.40494203854 от 2026-10-27. Автор просит о спонсорской поддержке проекта.

Ключевые факты

Lasm заранее компилирует обычные программы на Lean 4 в WebAssembly: один код становится сервером на Node, serverless- или edge-функцией, модулем WASI/Fastly или браузерным приложением.
Образец Conduit (приложение RealWorld) идёт со 117 доказанными теоремами: авторизация, слаги без коллизий, пагинация, общая валидация клиента и сервера и другое; проверка без sorry и только со стандартными аксиомами Lean.
Официальный набор API RealWorld проходит без изменений (13 из 13 файлов, 154 запроса) на Node, Cloudflare Workers и Bun; Playwright-тесты проходят на Node в трёх браузерах, на Workers и Bun, в Chromium.
Принято на веру, а не доказано: соответствие SQL-запросов модели, текстовый слой JSON, конкурентность запросов, а также Lean, Lasm и среда JavaScript.
Ограничения: ровно Lean 4.35.0, Std.Http, целиком написанный на Lean, на Node даёт 1,290 запросов в секунду, для Node-приложения нужно не меньше 512 МБ памяти.

Почему это важно

Проект пытается соединить формальные доказательства на Lean с привычными целями развёртывания: Node, serverless и edge, а не только с экспериментальными программами. Конкретный пример, Conduit с 117 теоремами о коде, который реально выполняется, а правило валидации, доказанное один раз в Shared.lean, действует и в браузере, и на сервере. При этом проект новый: это экспериментальная сборка, а публичных описаний боевого использования в тексте README нет.

Кому это важно

Разработчикам на Lean, которые хотят выкатывать свой код на Node, в облачные функции или в браузер; тем, кто интересуется формальной верификацией прикладного веб-кода (авторизация, пагинация, валидация); командам, которым нужна одна проверяемая логика на клиенте и на сервере.

Как это применить

Создать проект командой npm create @lasm@latest my-app -- --template hono (нужен только Node, Bun или Deno; Lean, Lake и инструменты сборки приедут с пакетом) и запустить npm run dev. Для одного файла достаточно Main.lean и команды npx @lasm/cli Main.lean. Образец доказательств: в examples/conduit команда npm run proofs проверяет все 117 теорем. Для деплоя выбирается шаблон под платформу (--deploy lambda-zip, workers, fastly и др.), а CLI самой платформы запускается вручную. Для продакшен-HTTP на Node рекомендованы Hono, Express, Fastify или Lasm.Fetch. Цена или условия лицензии в доступной части README не указаны.

Можно ли доверять

Источник, README самого проекта, то есть самоописание; независимых проверок в тексте нет. Результаты тестов и измерения получены в CI на бесплатном раннере GitHub и привязаны к конкретному прогону и версии @lasm/cli 0.3.4, а числа производительности, к сборке-кандидату от 2026-10-27. Имя автора или организации в выдержке не названо, сведений об использовании в продакшене нет. Сильная сторона README, честный список того, что не доказано. Важно не читать заголовок как «всё приложение формально верифицировано»: доказаны только перечисленные свойства Conduit.

Риски и подводные камни

Доказаны не все части системы: SQL-запросы, текстовый слой JSON, конкурентность и сама среда выполнения остаются на доверии, а соответствие спецификации RealWorld только протестировано. Жёсткая привязка к Lean 4.35.0. Std.Http, целиком написанный на Lean, на Node медленный (1,290 запросов в секунду), каждый вызов между потоком Lean и главным потоком Node стоит около 24 мкс, холодный старт растёт на малых долях CPU. На edge, в Bun/Deno, WASI и браузере Lean однопоточный, без сокетов и процессов. Приложению на Node нужно не меньше 512 МБ памяти. Нет сборок под Windows ARM64, готовых привязок к npm-пакетам нет, а развёрнутая программа не умеет компилировать и вычислять Lean. По политике проекта CI не деплоит в реальные облачные аккаунты, платформы проверяются локально.

«Раз это Lean, можно доказывать свойства кода, который вы разворачиваете.»

— README проекта Lasm