Hacker News 2026.04.14 25

Lean으로 '증명 완료'된 프로그램에서 버그가 나왔다 — 형식 검증의 함정

수학적으로 증명했는데 버그라니?

"형식 검증(formal verification)으로 프로그램이 올바르다고 증명했습니다" — 이 말을 들으면 뭔가 완벽하고 철벽 같은 느낌이 들잖아요. 수학적 증명이니까 틀릴 수가 없을 것 같고요. 그런데 한 개발자가 Lean이라는 정리 증명기(theorem prover)로 정확성이 증명된 프로그램에서 실제로 버그를 발견한 경험을 공유했어요. 이게 어떻게 가능한 걸까요?

이 이야기가 흥미로운 건, 형식 검증이 쓸모없다는 얘기가 아니라, 형식 검증을 제대로 활용하려면 "무엇을 증명하고 있는지"를 정확히 이해해야 한다는 교훈을 주기 때문이에요.

Lean이 뭔데요?

먼저 배경 설명을 좀 할게요. Lean은 마이크로소프트 리서치에서 만든 프로그래밍 언어이자 정리 증명 도구예요. 이게 뭐냐면, 쉽게 말해서 "이 프로그램이 특정 조건을 항상 만족한다"는 걸 수학적으로 증명할 수 있게 해주는 도구예요.

보통 우리가 프로그램이 맞는지 확인하려면 테스트를 짜잖아요. 근데 테스트는 내가 생각한 케이스만 확인하는 거라, 테스트에 없는 엣지 케이스에서 버그가 터질 수 있어요. 형식 검증은 이걸 수학적으로 "모든 가능한 입력에 대해" 프로그램이 올바르다는 걸 증명하는 거예요. 마치 수학 시간에 "모든 자연수 n에 대해 이 공식이 성립함을 증명하시오"라고 하는 것과 비슷한 거죠.

Lean 외에도 Coq, Isabelle, Agda 같은 도구들이 있는데, 최근에는 Lean 4가 실용성과 사용성 면에서 주목받으면서 수학계와 프로그래밍 커뮤니티 양쪽에서 인기를 얻고 있어요.

그래서 버그는 어디서 나온 건가

핵심은 이거예요: 증명은 명세(specification)에 대해 이루어지는데, 그 명세 자체가 틀릴 수 있다는 거예요.

비유를 하나 들어볼게요. 건축가가 "이 건물은 설계도면대로 완벽하게 지어졌습니다"라고 수학적으로 증명했다고 해요. 근데 설계도면 자체에 화장실 문이 안쪽으로 열리게 되어있어서 사람이 갇히는 문제가 있다면? 건물은 설계도대로 완벽하지만, 실제 사용에서는 버그(?)가 있는 거죠. 형식 검증도 마찬가지예요.

이 글의 저자는 Lean으로 프로그램의 특정 속성을 증명했는데, 문제는 그 속성이 프로그램이 "올바르게 동작한다"는 것의 전부를 담아내지 못했던 거예요. 증명한 속성 자체는 맞았지만, 실제 의도한 동작과 명세 사이에 간극(gap)이 있었던 거죠. 다시 말해, "올바르다"의 정의를 잘못 내렸거나 불완전하게 내린 거예요.

이건 형식 검증에서 꽤 잘 알려진 문제이긴 해요. 학계에서는 이걸 "specification gap" 또는 "specification bug"라고 부르는데, 도구가 아무리 완벽해도 사람이 명세를 쓰는 이상 이 간극은 항상 존재할 수 있어요.

형식 검증의 현재 위치

형식 검증은 지금까지 주로 안전이 극도로 중요한 분야에서 쓰여왔어요. 항공기 소프트웨어, 의료기기, 암호화 프로토콜 같은 곳에서요. 최근에는 블록체인 스마트 컨트랙트 쪽에서도 관심이 높아지고 있는데, 스마트 컨트랙트는 한번 배포하면 수정이 어렵고 돈이 직접 걸려있으니까요.

AWS에서도 TLA+라는 형식 명세 도구를 사용해서 분산 시스템의 설계를 검증하고 있고, seL4 마이크로커널은 전체 구현이 형식적으로 검증된 운영체제 커널로 유명해요. CompCert는 형식 검증된 C 컴파일러고요.

하지만 일반적인 소프트웨어 개발에서는 아직 진입 장벽이 높아요. 증명을 작성하는 것 자체가 프로그램을 작성하는 것만큼, 때로는 그 이상으로 어렵거든요. 그래서 현실에서는 완전한 형식 검증보다는, 타입 시스템을 활용한 부분적인 검증(Rust의 소유권 시스템이 대표적이죠)이 더 실용적인 접근법으로 자리 잡고 있어요.

한국 개발자에게 주는 시사점

이 글에서 가져갈 핵심 교훈은 두 가지예요.

첫째, "증명됨 = 버그 없음"이 아니에요. 형식 검증은 강력한 도구이지만, 결국 "무엇이 올바른 것인지"를 사람이 정의해야 하고, 그 정의가 틀릴 수 있어요. 이건 테스트에서도 마찬가지인데요, 테스트가 통과한다고 버그가 없는 게 아니라 "내가 확인한 범위에서는 맞다"는 거잖아요. 형식 검증도 "내가 정의한 명세에 대해서는 맞다"는 것이지, 명세를 넘어서는 보장은 해주지 않아요.

둘째, 형식 검증에 직접 뛰어들지 않더라도 이 사고방식은 일상 개발에 적용할 수 있어요. "이 함수가 올바르게 동작한다"를 정의할 때, 정말 모든 경우를 고려했는지 한 번 더 생각해보는 거예요. 특히 타입 시스템을 적극적으로 활용해서 "잘못된 상태가 아예 표현 불가능하게" 만드는 접근법은 TypeScript나 Kotlin 같은 언어에서도 바로 실천할 수 있어요.