형식 검증(formal verification)은 오랫동안 항공·금융·암호학 같은 고신뢰 영역의 전유물로 여겨졌다. 증명 보조 도구를 다룰 줄 아는 전문 인력이 필요하고, 그렇게 검증한 코드를 실제 서비스로 배포하는 경로도 마땅치 않았기 때문이다. 최근 Show HN에 올라온 Lasm는 바로 이 마지막 간극을 겨냥한다. 증명 지향 언어인 Lean 4로 작성한 평범한 프로그램을 WebAssembly로 사전(ahead-of-time) 컴파일해, 하나의 코드베이스에서 Node 서버, 서버리스·엣지 함수, WASI/Fastly 모듈, 브라우저 앱을 만들어내는 도구다. Lean으로 짰기 때문에 배포하는 코드의 속성을 수학적으로 증명할 수 있다는 점이 핵심 차별점이다.
하나의 Lean 코드, 여러 런타임
Lasm는 npm으로 배포되며 Lean과 빌드 도구(Lake 포함)를 함께 가져오기 때문에, 사용자는 Node(또는 Bun·Deno)만 갖추면 된다. 새 머신에서 첫 빌드는 Lean과 도구를 한 번 내려받느라 약 250~275MB를 소비하며, Linux CI 러너 기준 19초가 걸렸다고 한다. 이후 한 줄 수정에 대한 개발 빌드는 1~2초 수준이다. 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 같은 엣지 환경까지 아우른다. 다만 런타임 능력에는 분명한 선이 그어져 있다. Node 빌드는 스레드·파일·프로세스·소켓을 갖춘 Lean의 완전한 런타임을 쓰지만, 엣지·Bun/Deno·WASI·브라우저 빌드는 단일 스레드로 돌며 소켓과 프로세스가 없다(WASI를 제외하면 파일도 없다). 나머지 Lean 기능은 동작한다.
증명되는 것과 증명되지 않는 것
대표 예제인 Conduit는 흔히 'Medium 클론'으로 불리는 RealWorld 앱을 REST API, 서버 렌더링 브라우저 앱, 증명까지 전부 Lean으로 작성한 것으로, 117개의 정리(theorem)가 증명되어 있다. 풀스택 템플릿은 서버(Lasm.Fetch), 브라우저 앱(Lasm.UI), 그리고 둘 사이의 API(Lasm.RPC)를 하나의 Lean 프로젝트로 묶고, 요청이 만족해야 하는 규칙을 Shared.lean에 한 번만 작성·증명해 양쪽이 공유하도록 설계됐다.
여기서 실무자가 주목해야 할 지점은 Lasm가 증명하지 않는 범위를 명확히 공개한다는 사실이다. 클라이언트와 서버 사이의 JSON/HTTP 전송, 실제 DOM에 패치를 적용하는 자바스크립트, Lasm 컴파일러와 런타임, 그리고 브라우저 자체는 증명 대상이 아니라 CI에서 테스트로 검증된다. Lean 자신의 컴파일러는 다른 Lean 프로그램과 마찬가지로 신뢰 기반(trusted)으로 둔다. 즉 '증명된 앱'이라는 표현이 전체 스택의 무결성을 보장하는 것은 아니며, 신뢰 경계가 어디까지인지 분명히 알고 써야 한다.
성능의 현실과 제약
이 접근에는 대가가 따른다. Node 위의 Lean은 WebAssembly와 그 스레드 비용을 치르며, 콜드 스타트는 CPU 바운드라 CPU 할당이 적은 서버리스 환경일수록 길어진다. 모든 자바스크립트 호출이 스레드 경계를 넘나든다는 점도 오버헤드다. 순수 Lean의 Std.Http는 Node에서 1,290 req/s로 느리기 때문에, 프로덕션 HTTP에는 Hono·Express·Fastify나 Lasm.Fetch를 쓰라고 권한다. 또한 큰 수 연산은 GMP(GNU MP) 대신 Lean 자체 임의정밀도 코드를 쓰므로 LGPL 코드가 섞이지 않는 장점이 있지만, 1만 자리 곱셈이 약 5배, Nat.gcd가 약 60배 느려진다.
배포 환경 요건도 가볍지 않다. Lean 툴체인은 v4.35.0로 고정되어 다른 버전은 거부되고, Node는 24 이상에 최소 512MB 메모리가 필요하며, Node 빌드는 약 22GB의 주소 공간을 예약하기 때문에 가상 메모리를 제한하는 호스트에서는 실행을 거부한다. 미리 빌드된 네이티브 라이브러리(libcurl, OpenSSL, libpq 등)는 링크할 수 없다는 제약도 있다.
종합하면 Lasm는 '검증된 코드를 어디서나 돌린다'는 이상과, 엣지·서버리스 런타임의 물리적 한계 사이에서 타협점을 설계한 실험적 프로젝트다. 라이선스는 본체가 MIT, 생성되는 스타터 코드는 저작자 표기조차 필요 없는 MIT-0로 열려 있고, 제작자는 월 250달러 후원을 첫 목표로 내걸고 있다. 당장 프로덕션에 올리기보다는, 핵심 비즈니스 규칙을 증명으로 못 박고 싶은 일부 경로나 사이드 프로젝트에서 형식 검증의 실용성을 가늠해 보는 용도로 접근하는 편이 현실적이다.