버그가 '없다'는 걸 증명할 수 있는데, 왜 아무도 형식 기법을 안 쓸까

"테스트는 버그가 있다는 것은 보여줄 수 있지만, 없다는 것은 증명하지 못한다." 컴퓨터 과학자 다익스트라의 유명한 말인데요. 그렇다면 버그가 '없다는 것'을 수학적으로 증명하는 방법이 있다면 어떨까요? 실제로 그런 분야가 있어요. '형식 기법(formal methods)'이라고 하는데, 수십 년 역사에 확실한 성공 사례까지 있는데도 현업에서는 거의 쓰이지 않죠. 왜 그럴까요? 이 분야 전문가인 힐렐 웨인(Hillel Wayne)이 이 질문을 정면으로 파고든 글이 있어서 소개해요. 2019년 글이지만 지금 읽어도 통찰이 그대로 유효하거든요.

형식 기법이 뭐냐면

간단히 말해 소프트웨어가 '무엇을 해야 하는지'를 수학적으로 엄밀하게 적고(명세), 실제로 그걸 만족하는지 기계적으로 확인(검증)하는 방법이에요. 글에서는 이걸 크게 두 갈래로 나눠요.

첫째는 설계 검증이에요. 코드를 짜기 전에 시스템의 설계 자체를 TLA+나 Alloy 같은 명세 언어로 모델링하고, '모델 체커'라는 도구가 가능한 모든 실행 순서를 전부 탐색해서 문제를 찾아주는 방식이죠. 특히 분산 시스템처럼 여러 프로세스가 동시에 움직이는 시스템에서 위력적이에요. 사람 머리로는 "A 서버가 응답하기 직전에 B 서버가 죽고, 그 순간 재시도가 겹치면?" 같은 경우의 수를 다 따질 수 없는데, 도구는 기계적으로 전부 따져보거든요.

둘째는 코드 검증이에요. 코드 자체가 명세를 만족한다는 걸 Coq이나 Isabelle 같은 증명 도구로 수학적으로 증명하는 거예요. 운영체제 커널인 seL4, 검증된 C 컴파일러인 CompCert가 이 분야의 대표 사례죠.

그런데 왜 아무도 안 쓸까

글의 진단은 냉정해요. 우선 명세를 쓰는 것 자체가 어렵기 때문이에요. "내가 원하는 게 정확히 뭔지"를 모호함 없이 적는 건 생각보다 훨씬 어려운 기술이고, 우리 대부분은 그런 훈련을 받아본 적이 없어요. 요구사항을 애매하게 적으면 증명이 통과해도 아무 의미가 없고요.

코드 검증 쪽은 비용이 살인적이에요. seL4는 약 1만 줄짜리 커널을 검증하는 데 여러 해에 걸친 인년(person-year) 단위의 노력이 들었어요. 게다가 증명은 코드 변경에 아주 취약해서, 코드를 조금만 고쳐도 증명을 상당 부분 다시 해야 해요. 매주 배포하는 일반적인 서비스 개발 리듬과는 도저히 맞지 않죠. 그래서 저자의 결론은 명확해요. 코드 전체 증명은 항공, 커널, 암호 라이브러리처럼 버그 하나가 재앙인 극소수 영역에서만 합리적이라는 거예요.

하지만 반전이 있어요. 설계 검증은 이야기가 완전히 다르다는 거죠. 비용이 훨씬 싸고 효과는 즉각적이거든요. 실제로 AWS는 TLA+로 DynamoDB와 S3의 핵심 프로토콜을 모델링해서, 테스트로는 도저히 못 찾았을 심각한 설계 버그들을 출시 전에 잡아낸 경험을 논문으로 공개했어요. 재현하려면 수십 단계의 이벤트가 정확한 순서로 겹쳐야 하는 버그를 사람이 테스트로 찾아낼 수는 없잖아요.

지금 시점에서 다시 보면

이 글 이후의 흐름을 보면, 형식 기법의 아이디어가 다른 모습으로 업계에 스며들고 있어요. 러스트의 소유권 시스템이나 타입스크립트의 타입 시스템도 넓게 보면 '가벼운 형식 기법'이에요. 컴파일러가 특정 종류의 버그가 없음을 증명해주는 거니까요. 속성 기반 테스트(property-based testing)라는 것도 있는데, 구체적인 예시 대신 "어떤 입력에도 이 성질은 항상 성립해야 한다"를 적으면 도구가 무작위 입력을 퍼부어 반례를 찾아줘요. 테스트와 명세의 중간 다리 같은 존재죠. 그리고 AI가 코드를 짜주는 요즘, "무엇을 원하는지 정확하게 기술하는 능력"의 가치는 오히려 올라가고 있고요.

배워둘 가치가 있을까

결제, 재고, 예약처럼 동시성 버그가 곧바로 돈 문제로 이어지는 도메인을 다루신다면, TLA+는 진지하게 배워볼 가치가 있어요. 시스템 전체가 아니라 제일 아슬아슬한 프로토콜 하나만 모델링해도 효과를 봐요. 저자가 쓴 입문서 'Learn TLA+'가 무료로 공개되어 있고, AWS의 논문 'How Amazon Web Services Uses Formal Methods'도 훌륭한 출발점이에요.

한줄 정리: 코드를 증명하는 건 여전히 너무 비싸지만, 설계를 검증하는 건 이미 충분히 실용적이에요.

여러분은 어떠세요? "테스트만으로는 부족하다"고 느꼈던 순간이 있었나요? 동시성 버그 때문에 밤새워 본 경험이 있다면 들려주세요.