# Lasm: 증명한 Lean 코드를 Node 에서 실행하기 # Lasm: running proven Lean code on Node - Site: https://select1.dev/2026-10-31 (English), https://select1.dev/ko/2026-10-31 (Korean) - Entry: 021 - Published: 2026-10-31 (KST). Launch date: 2026-10-30 - Pick: Lasm (source: Show HN) - Verified: ran - What: Lasm 은 Lean 4 프로그램을 브라우저와 Node 에서 실행할 수 있게 해 주는 프로덕트다. Lean 코드를 WebAssembly 로 컴파일한다. - What (en): Lasm is a product that lets Lean 4 programs run in the browser and on Node. It compiles Lean code to WebAssembly ahead of time. - Why: 오늘의 픽으로 선정한 이유는 웹 서버 코드의 규칙을 배포 전에 증명할 수 있게 하기 때문이다. 테스트와 달리 증명은 모든 요청에 대해 성립한다. - Why (en): It is today’s pick because it lets you prove a web server follows its rules before deploying it. Unlike tests, the proofs cover every request. - Verdict: 작동한다. Lean 으로 작성한 서버가 응답했고, 잘못된 정리를 넣자 빌드가 실패했다. - Verdict (en): It works. The server written in Lean answered, and a false theorem failed the build. - Tags: lean, formal-verification, webassembly, node, compiler, ai-built ## Checked against the README - [pass] Node 만 있으면 된다. Lasm 이 Lean 을 설치하므로 Lean 버전 관리 도구 elan 이 필요 없다(you only need Node, Lasm installs it, and you need no elan to build) — 환경 변수를 비우고 새 디렉토리에서 Node 24 만으로 템플릿 앱을 만들어 빌드하고 실행했다. Lean 과 elan 은 따로 설치하지 않았다 - [pass] 배포하는 코드의 성질을 증명할 수 있다(you can prove properties of the code you deploy) — App.lean 에 greet 함수에 대한 정리 두 개를 추가하자 빌드가 통과했다. greet "Ada" 의 결과에 Bob 이 들어간다는 잘못된 정리를 넣자 빌드가 실패했다. Tactic `decide` proved that the proposition … is false 라는 오류가 출력됐다 - [unknown] Hono 에 Lean 핸들러를 연결하면 서버의 처리량은 Node 기본 http 서버의 0.24배다(Lasm 서버 24,911 req/s, Node http 서버 103,134 req/s) — autocannon(연결 50개, 8초)으로 측정하자 Lasm 서버는 10,058 req/s, 직접 작성한 Node http 서버는 64,510 req/s 를 처리했다. Lasm 서버의 처리량은 Node http 서버의 0.16배다. 제작자는 서버와 부하 도구가 같은 컴퓨터의 서로 다른 코어를 쓰도록 지정해 측정했다. 오늘은 지정하지 않았다 ## Measured - Hono 템플릿의 첫 빌드 시간과 program.wasm 크기. 4코어 컴퓨터: 50초, 783 KB (time npm run build, ls -l dist/program.wasm) ## 한국어 ## 무엇이 문제인가 웹 앱의 테스트는 미리 지정한 입력에서만 코드의 결과를 확인한다. "글은 작성자만 고칠 수 있다" 같은 규칙이 모든 요청에서 지켜지는지는 테스트로 확인할 수 없다. 제작자는 README 에서 Lasm 의 성능을 Node 의 기본 http 서버와 비교했다. TypeScript 공식 핸드북에 따르면 TypeScript 의 타입 시스템은 컴파일할 때 안전한지 알 수 없는 연산도 허용한다. TypeScript 의 타입은 값의 형태를 확인할 뿐, 함수의 결과가 어떤 규칙을 지키는지는 표현하지 못한다. ## 어떻게 해결했나 Lasm 은 2026년 10월 30일 Hacker News 에 Show HN 글로 올라왔다. 사용자는 서버 코드를 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 기본 서버보다 크게 낮았다. 권한 규칙처럼 잘못되면 안 되는 서버 로직을 증명하고 싶은 경우에 써 볼 만하다. ### 용어 - Lean: 프로그래밍 언어이자 증명 보조기다. 함수와 함께 그 함수가 만족하는 성질을 정리로 작성하고 증명하면, Lean 이 컴파일할 때 증명이 타당한지 검사한다. - 서버리스: 서버를 직접 운영하지 않고, 요청이 올 때마다 클라우드가 함수를 실행해 주는 배포 방식이다. - 바인딩: 다른 언어로 작성한 함수를 호출할 수 있도록, 호출하는 언어에서 그 함수의 이름과 타입을 선언한 것이다. ## English ## The problem Web app tests check the code only on the inputs you choose. They cannot show that a rule such as "only the author can edit a post" holds for every request. In the README, the maker compares Lasm’s performance with Node’s plain http server. The official TypeScript handbook says the type system allows some operations that cannot be known to be safe at compile time. TypeScript types check the shape of values, but they cannot state rules about a function’s results. ## How it solves it Lasm was posted on Hacker News as a Show HN on October 30, 2026. You write the server code in Lean. In the same project, you state its rules as theorems and prove them. At build time Lean checks the proofs, and Lasm compiles the checked code to WebAssembly ahead of time. The output becomes a Node server, a serverless function or a browser app. The Lean compiler and build tools come in npm packages, so you only install Node. You call npm packages such as the web framework Hono from Lean by declaring a binding for each function. ## What is different The first difference is how the rules are checked. In Lasm, Lean checks proofs that the rules hold for every input. A wrong proof fails the build, so that code cannot be deployed. The README’s example, Conduit, is a blog app modeled on Medium. The maker says it proves 117 theorems, including one that says only the author can edit a post. But according to the README, the proofs do not cover whether each SQL statement matches the model of the tables used in the proofs. They also do not cover JSON parsing and printing, or concurrent requests. The proofs assume that Lean, Lasm and the JavaScript runtime are correct. The second difference is how the code runs. TypeScript compiles to JavaScript, which Node runs directly. Lasm compiles Lean to WebAssembly, so proven code runs inside a JavaScript runtime and can call npm packages. According to the README, Lean code on Node runs in WebAssembly threads and crosses a thread boundary each time it calls JavaScript. The tradeoff is lower throughput than a plain Node http server. The README also says to give each app at least 512 MB of memory. ## How it was built - The repository has 1,180 commits from September 17 to October 28, 2026. Of these, 605 have a Co-authored-by trailer for Claude. - The README points AI agents to separate guide files (llms.txt and docs/AI.md). - The numbers in the README’s performance table were measured on a free 4-CPU GitHub runner. The table names the CI run behind each number, so you can look up its log. ## Running it With Node 24, I followed the README’s commands to create the Hono template app, and built and ran it. 1. Install. `npm create @lasm@latest app -- --template hono` and `npm install` finished in 20 seconds. node_modules was 674 MB. 2. Build. The first `npm run build` took 50 seconds and left a 2.7 GB cache in `.cache/lasm` in the home folder. After I deleted dist, a rebuild took 1.6 seconds. program.wasm was 783 KB. 3. Run. It took 292 ms from starting the server process with `node dist/main.mjs` to its first response. /hello/Ada returned the Lean function’s greeting as JSON. POST /echo sent Korean text back in JSON without changing it. 4. Proof. I added two theorems about the greet function to App.lean, and the build passed in 9 seconds. One says `greet "Ada"` returns a fixed greeting, and the other says the greeting has the same format for every name. A false theorem that put Bob in place of Ada failed the build in 0.8 seconds. 5. Throughput. I ran autocannon with 50 connections for 8 seconds, and the server handled 10,058 requests per second. A plain Node http server I wrote handled 64,510 on the same machine. So Lasm had 0.16 times the throughput of the plain server. The README reports 0.24. The maker ran the server and the load generator on separate cores. Today the load generator ran on the server’s 4-core machine without assigned cores. I did not check whether this affects both servers equally. 6. Memory. Under load, the server used 358 MB, less than the 512 MB minimum the README gives. ``` App.lean:11:67: error: Tactic `decide` proved that the proposition [lasm] Build failed. Fix the error above and run the command again. ``` ## Not checked - The 117 theorems in Conduit. Run `npm run proofs` in the example folder and compare the theorems with the descriptions in PROOFS.md. - Other targets. Build the same app with `--target workers` and `--target bun`, and check that it answers on Cloudflare Workers and Bun. ## Verdict It works. The server written in Lean answered, and a false theorem failed the build. But its throughput was far below that of a plain Node server. It is worth trying if you want to prove server logic such as permission rules. ### Terms - Lean: A programming language and proof assistant. You write functions together with theorems about them, and the compiler checks the proofs. - serverless: A way to deploy code without running your own server. A cloud provider runs your function for each request. - binding: A declaration that links a function written in another language to a name and type in this language, so you can call it. ## Launches the same day - DOOMFORMER (Show HN, 121): 신경망 계산 실험. DOOM 맵 안에서 신경망을 계산하고, 값을 NumPy 결과와 하나씩 대조한다. - Arsaze (Show HN, 60): 영상 편집 앱. 탭 자동 완성과 에이전트 편집을 지원한다고 소개한다. - Lasm (Show HN, 34): Lean 4 컴파일러. Lean 으로 작성하고 증명한 웹 앱을 WebAssembly 로 빌드한다. - hyperbin (Show HN, 14): 파일 휴지통 도구. 지운 파일을 정리하는 기능을 할로윈에 맞춰 소개했다. - Fraktur (Show HN, 14): 브라우저 DJ 믹싱 앱. - unslop (GitHub, 941): Claude 스킬. AI 가 만든 티가 나는 화면을 디자인된 화면으로 바꾼다고 소개한다. - florilegium (GitHub, 405): LuaLaTeX 꽃무늬 여백. 페이지마다 Lua 로 꽃과 줄기를 새로 그린다. - pixelfx (GitHub, 246): 픽셀 아트 효과 232개. 효과마다 짧은 코드이고, 효과를 만드는 Claude Code 스킬을 함께 준다. - Vaani Developer Platform (Product Hunt, 253): 음성 AI 개발 플랫폼이라고 소개한다. - Knocket AI (Product Hunt, 239): 웹사이트 방문자 채팅 도구. - SpeakON Agent (Product Hunt, 237): 음성 명령 에이전트. 말로 한 요청을 작업으로 바꾼다고 소개한다. ## Getting started - Steps: npm create @lasm@latest app -- --template hono ; cd app && npm install && npm run dev - Needs: Node 24 이상(또는 Bun, Deno). Lean 과 빌드 도구는 npm 패키지에 들어 있다 - Cost: MIT, 무료. - Note: README 에 따르면 첫 빌드 뒤 홈 디렉토리의 캐시가 약 2.5 GB 를 차지한다. 오늘은 2.7 GB 였다.