웹앱 코드에 '증명서'를 붙인다면?
코드 리뷰를 아무리 꼼꼼히 해도, 테스트 커버리지를 90% 넘게 채워도 버그는 결국 어딘가에서 터지거든요. 테스트는 '우리가 미리 생각해 본 경우'만 확인해 주니까요. 그런데 만약 “이 함수는 어떤 입력이 들어와도 절대 음수 잔액을 만들지 않는다”는 사실을 컴파일러가 수학적으로 확인해 준다면 어떨까요?
이번에 공개된 Lasm은 바로 이런 발상에서 출발한 프로젝트예요. 정리 증명기(theorem prover)이면서 프로그래밍 언어이기도 한 Lean으로 웹앱을 작성하고, 그걸 Node.js, 서버리스, 엣지 런타임에서 돌릴 수 있게 해주는 도구라고 소개하고 있어요. 그러니까 '수학적으로 검증된 코드'를 연구실에서 꺼내서, 우리가 매일 배포하는 실제 웹 환경으로 가져와 보겠다는 시도예요.
형식 검증, 이게 뭐냐면
형식 검증(formal verification)은 코드가 어떤 성질을 만족한다는 걸 '증명'으로 보장하는 기법이에요. 테스트가 “입력 100개 넣어봤는데 다 괜찮았어요”라면, 형식 검증은 “가능한 모든 입력에서 괜찮다는 걸 논리적으로 증명했어요”에 가까워요. 비유하자면 테스트는 다리 위로 트럭 몇 대를 지나가게 해보는 거고, 형식 검증은 구조 계산으로 하중을 견딘다는 걸 증명하는 거예요.
Lean은 원래 수학자들이 정리를 증명할 때 많이 쓰는 언어인데, 일반 프로그램도 짤 수 있는 함수형 언어이기도 해요. 예를 들어 이런 식으로 '조건을 만족하는 값만 존재할 수 있는 타입'을 만들 수 있어요.
structure Age where
val : Nat
isValid : val ≤ 150
def myAge : Age := ⟨30, by decide⟩
Age를 만들려면 값과 함께 “이 값은 150 이하다”라는 증명을 같이 넘겨야 하고, 증명을 못 하면 컴파일 자체가 안 돼요. 그러니 런타임에 방어 코드를 여기저기 흩뿌릴 일이 줄어들어요. theorem rev_rev (xs : List Nat) : xs.reverse.reverse = xs := by simp처럼 함수의 성질 자체를 정리로 적어두고 증명할 수도 있고요.
왜 하필 Node, 서버리스, 엣지일까
Lean 4는 기본적으로 C 코드로 컴파일되는 구조라서, 지금까지는 네이티브 바이너리로 실행하는 게 일반적이었어요. 반면 요즘 웹 백엔드는 Node.js 서버, AWS Lambda 같은 서버리스 함수, Cloudflare Workers 같은 엣지 런타임처럼 자바스크립트 계열 실행 환경에서 돌아가는 경우가 많죠. 참고로 엣지 런타임은 사용자와 가까운 전 세계 서버에서 코드를 실행해 응답 속도를 줄이는 방식이에요. Lasm은 이 간극을 메워서 Lean으로 쓴 로직을 이런 환경에 배포할 수 있게 하겠다는 거예요. 아직 초기 프로젝트라서 구체적인 빌드 방식이나 지원 범위는 저장소 README를 직접 확인해 보시는 걸 추천해요.
여기서 꼭 짚고 넘어갈 개념이 신뢰 기반(TCB, Trusted Computing Base)이에요. 이게 뭐냐면 '검증은 안 됐지만 그냥 믿고 쓰는 부분'이에요. 비즈니스 로직을 Lean으로 증명해도 그 아래 있는 JS 런타임, HTTP 처리, DB 드라이버, 그리고 Lean 코드를 변환해 주는 도구 자체는 증명 범위 밖에 있어요. 또 증명은 '명세(spec)대로 동작한다'는 것만 보장하기 때문에, 명세가 틀렸다면 틀린 걸 완벽하게 구현한 셈이 돼요. 형식 검증이 만능은 아니라는 점은 꼭 기억해 두세요.
업계 흐름 속에서 보면
검증된 소프트웨어를 실무로 끌고 오려는 시도는 꾸준히 있었어요. F 언어로 만든 암호 라이브러리 HACL는 Firefox와 CPython의 해시 구현에 실제로 들어가 있고, AWS가 밀고 있는 Dafny는 JS, Go, Java, Python 등으로 컴파일돼요. 웹에 특화된 시도로는 MIT의 Ur/Web이 있었고, AWS는 권한 정책 언어 Cedar의 명세와 증명을 Lean으로 작성하기도 했어요.
요즘 Lean이 특히 뜨는 건 수학과 AI 덕분이에요. 테렌스 타오 같은 수학자들이 Lean으로 증명을 검증하고, 구글 딥마인드의 AlphaProof는 국제수학올림피아드 문제를 Lean으로 풀어냈죠. 여기에 AI가 코드를 대량으로 만들어 내면서 'AI가 짠 코드를 어떻게 믿을 거냐'는 질문이 커졌는데, 그 답으로 형식 검증이 다시 떠오르고 있어요. AI가 코드와 증명을 같이 쓰고 Lean이 그 증명을 기계적으로 검사하는 구조라면, 사람이 모든 줄을 리뷰하지 않아도 되니까요. Lasm은 이 흐름에서 Lean 생태계를 웹 백엔드까지 넓히는 퍼즐 조각이라고 볼 수 있어요.
한국 개발자에게 주는 시사점
솔직히 당장 회사 프로덕션을 Lean으로 갈아엎는 건 현실적이지 않아요. 초기 프로젝트인 데다 라이브러리, 레퍼런스, 채용 시장 모두 TypeScript나 Kotlin과는 비교가 안 되니까요. 대신 이렇게 접근해 보면 좋아요.
- 핵심 로직만 검증하기: 결제 금액 계산, 포인트 적립, 권한 체크처럼 틀리면 돈이나 보안 사고로 바로 이어지는 순수 함수만 Lean으로 쓰고 증명하는 그림을 그려볼 수 있어요.
- 금융·블록체인 분야라면 더 주목: 스마트 컨트랙트 감사나 핀테크처럼 한 번의 버그가 큰 손실로 이어지는 도메인에서는 형식 검증 경험이 차별화된 역량이 돼요.
- 사이드 프로젝트로 맛보기: 공식 문서인 'Functional Programming in Lean', 'Theorem Proving in Lean 4', 게임처럼 증명을 배우는 Natural Number Game으로 시작해 보세요. 타입으로 버그를 막는 사고방식은 TypeScript나 Rust를 쓸 때도 그대로 도움이 돼요.
마무리
한 줄 정리: Lasm은 '증명된 코드'를 연구실에서 꺼내 우리가 매일 배포하는 Node·서버리스·엣지 환경으로 옮겨 보려는 실험이에요.
여러분 서비스에서 '이것만큼은 절대 틀리면 안 된다' 싶은 로직은 뭔가요? 그 부분에 테스트 대신 증명을 붙일 수 있다면, 학습 비용을 감수할 의향이 있으신가요?
🔗 출처: Hacker News