정형 검증, 당신이 아는 게 전부가 아닙니다 — 수학으로 버그를 '증명'하는 세계

테스트로는 절대 알 수 없는 것

"우리 코드에 버그 없다고 100% 확신하세요?" 이렇게 물으면 대부분 "테스트 다 통과했어요"라고 답하거든요. 그런데 컴퓨터 과학의 전설 다익스트라가 이런 말을 남겼어요. "테스트는 버그가 있다는 건 보여줘도, 버그가 없다는 건 절대 증명 못 한다." 무슨 뜻이냐면, 테스트를 1000개 돌려서 전부 초록불이 떠도, 우리가 미처 생각 못 한 1001번째 입력에서 시스템이 터질 수 있다는 거예요. 테스트는 결국 '우리가 떠올린 시나리오'만 확인하니까요.

정형 검증(Formal Verification)은 바로 이 한계를 정면으로 돌파하려는 분야예요. 이게 뭐냐면, 프로그램이 정해진 명세(원하는 동작 규칙)를 '모든 경우에' 만족한다는 걸 수학적으로 증명해버리는 기술이거든요. 한두 개 케이스를 돌려보는 게 아니라, 수학 정리를 증명하듯 "이 코드는 어떤 입력이 와도 이 규칙을 절대 안 어긴다"를 논리로 못 박는 거죠.

그래서 어떻게 모든 경우를 확인하나요?

크게 세 갈래 방법이 있어요.

첫째, 모델 체킹(Model Checking)이에요. 시스템이 가질 수 있는 모든 상태를 자동으로 쫙 탐색하면서 "여기서 데드락 걸리는 경로 있나? 이 조건이 깨지는 순간이 있나?"를 기계가 전수조사하는 방식이에요. 상태가 너무 많아 폭발하는 게 약점이지만, 영리한 압축 기법으로 다뤄요.

둘째, 정리 증명(Theorem Proving)이에요. Coq, Isabelle, Lean 같은 도구로 사람이 증명의 큰 그림을 잡아주면, 컴퓨터가 한 줄 한 줄 논리적 허점이 없는지 깐깐하게 검사해줘요. 수학 교수님이 채점하듯이요.

셋째, SMT 솔버예요. Z3가 대표적인데, "이 조건들을 동시에 만족시키면서 버그를 일으키는 입력이 존재하나?"라는 질문을 자동으로 풀어줘요. 답이 '없음'이면 그 부분은 안전하다는 뜻이죠.

가장 흔한 오해

이 글 제목처럼, 정형 검증엔 사람들이 흔히 착각하는 지점이 많아요. 제일 큰 오해는 "증명만 끝나면 버그가 0이다"인데요, 사실 그렇지 않아요. 정형 검증이 보장하는 건 "코드가 명세를 만족한다"는 거지, "명세 자체가 옳다"는 게 아니거든요. 명세를 잘못 적으면, 그 잘못된 명세를 완벽하게 지키는 프로그램이 나와버려요. 그래서 정형 검증은 만능 보증서가 아니라 아주 강력한 '도구'로 봐야 해요.

실제로 어디에 쓰일까

"그거 학교에서나 쓰는 거 아니냐" 싶지만, 현장에서 꽤 씁니다. 대표적인 게 seL4 운영체제 커널인데, 코드 전체가 명세대로 동작한다는 걸 수학적으로 증명한 범용 OS 커널이에요. CompCert는 검증된 C 컴파일러로 "컴파일 과정에서 코드의 의미가 바뀌지 않는다"를 증명했고요. AWS는 분산 시스템 설계에 TLA+라는 명세 언어를 오래 써왔고, 최근엔 Dafny로 코드 수준 검증까지 넓히고 있어요. 인텔은 1994년 펜티엄 나눗셈 버그로 큰돈을 날린 뒤 하드웨어 검증에 정형 기법을 본격 도입했죠.

한국 개발자에게

모든 코드를 증명할 필요는 없어요. 비용이 크거든요. 하지만 결제 로직, 동시성 제어, 분산 합의처럼 '한 번 틀리면 치명적인' 핵심 부분은 TLA+로 설계를 먼저 검증해보는 것만으로도 가치가 커요. 머릿속으로만 그리던 동시성 시나리오의 반례를 기계가 대신 찾아주거든요. 게다가 요즘은 AI가 코드를 쏟아내는 시대라, "이 코드가 정말 맞나"를 기계적으로 검증하는 능력이 오히려 더 중요해지고 있어요.

마무리

정리하면, 정형 검증은 테스트로 못 잡는 버그를 수학으로 잡는 강력한 무기지만, 명세를 잘 써야 빛을 발하는 도구예요. 여러분 프로젝트에서 "여기는 절대 틀리면 안 되는데" 싶은 부분, 어디인가요? 그곳을 TLA+로 한번 모델링해본다면 어떤 숨은 버그가 튀어나올까요?