Lasm: 증명한 Lean 코드를 Node 에서 실행하기

무엇이 문제인가

웹 앱의 테스트는 미리 지정한 입력에서만 코드의 결과를 확인한다. "글은 작성자만 고칠 수 있다" 같은 규칙이 모든 요청에서 지켜지는지는 테스트로 확인할 수 없다.

제작자는 README 에서 Lasm 의 성능을 Node 의 기본 http 서버와 비교했다. TypeScript 공식 핸드북에 따르면 TypeScript 의 타입 시스템은 컴파일할 때 안전한지 알 수 없는 연산도 허용한다. TypeScript 의 타입은 값의 형태를 확인할 뿐, 함수의 결과가 어떤 규칙을 지키는지는 표현하지 못한다.

어떻게 해결했나

Lasm 은 2026년 10월 30일 Hacker News 에 Show HN 글로 올라왔다. 사용자는 서버 코드를 LeanLean프로그래밍 언어이자 증명 보조기다. 함수와 함께 그 함수가 만족하는 성질을 정리로 작성하고 증명하면, Lean 이 컴파일할 때 증명이 타당한지 검사한다. 으로 작성하고, 같은 프로젝트에 코드가 지켜야 할 규칙을 정리로 작성해 증명한다. 빌드할 때 Lean 이 증명을 검사한다. Lasm 은 검사를 통과한 코드를 WebAssembly 로 컴파일한다.

결과물은 Node 서버, 서버리스서버리스서버를 직접 운영하지 않고, 요청이 올 때마다 클라우드가 함수를 실행해 주는 배포 방식이다. 함수, 브라우저 앱 가운데 하나가 된다. Lean 컴파일러와 빌드 도구는 npm 패키지에 들어 있어, 사용자는 Node 만 설치하면 된다. 사용자는 웹 프레임워크 Hono 같은 npm 패키지의 함수마다 바인딩바인딩다른 언어로 작성한 함수를 호출할 수 있도록, 호출하는 언어에서 그 함수의 이름과 타입을 선언한 것이다.을 선언해 Lean 에서 호출한다.

무엇이 다른가

첫째, 규칙을 확인하는 방법이 다르다. Lasm 에서는 규칙이 모든 입력에서 성립한다는 증명을 Lean 이 검사한다. 증명이 잘못되면 빌드가 실패해 그 코드는 배포할 수 없다. README 의 예제 Conduit 은 Medium 을 본뜬 블로그 앱이다. 제작자는 작성자만 글을 고칠 수 있다는 규칙을 포함해 정리 117개를 증명했다고 밝혔다. 다만 README 에 따르면 SQL 문이 증명에 쓴 테이블 모델대로 작동하는지, JSON 텍스트를 올바르게 읽고 쓰는지, 동시에 들어오는 요청을 올바르게 처리하는지는 증명 범위 밖이다. 증명은 Lean 과 Lasm, JavaScript 런타임이 올바르다고 가정한다.

둘째, 실행하는 방식이 다르다. TypeScript 는 JavaScript 로 컴파일돼 Node 가 그대로 실행한다. Lasm 은 Lean 코드를 WebAssembly 로 컴파일해, 증명한 코드를 JavaScript 런타임 안에서 실행하고 npm 패키지를 호출할 수 있게 한다. README 에 따르면 Node 에서 Lean 코드는 WebAssembly 스레드에서 실행되고, JavaScript 를 호출할 때마다 스레드를 넘나든다. 트레이드오프는 이 때문에 처리량이 기본 http 서버보다 낮다는 점이다. README 에 따르면 앱마다 메모리도 512 MB 이상 할당해야 한다.

어떻게 만들었나

• 커밋 1,180개는 2026년 9월 17일부터 10월 28일까지 작성됐다. 그중 605개에 Claude 와 함께 작성했다는 Co-authored-by 트레일러가 있다.
• README 에는 AI 에이전트를 위한 안내 파일(llms.txt, docs/AI.md)의 링크가 있다.
• README 의 성능 표는 모두 GitHub 의 무료 4 CPU 러너에서 측정한 값이다. 제작자는 측정에 쓴 CI 실행 번호도 함께 밝혀, 그 실행의 기록을 찾아볼 수 있게 했다.

실행해 보니

Node 24 로 README 의 명령을 따라 Hono 템플릿 앱을 만들어 빌드하고 실행했다.

1. 설치. npm create @lasm@latest app -- --template hono 와 npm install 이 20초 만에 끝났다. node_modules 는 674 MB 였다.
2. 빌드. 첫 npm run build 는 50초가 걸렸다. 이때 홈 디렉토리의 .cache/lasm 에 캐시 2.7 GB 가 생겼다. dist 를 지우고 다시 빌드하는 데는 1.6초가 걸렸다. program.wasm 은 783 KB 였다.
3. 실행. node dist/main.mjs 로 서버 프로세스를 시작해 첫 요청에 응답하기까지 292 ms 가 걸렸다. /hello/Ada 는 Lean 함수가 만든 인사말을 JSON 으로 반환했고, POST /echo 는 한글이 든 JSON 을 그대로 반환했다.
4. 증명. App.lean 에 greet 함수에 대한 정리 두 개를 추가하자 빌드가 9초 만에 통과했다. 하나는 greet "Ada" 의 결과가 정해진 인사말이라는 정리이고, 다른 하나는 모든 이름에 대해 인사말이 같은 형식이라는 정리다. 결과에 Ada 대신 Bob 이 들어간다는 잘못된 정리를 넣자 빌드가 0.8초 만에 실패했다.
5. 처리량. autocannon 으로 연결 50개를 8초 동안 유지하며 요청을 보내자 Lasm 서버는 초당 10,058건을 처리했다. 직접 작성한 Node 기본 http 서버는 같은 컴퓨터에서 초당 64,510건을 처리했다. Lasm 서버의 처리량은 Node 기본 http 서버의 0.16배로, README 의 0.24배보다 낮았다. 제작자는 서버와 부하 도구가 서로 다른 코어를 쓰도록 지정해 측정했다. 오늘은 부하 도구를 서버와 같은 4코어 컴퓨터에서, 프로세스마다 사용할 코어를 지정하지 않고 실행했다. 이 조건이 두 서버에 같은 영향을 주는지는 확인하지 못했다.
6. 메모리. 부하 중 서버의 메모리 사용량은 358 MB 로, README 에서 안내한 최소 할당량 512 MB 보다 적었다.

App.lean:11:67: error: Tactic `decide` proved that the proposition
[lasm] Build failed. Fix the error above and run the command again.

확인하지 못한 것

• Conduit 의 정리 117개. 예제 디렉토리에서 npm run proofs 를 실행하고, 정리를 PROOFS.md 의 설명과 대조하자.
• 다른 배포 대상. 같은 앱을 --target workers 와 --target bun 으로 빌드해 Cloudflare Workers 와 Bun 에서 응답하는지 확인하자.

판정

작동한다. Lean 으로 작성한 서버가 응답했고, 잘못된 정리를 넣자 빌드가 실패했다. 다만 처리량은 Node 기본 서버보다 크게 낮았다. 권한 규칙처럼 잘못되면 안 되는 서버 로직을 증명하고 싶은 경우에 써 볼 만하다.