버그를 '안 나길 기도'하는 대신 '수학으로 증명'한다 — Jane Street의 형식 검증 이야기

코드가 맞다는 걸 어떻게 '증명'할까

우리가 코드를 짜고 나서 '이거 맞나?' 확인하는 방법은 보통 테스트죠. 입력 몇 개 넣어보고 원하는 결과가 나오면 'OK 통과!' 하고 넘어가요. 그런데 생각해보면 이건 좀 불안한 방식이에요. 테스트는 '내가 넣어본 경우엔 잘 돌더라'를 보여줄 뿐, '모든 경우에 잘 돈다'를 보장하진 못하거든요. 다익스트라라는 유명한 컴퓨터 과학자가 이런 말을 했어요. '테스트는 버그가 있다는 건 보여줄 수 있어도, 버그가 없다는 건 절대 증명하지 못한다.'

그래서 등장한 게 형식 검증(Formal Methods, 형식 기법)이에요. 월스트리트의 퀀트 트레이딩 회사인 Jane Street가 자기들이 이 기술을 실무에 어떻게 쓰는지 정리한 글을 공개했는데, 이 회사가 왜 여기에 진심인지부터 알면 이해가 쉬워요.

1초에 수십억이 오가는 곳의 고민

Jane Street는 초고속으로 주식을 사고파는 회사예요. 코드에 버그가 하나 있으면 몇 초 만에 수백만 달러가 날아갈 수 있는 환경이죠. 실제로 과거 Knight Capital이라는 회사는 배포 사고 하나로 45분 만에 4억 4천만 달러를 잃고 사실상 무너졌어요. 이런 동네에서는 '테스트 돌려보고 괜찮으면 배포'라는 일반적인 방식이 너무 위험한 거예요.

그래서 이들이 택한 길이 형식 검증이에요. 이게 뭐냐면, 코드가 하는 일을 수학적인 명제로 바꿔서, 논리적으로 '이 코드는 어떤 입력이 들어와도 절대 이런 잘못된 상태가 안 된다'를 증명하는 거예요. 마치 수학 시간에 '삼각형 내각의 합은 항상 180도'임을 한번 증명하면 세상 모든 삼각형의 각도를 일일이 재볼 필요가 없는 것처럼요.

전부 다 증명하는 건 아니에요 — 스펙트럼이 있어요

여기서 오해하기 쉬운 게 있어요. 형식 검증이라고 하면 '모든 코드를 수학으로 증명한다'고 생각하기 쉬운데, 현실은 비용 대비 효과에 따라 단계가 나뉘어요.

가장 가벼운 단계는 속성 기반 테스트(Property-based testing)예요. 보통 테스트가 '2 더하기 3은 5다' 같은 구체적 예시를 확인한다면, 속성 기반 테스트는 '어떤 숫자 a, b를 넣어도 a+b는 b+a와 같아야 한다' 같은 성질을 정하고, 컴퓨터가 무작위로 수천 개의 입력을 자동 생성해서 그 성질이 깨지는지 두들겨보는 방식이에요.

그 위 단계로는 TLA+ 같은 모델 검사 도구가 있어요. 동시성(여러 작업이 동시에 돌아갈 때) 문제처럼 사람 머리로는 모든 경우의 수를 따지기 불가능한 영역에서, 시스템이 가질 수 있는 모든 상태를 컴퓨터가 샅샅이 뒤져서 '절대 일어나면 안 되는 상황'이 생기는지 확인해줘요.

가장 무거운 단계가 정리 증명기(Coq, Lean 같은 도구)를 이용한 완전한 증명이에요. 비용이 크지만, 정말 절대 틀리면 안 되는 핵심 알고리즘에만 집중적으로 적용하는 식이죠.

업계 흐름에서 보면

형식 검증은 사실 학계에선 수십 년 된 분야인데, 최근 몇 년 사이 산업계로 빠르게 넘어오고 있어요. AWS는 클라우드 권한 시스템(IAM)과 S3의 핵심 로직을 TLA+와 자동 추론으로 검증하는 걸로 유명하고, 마이크로소프트는 윈도우 드라이버 검증 도구를 오래전부터 써왔어요. 항공·우주·자동차처럼 사람 목숨이 걸린 분야에선 이미 필수죠. Jane Street의 글이 의미 있는 건, '금융 IT 회사가 일상적인 개발 워크플로에 형식 검증을 현실적으로 녹여넣는 방법'을 보여준다는 점이에요. 거창한 이론이 아니라 매일 짜는 코드 옆에 둔다는 거죠.

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

'우리 회사는 트레이딩도 안 하는데 이게 무슨 상관?' 싶을 수 있어요. 하지만 가장 가벼운 단계인 속성 기반 테스트는 지금 당장 써먹을 수 있어요. 결제 모듈, 정산 로직, 권한 체크처럼 '절대 틀리면 안 되는' 부분에 적용하면 단위 테스트로는 놓치던 엣지 케이스를 잡아낼 수 있거든요. 파이썬엔 Hypothesis, 자바스크립트엔 fast-check 같은 라이브러리가 잘 나와 있어요. 동시성 버그로 고생하는 분이라면 TLA+를 한번 공부해두는 것도 큰 자산이 돼요.

마무리

핵심은 이거예요. 테스트가 '버그를 찾는' 활동이라면, 형식 검증은 '버그가 없음을 보장하는' 활동이라는 것. 전부에 적용할 순 없어도, 우리 코드 중 가장 중요한 1%에 적용하면 밤잠이 편해지죠. 여러분 코드베이스에서 '여기만큼은 절대 틀리면 안 된다' 싶은 부분은 어디인가요?