테스트를 아무리 돌려도 못 잡는 버그가 있어요
분산 시스템을 만들다 보면 이상한 경험을 하게 돼요. 유닛 테스트도 다 통과하고 코드 리뷰도 꼼꼼히 했는데, 운영 환경에서 아주 가끔, 재현도 안 되는 버그가 터지는 거예요. 알고 보면 코드가 아니라 설계 자체에 구멍이 있었던 경우가 많거든요. 예를 들어 '노드 A가 락을 잡은 직후 네트워크가 끊기고, 그 사이 B가 타임아웃으로 락을 다시 잡으면?' 같은 시나리오는 사람이 머릿속으로 모든 경우를 따져보기가 거의 불가능해요. 이런 문제를 코드 작성 전에 잡아내는 도구가 정형 명세(formal specification)인데, 이걸 작성하기 위한 플랫폼인 SpecForge가 공개됐어요.
정형 명세가 뭐냐면
정형 명세가 뭐냐면, 시스템이 어떻게 동작해야 하는지를 수학적으로 애매함 없이 적어놓은 설계도예요. 일반 설계 문서와 결정적으로 다른 점은 기계가 검증할 수 있다는 거예요. '모델 체킹(model checking)'이라는 기법인데, 명세에 적힌 시스템이 도달할 수 있는 모든 상태를 컴퓨터가 하나도 빠짐없이 탐색하면서 '잔액이 마이너스가 되면 안 된다' 같은 규칙이 깨지는 경우가 있는지 전수 조사하는 거예요. 사람은 대표적인 시나리오 몇 개만 테스트하지만, 모델 체커는 요청이 겹치는 모든 순서, 장애가 나는 모든 타이밍을 다 따져보거든요.
이 분야의 대표 주자가 TLA+라는 언어인데, 아마존이 S3와 DynamoDB의 설계 검증에 써서 유명해졌어요. 사람 손으로는 도저히 못 찾을, 35단계의 이벤트가 특정 순서로 겹쳐야만 발생하는 데이터 손실 버그를 코드 한 줄 쓰기 전에 찾아냈다는 사례가 잘 알려져 있죠. 문제는 진입장벽이에요. TLA+는 수학 기호에 가까운 독특한 문법을 쓰는 데다 공식 도구도 투박해서, 배우다가 포기하는 사람이 많거든요. SpecForge는 바로 이 지점을 파고든 제품이에요. 명세를 '작성하는 경험' 자체를 다듬어서, 문서화된 투어를 따라가며 배우고, 명세를 쓰고, 검증하는 흐름을 하나의 플랫폼 안에서 해결하겠다는 접근이죠.
명세 작성에서 중요한 감각 하나를 짚자면, 시스템 전체를 옮겨 적는 게 아니라는 점이에요. 코드를 한 줄 한 줄 번역하는 게 아니라, 핵심 프로토콜(락 획득 규칙, 상태 전이, 메시지 순서 같은 것)만 추상화해서 적는 거예요. 그래서 잘 쓴 명세는 몇십 줄에서 몇백 줄 수준으로 짧고, 그 자체가 팀 최고의 설계 문서가 되기도 해요.
업계 맥락: 형식 기법의 조용한 르네상스
이 동네에는 플레이어가 꽤 있어요. 원조 격인 TLA+와 모델 체커 TLC, 관계 논리 기반의 Alloy, TLA+를 현대적인 개발자 친화 문법으로 다시 만든 Quint, 마이크로소프트가 Azure 서비스 검증에 쓰는 P 언어까지. Lean이나 Coq 같은 정리 증명기와는 결이 좀 다른데요, 정리 증명기는 사람이 수학적 증명을 직접 구성해야 하는 반면, 모델 체킹은 버튼을 누르면 기계가 알아서 전수 탐색해 주기 때문에 실무 진입장벽이 훨씬 낮아요. 최근 이 분야가 다시 주목받는 배경도 재미있어요. AI가 코드를 대신 짜주는 시대가 되면서, '무엇을 만들어야 하는가'를 정확하게 기술하는 능력, 즉 명세의 가치가 오히려 올라가고 있거든요.
한국 개발자에게 주는 시사점
결제, 재고 차감, 분산 락, 캐시 무효화처럼 동시성이 얽히는 설계를 하고 있다면 배워둘 가치가 충분해요. 전체 시스템을 명세할 필요 없이, 제일 위험한 프로토콜 하나만 골라서 하루 이틀 모델링해 봐도 '어, 이 순서로 오면 깨지네?' 하고 발견하는 경험을 할 수 있거든요. SpecForge처럼 작성 경험의 문턱을 낮춘 도구가 나오는 건 그 첫 시도를 훨씬 수월하게 만들어 준다는 점에서 반가운 일이고요.
정리하면, 정형 명세는 테스트가 못 잡는 설계 버그를 코드 작성 전에 잡는 기술이고, SpecForge는 그 작성 경험을 제품 수준으로 끌어올리려는 시도예요. 여러분의 시스템에서 '이건 머리로 다 못 따져보겠다' 싶은 동시성 설계가 있다면 어떤 부분인가요?
🔗 출처: Hacker News