수학으로 버그를 잡는다: 제인 스트리트의 형식 검증 이야기

버그를 '테스트'가 아니라 '증명'으로 잡는다면

우리가 보통 코드가 맞는지 확인하는 방법은 테스트죠. 입력 몇 개 넣어보고 결과가 맞으면 "오케이 통과". 그런데 이건 한계가 명확해요. 내가 생각해본 경우만 확인하는 거니까요. 테스트는 버그가 "있다"는 건 보여줘도, 버그가 "없다"는 건 절대 증명 못 해요. 금융권에서 OCaml로 유명한 퀀트 트레이딩 회사 제인 스트리트(Jane Street)가 자기들이 형식 검증(formal methods)을 어떻게 쓰는지 시리즈로 정리해 공개했는데, 이 주제를 처음 접하는 분들한테 좋은 입문서예요.

형식 검증이 뭐냐면

형식 검증은 쉽게 말해 "수학으로 프로그램이 옳다는 걸 증명하는 것"이에요. 테스트가 "몇 개 찍어보기"라면, 형식 검증은 "모든 경우에 대해 성립함을 논리적으로 보이기"예요.

비유하자면 이래요. 어떤 식 x + y = y + x가 모든 숫자에서 성립하는지 확인한다고 해봐요. 테스트 방식은 1+2, 3+5, 100+7... 계속 숫자를 넣어보는 거예요. 아무리 많이 넣어도 "전부 다"는 못 하죠. 반면 수학자는 한 번의 증명으로 "모든 x, y에 대해 성립"을 끝내버려요. 형식 검증이 코드에 대해 하려는 게 바로 이거예요.

어떻게 동작하냐면

대표적인 도구가 두 종류예요. 하나는 모델 검사(model checking)인데, TLA+ 같은 도구가 유명해요. 시스템이 가질 수 있는 상태들을 컴퓨터가 빠짐없이 탐색하면서 "절대 일어나면 안 되는 상황(예: 돈이 두 번 빠져나감, 교착 상태)"에 도달하는 경로가 있는지 싹 뒤져요. 사람이 상상 못 한 희한한 동시성 버그를 잡는 데 특히 강력해요.

다른 하나는 정리 증명(theorem proving)이에요. 코드의 성질을 수학 명제로 바꾼 다음, 증명기를 통해 한 단계씩 논리적으로 참임을 보이는 방식이죠. 제인 스트리트는 여기에 더해 타입 시스템도 적극 활용해요. 강한 타입 시스템 자체가 가벼운 형식 검증의 일종이거든요. "이 함수엔 양수만 들어올 수 있다"를 타입으로 박아두면, 컴파일 단계에서 잘못된 호출이 아예 막히니까요.

왜 하필 금융 회사가

여기서 "왜 트레이딩 회사가 이런 걸 하지?" 싶을 거예요. 이유는 단순해요. 돈이니까요. 거래 시스템에서 동시성 버그 하나가 터지면 몇 초 만에 수백만 달러가 날아갈 수 있어요. 그런 시스템은 "운영하면서 버그 잡자"가 통하지 않아요. 배포 전에 "이 시스템은 이런 나쁜 상태에 절대 안 빠진다"를 보장받아야 하죠. 그래서 비용이 많이 드는 형식 검증이 오히려 수지가 맞는 거예요.

업계 흐름에서 보면

형식 검증은 예전엔 항공·우주·반도체처럼 "실패하면 사람이 죽거나 칩을 리콜해야 하는" 극단적인 분야의 전유물이었어요. AWS도 분산 시스템 설계에 TLA+를 쓴다고 공개한 적 있고요. 최근 흐름은 이 무거운 기법을 일상 개발에 조금씩 녹여 쓰는 쪽이에요. 전체를 증명하진 않더라도, 가장 위험한 핵심 부분만 골라서 모델 검사를 돌리거나, Rust처럼 강한 타입과 소유권 시스템으로 한 부류의 버그를 컴파일 단계에서 통째로 없애버리는 식으로요.

한국 개발자에게

당장 내일부터 TLA+로 증명하라는 건 아니에요. 다만 두 가지는 지금도 써먹을 수 있어요. 첫째, 정말 중요한 동시성·상태 머신 로직(결제, 재고 차감, 분산 락 같은 곳)은 코드를 짜기 전에 상태와 불변식을 종이에 적어보는 것만으로도 버그가 확 줄어요. 둘째, 타입 시스템을 "귀찮은 검사"가 아니라 "공짜로 받는 작은 증명"으로 보기 시작하면 코드 설계가 달라져요. 불가능한 상태를 아예 표현 못 하게 타입을 짜는 거죠.

한 줄 정리

테스트는 버그의 존재를 보여주고, 형식 검증은 버그의 부재를 증명해요. 전부에 쓸 순 없어도, 진짜 무너지면 안 되는 곳엔 한 번쯤 꺼내볼 무기예요.

여러분은 "여기 버그 나면 진짜 끝장난다" 싶은 코드를 어떻게 검증하고 계세요? 테스트 말고 다른 안전장치를 써본 경험이 있으면 들려주세요.