ONEDEV

Lasm이 Lean 4 코드를 WebAssembly로 컴파일해 증명까지 함께 배포한다

Hacker News그저께

Lean 4로 쓴 프로그램을 WebAssembly로 미리 컴파일해, 하나의 코드베이스로 Node 서버와 서버리스 함수, 엣지 런타임 모듈, 브라우저 앱까지 배포하는 도구 Lasm이 공개됐다. 핵심은 컴파일 결과물이 그냥 동작하는 수준이 아니라, Lean의 증명 기능을 그대로 활용해 배포되는 코드의 성질을 정리(theorem)로 보장할 수 있다는 점이다.

배포 형태는 `@lasm/cli` 패키지(0.3.5)로 npm에 올라와 있고, Lean은 4.35.0 버전으로 고정된다. Lean과 Lake, 빌드 도구를 CLI가 함께 가져오기 때문에 elan 같은 별도 툴체인 관리자 없이 Node만 있으면 된다. Node 24 이상을 기준으로 24.0.0, 24.22.1, 26.12.1에서 테스트됐고, Bun 1.4.4와 Deno 2.9.6도 단독 런타임으로 검증됐다. 빌드 머신은 Linux x64·arm64(glibc 2.34 이상), macOS x64·arm64, Windows x64를 지원한다. 파일 하나짜리 프로그램은 프로젝트 없이 `npx @lasm/cli Main.lean`으로 바로 빌드·실행된다.

타깃은 상당히 넓다. Node 서버나 일반 프로그램, AWS Lambda·Vercel·Netlify·Azure·Google Cloud Functions 같은 서버리스, Cloudflare Workers·Deno Deploy·Supabase 같은 엣지, Fastly Compute와 wasmtime·wasmer·node:wasi 기반 WASI, wasi-http(wasmtime serve, Spin), 그리고 주요 브라우저까지 같은 소스를 가지고 나간다. Hono·Express·Fastify 템플릿과 Lambda zip, Workers, Fastly 등 배포용 레시피가 플래그(`--deploy`)로 제공된다.

가장 눈에 띄는 것은 플래그십 예제인 Conduit이다. Medium 클론으로 알려진 RealWorld 앱을 REST API, 서버 렌더링 브라우저 앱, 증명까지 전부 Lean으로 작성했고 117개의 정리를 `sorry` 없이 Lean의 표준 공리만 사용해 검증했다. 증명이 다루는 범위는 작성자만 자신의 글과 댓글을 수정할 수 있다는 권한 규칙, 팔로우와 즐겨찾기, 슬러그가 충돌하지 않는다는 성질, 페이지네이션이 항목을 건너뛰거나 중복하지 않는다는 성질, 클라이언트와 서버가 같은 검증 로직을 공유해 서버가 거부할 요청을 앱이 보내지 않는다는 성질, JSON 왕복, 마크다운 링크 안전성 등이다. 엔드포인트는 함수 저장소(Store) 위에 작성되고, 증명은 같은 코드를 테이블 모델 위에서 실행해 확인한다.

물론 증명되지 않고 신뢰하는 층도 분명히 밝혀져 있다. 각 SQL 문이 모델대로 동작한다는 가정, JSON 텍스트 계층, 요청 간 동시성, 그리고 Lean과 Lasm, JavaScript 런타임 자체다. RealWorld 스펙 전체와의 일치 여부는 증명이 아니라 테스트로 확인한다. 공식 RealWorld API 스위트는 수정 없이 13개 파일, 154개 요청을 Node(node:sqlite), Cloudflare Workers(D1), Bun(bun:sqlite)에서 통과했다. 프런트엔드는 Lasm.UI로 공식 템플릿을 구현했고 서버 사이드 렌더링과 하이드레이션, Lean으로 파싱한 마크다운을 포함한다. 공식 Playwright 엔드투엔드 스위트도 Node에서 Chromium·Firefox·WebKit, Workers와 Bun에서 Chromium으로 재시도 없이 통과했다.

배경에는 정적 타입 검사가 컴파일 시점까지만 책임진다는 오랜 공백이 있다. 테스트는 배포된 코드의 모든 경로를 보장하지 못하고, 런타임에서 드러나는 권한·불변식 위반은 사후에야 발견된다. Lasm은 Lean 4의 커널과 정교한 타입 시스템을 웹 런타임에 얹어, "무엇을 배포하는가"와 "그것이 어떤 성질을 만족하는가"를 같은 언어 안에서 다루려 한다. HTTP용 `Lasm.Fetch`, 브라우저용 `Lasm.UI`(Elm 아키텍처, diff 증명 포함), 타입 있는 클라이언트·서버 API를 위한 `Lasm.RPC`, DOM과 웹 API를 위한 `Lasm.Web`, 키-값 저장용 `Lasm.KV` 같은 모듈이 함께 제공된다.

실무 관점에서 눈여겨볼 부분은 기존 JavaScript 생태계와의 접점이다. `import Lasm.JS`를 추가하고 호출할 함수마다 `@[js "pkg" "export"]` 한 줄을 붙이면 npm 패키지를 그대로 부를 수 있다. 미리 만들어진 바인딩은 없고, RealWorld 예제도 타깃마다 손으로 작성한 바인딩 모듈 하나씩을 둔다. 빌드 비용은 첫 빌드에서 Lean과 도구를 한 번 내려받는 250~275MB가 발생하고 Linux CI 러너 기준 19초가 걸렸으며, 이후 한 줄 수정 빌드는 1~2초 수준이다. `npm run dev`는 저장 후 약 2초 만에 재빌드하고 서버를 재시작하며, 타입 오류가 나면 마지막 정상 빌드를 계속 돌린다.

런타임별 제약은 분명히 갈린다. Node 빌드는 스레드, 파일, 프로세스, 소켓을 포함한 Lean 전체 런타임을 쓰지만, 엣지와 Bun·Deno, WASI, 브라우저 빌드는 단일 스레드로 돌고 소켓과 프로세스가 없으며 WASI를 제외하면 파일도 없다. 또한 Lasm은 wrangler나 vercel 같은 플랫폼 자체 CLI를 설치하거나 실행하지 않으므로 배포 단계는 사용자가 직접 수행해야 한다. 프로젝트 정책상 CI는 실제 클라우드 계정에 배포하지 않고, 각 타깃을 해당 플랫폼의 로컬 런타임이나 이미지, 에뮬레이터로만 검증한다. 라이선스는 Lasm이 MIT, 템플릿과 예제, README 코드 샘플은 MIT-0이다.