수학이 '버그 없음'을 보증했는데, 버그가 나왔습니다

“이 프로그램은 수학적으로 증명되었습니다. 버그가 없습니다.”

이 문장을 들으면 안심이 되시나요? 그런데 현실에서는 형식 검증(formal verification)을 통과한 프로그램에서도 버그가 발견됩니다. 수학이 틀린 걸까요? 아닙니다. 우리가 수학에게 잘못된 질문을 한 겁니다.

형식 검증이란 무엇인가

먼저 용어부터 정리하겠습니다. 형식 검증은 프로그램이 특정 명세(specification)를 만족하는지 수학적으로 증명하는 기법입니다. 테스트가 “이 입력에서는 잘 동작한다"를 확인하는 거라면, 형식 검증은 “모든 가능한 입력에서 이 성질이 성립한다"를 보장합니다.

Lean은 이 분야에서 가장 주목받는 정리 증명기(theorem prover) 중 하나입니다. 원래 수학 증명을 기계적으로 검증하기 위해 만들어졌지만, Lean 4부터는 범용 프로그래밍 언어로도 사용할 수 있게 되면서 소프트웨어 검증 도구로서의 가능성이 크게 확장되었습니다. 구글, 마이크로소프트, 아마존 같은 빅테크들도 형식 검증을 일부 핵심 시스템에 도입하고 있고요.

그러니까 이론적으로는 완벽한 셈입니다. 그런데 왜 버그가 나올까요?

증명이 보증하는 것과 보증하지 않는 것

핵심은 이겁니다. 형식 검증이 증명하는 건 “코드가 명세를 만족한다”는 것이지, “프로그램에 버그가 없다”는 게 아닙니다.

이 차이가 미묘해 보이지만 실제로는 거대합니다.

예를 들어 보겠습니다. 정렬 알고리즘을 검증한다고 합시다. “출력 리스트는 오름차순이다"라고만 명세를 작성하면 어떻게 될까요? 입력을 전부 무시하고 빈 리스트를 반환하는 프로그램도 이 명세를 만족합니다. 수학적으로 완벽하게요. 명세에 “입력의 모든 원소가 출력에 포함되어야 한다"는 조건을 빠뜨렸기 때문입니다.

이것이 바로 명세 오류(specification bug)의 문제입니다. 현실 세계의 요구사항을 수학적 명세로 번역하는 과정에서 빠지거나 잘못 표현되는 것들이 생깁니다. 수학은 우리가 물어본 질문에만 정확히 답할 뿐, 우리가 물어보지 않은 질문까지 챙겨주지 않습니다.

증명과 현실 사이의 간극

명세가 완벽하다고 가정해도 문제는 남습니다. 형식 검증에는 신뢰 기반(Trusted Computing Base, TCB)이라는 개념이 있습니다. 증명 자체가 의존하는, 하지만 증명 범위 밖에 있는 것들을 뜻합니다.

구체적으로 짚어 보면 이렇습니다.

첫째, 컴파일러입니다. Lean으로 작성하고 검증한 코드도 결국 기계어로 컴파일되어야 실행됩니다. 이 컴파일 과정에서 버그가 유입될 수 있습니다. 검증된 C 컴파일러인 CompCert조차 검증 범위 밖의 코드에서 버그가 발견된 적이 있습니다.

둘째, 운영체제와 하드웨어입니다. 형식 검증된 마이크로커널 seL4는 C 코드 수준에서는 수학적으로 검증되었지만, 그 아래의 어셈블리 코드나 하드웨어 동작은 증명 범위에 포함되지 않습니다. 메모리 컨트롤러의 미묘한 타이밍 문제? 증명은 이런 걸 모릅니다.

셋째, 정리 증명기 자체의 건전성(soundness)입니다. Lean 4의 타입 체커에서도 건전성 관련 이슈가 보고된 바 있습니다. 증명을 검증하는 도구 자체에 결함이 있다면, 증명의 신뢰성은 근본부터 흔들립니다. “이 자물쇠는 절대 열리지 않습니다"라고 보증한 자물쇠 제조사의 보증서 자체가 위조일 수 있는 셈이죠.

AI가 코드를 작성하는 시대, 형식 검증의 역설

여기서 이야기가 AI와 만납니다.

요즘 AI 코딩 어시스턴트가 생성하는 코드의 양이 폭발적으로 늘고 있습니다. 자연스럽게 “AI가 만든 코드를 형식 검증으로 검증하면 되지 않나?“라는 아이디어가 나옵니다. 실제로 AI와 형식 검증을 결합하려는 연구가 활발합니다. AI가 코드를 쓰고, 다른 AI가 Lean 증명을 생성하고, 정리 증명기가 이를 기계적으로 검증하는 파이프라인을 구상하는 것이죠.

문제는 이 파이프라인에서 가장 취약한 고리가 여전히 명세 작성이라는 점입니다. AI가 아무리 정교한 증명을 생성해도, “무엇을 증명해야 하는가"를 결정하는 건 결국 사람의 몫입니다. 그런데 AI가 만든 코드는 사람이 처음부터 설계한 코드보다 의도를 파악하기 어려운 경우가 많습니다. 내가 완전히 이해하지 못하는 코드에 대해 완전한 명세를 작성하는 건 거의 불가능에 가깝습니다.

더 우려스러운 시나리오도 있습니다. 형식 검증이 주는 거짓 안도감입니다. “수학적으로 증명되었으니 안전하다"는 레이블이 붙으면, 코드 리뷰나 통합 테스트 같은 다른 안전장치들이 느슨해질 수 있습니다. 형식 검증을 만병통치약으로 오해하는 순간, 오히려 전체 시스템의 안전성이 떨어지는 역설이 발생합니다.

그렇다면 형식 검증은 쓸모없는 것인가

전혀 아닙니다. 형식 검증은 여전히 소프트웨어 품질 보증에서 가장 강력한 도구 중 하나입니다. 핵심은 이 도구가 무엇을 할 수 있고 무엇을 할 수 없는지 정확히 이해하는 것입니다.

형식 검증은 특정 종류의 버그를 원천 차단하는 데 탁월합니다. 버퍼 오버플로, 정수 오버플로, 특정 논리 오류 같은 것들이요. 하지만 명세의 완전성, 외부 환경과의 상호작용, 시스템 전체의 정합성까지 보장하지는 못합니다. 형식 검증은 울타리입니다. 아주 튼튼한 울타리지만, 울타리가 쳐지지 않은 방향에서 들어오는 문제까지 막아주지는 않습니다.

건강한 접근법은 형식 검증을 단독으로 쓰는 게 아니라 기존의 테스트, 코드 리뷰, 정적 분석과 함께 계층적 방어(defense in depth)의 한 층으로 활용하는 것입니다.

수학은 거짓말을 하지 않습니다. 하지만 수학이 대답할 수 있는 건 우리가 던진 질문뿐입니다. “이 프로그램이 정확한가"라는 질문 자체를 제대로 공식화하는 것이 형식 검증보다 어려운 문제일 수 있습니다. AI가 점점 더 많은 코드를 작성하는 시대, 우리에게 진짜 필요한 건 더 강력한 증명기가 아니라 더 정확한 질문을 던지는 능력이 아닐까요?