AI가 수학 증명을 대신 쓰는 시대 — Lean으로 검증된 zstd가 보여준 것

크롬의 TLS(웹 암호화 통신) 스택과 BoringSSL 라이브러리로 유명한 보안 엔지니어 아담 랭리(Adam Langley)가 자신의 블로그에 흥미로운 글을 올렸어요. 요지는 이래요. 'zstd 압축 해제기를 Lean이라는 정리 증명 도구로 형식 검증해봤는데, 이제는 증명 작업을 자동화할 수 있는 시대가 왔다.' 형식 검증이라는, 오랫동안 '이론적으로는 최고지만 비용 때문에 못 쓰는 기술'로 여겨지던 분야의 판이 바뀌고 있다는 신호거든요.

형식 검증이 뭐냐면

우리가 평소에 하는 테스트는 '몇 가지 입력을 넣어보고 결과가 맞는지 확인'하는 방식이에요. 아무리 테스트를 많이 짜도 모든 입력을 다 넣어볼 수는 없죠. 반면 형식 검증(formal verification)은 코드가 '모든 가능한 입력에 대해' 명세대로 동작한다는 걸 수학적으로 증명하는 기법이에요. 버그가 적을 것 같다, 가 아니라 특정 종류의 버그가 아예 없다는 걸 보장하는 거죠. Lean은 이런 증명을 작성하고 기계적으로 검사해주는 '정리 증명기(theorem prover)'인데요, 필즈상 수상자인 테렌스 타오 같은 수학자들이 실제 수학 연구에 쓸 만큼 검증된 도구예요.

왜 하필 zstd 압축 해제기일까

압축 해제기는 보안 관점에서 가장 위험한 코드 중 하나예요. 신뢰할 수 없는 외부 데이터를 받아서 해석(파싱)하는 코드거든요. 역사적으로 이미지 디코더, 압축 라이브러리, 폰트 파서 같은 곳에서 버퍼 오버플로우(할당된 메모리 범위를 벗어나 읽고 쓰는 버그) 취약점이 끊이지 않았어요. 공격자가 악의적으로 조작한 파일 하나로 원격 코드 실행까지 이어질 수 있는 영역이죠. zstd는 요즘 리눅스 커널부터 데이터베이스, 웹 서버까지 안 쓰이는 곳이 없는 압축 포맷이라, 이 해제기의 안전성이 수학적으로 증명되면 파급력이 상당해요.

핵심은 'AI의 환각이 문제가 안 되는 구조'

그동안 형식 검증이 안 퍼진 이유는 단순해요. 너무 비쌌거든요. 검증된 마이크로커널 seL4나 검증된 C 컴파일러 CompCert 같은 프로젝트는 박사급 인력이 수년씩 매달려야 했어요. 코드 한 줄에 증명 열 줄이 붙는 식이었으니까요.

그런데 여기에 LLM이 들어오면서 계산이 완전히 달라졌어요. 이 조합이 아름다운 이유가 있는데요. AI가 일반 코드를 짜주면 우리는 그 코드가 맞는지 결국 사람이 리뷰해야 하잖아요. AI는 그럴듯한 거짓말, 즉 환각을 하니까요. 그런데 형식 증명의 세계는 달라요. AI가 아무리 엉터리 증명을 내놔도 Lean의 증명 검사기가 기계적으로 걸러내거든요. 검사기를 통과한 증명은 누가 썼든, 어떻게 만들어졌든 옳다는 게 보장돼요. 즉 '만들기는 어렵지만 검증은 확실한' 분야라서, AI의 최대 약점인 신뢰성 문제가 구조적으로 사라지는 거예요. 사람은 명세(무엇을 증명할 것인가)만 제대로 쓰면 되고, 지루하고 방대한 증명 노동은 자동화에 맡기면 돼요.

업계 흐름 속에서 보면

이건 고립된 실험이 아니에요. 구글 딥마인드의 AlphaProof는 국제수학올림피아드 수준의 문제를 Lean으로 풀어냈고, AWS와 마이크로소프트는 이미 핵심 인프라 설계에 형식 기법을 적용해왔어요. 암호화 쪽에서는 HACL* 같은 검증된 구현이 파이어폭스에 들어가 있고요. 러스트(Rust)가 언어 차원에서 메모리 안전성을 보장하는 흐름이었다면, 형식 검증은 거기서 한발 더 나아가 '기능적 정확성', 그러니까 로직 자체가 맞다는 것까지 보장하는 다음 단계예요. AI가 증명 비용을 떨어뜨리면, 지금까지 seL4급 프로젝트에서만 가능했던 수준의 보증이 평범한 라이브러리에도 내려올 수 있어요.

우리에게 주는 시사점

당장 실무에 Lean을 도입할 일은 드물겠지만, 방향은 분명해요. 파서, 암호화, 직렬화처럼 보안이 걸린 코드부터 '검증된 구현'을 쓰는 게 표준이 되는 흐름이 올 수 있거든요. AI 코딩 도구를 쓰면서 '이 코드를 어떻게 믿지?'라는 고민을 해보셨다면, 그 답의 한 갈래가 여기 있어요. 신뢰는 사람의 리뷰가 아니라, 기계가 검사할 수 있는 증명에서 나올 수 있다는 것.

한줄 정리: AI가 형식 증명의 비용을 무너뜨리면서, '수학적으로 안전한 소프트웨어'가 소수 연구실의 전유물에서 벗어나기 시작했어요. 여러분이라면 어떤 코드가 가장 먼저 형식 검증되길 바라시나요?