16년 묵은 SQLite 버그를 잡아낸 건 AI가 아니라 '수학'이었습니다

여러분 지금 이 글을 읽고 있는 기기 안에도 거의 확실히 들어 있는 소프트웨어가 하나 있습니다. 바로 SQLite인데요. 스마트폰, 브라우저, 항공기 시스템까지 전 세계에 1조 개 이상 배포된, 지구상에서 가장 많이 깔린 데이터베이스입니다. 그런데 이 검증되고 또 검증된 소프트웨어에서, 무려 16년 동안 아무도 눈치채지 못한 버그가 발견됐습니다. 더 흥미로운 건 그걸 찾아낸 방법입니다. 최신 AI 코딩 도구가 아니라, 1990년대에 나온 수학적 형식 검증 기법이었거든요.

16년을 숨어 있던 버그, 대체 뭐였나

문제의 무대는 SQLite의 WAL(Write-Ahead Logging) 모드입니다. WAL은 쉽게 말해 데이터베이스에 변경을 바로 반영하지 않고, 별도의 로그 파일에 먼저 적어두는 방식인데요. 성능을 크게 올려주는 대신 로직이 상당히 까다롭습니다. 여러 프로세스가 동시에 읽고 쓰는 상황에서 데이터 일관성을 지켜야 하기 때문이죠.

이번에 드러난 버그는 이 WAL의 체크포인트 과정과 관련된 경계 조건이었습니다. 특정한 타이밍에 특정한 순서로 동작이 겹칠 때만 나타나는, 이른바 희귀 경합 상황이었는데요. 평소에는 거의 발생하지 않지만, 한번 터지면 데이터가 조용히 어긋날 수 있는 종류의 문제입니다. 눈에 잘 안 띄면서도 치명적인, 가장 무서운 유형이죠.

핵심은 이겁니다. 수억 명이 쓰고, 테스트 커버리지가 100퍼센트에 가깝기로 유명한 SQLite에서조차, 사람의 눈과 일반적인 테스트로는 16년간 못 잡았다는 점입니다.

결정타는 dqlite와 TLA+였습니다

이 버그가 수면 위로 올라온 배경에는 dqlite라는 프로젝트가 있습니다. dqlite는 SQLite를 분산 환경에서 쓸 수 있게 만든 확장판인데요. 여러 서버에 걸쳐 데이터를 복제하다 보니, 원본 SQLite의 WAL 동작을 아주 정밀하게 이해하고 모델링해야 했습니다.

이 과정에서 개발자들이 꺼내 든 도구가 TLA+였습니다. TLA+는 코드를 실행해보는 게 아니라, 시스템이 가질 수 있는 모든 상태를 수학적으로 정의하고 검증하는 형식 명세 언어입니다. 튜링상 수상자인 레슬리 램포트가 만든 것으로 유명하죠. 아마존이 대규모 분산 시스템을 설계할 때 쓰는 것으로도 잘 알려져 있습니다.

일반적인 테스트가 “이 입력을 넣으면 이 결과가 나오나?“를 확인하는 거라면, TLA+는 “이 시스템이 도달할 수 있는 모든 경우의 수 중에 잘못된 상태가 하나라도 있나?“를 따집니다. 사람이 상상하지 못한 타이밍 조합까지 기계가 전부 훑어보는 셈인데요. 바로 이 전수조사 방식이, 16년간 테스트의 그물망을 빠져나갔던 경합 상황을 붙잡아낸 겁니다.

왜 하필 지금, 이 소식이 화제일까

솔직히 형식 검증은 새로운 기술이 아닙니다. 오히려 학계에서는 오래된 축에 속하죠. 그런데 이 이야기가 지금 유독 주목받는 데는 시대적 맥락이 있습니다.

지금은 AI가 코드를 폭포수처럼 쏟아내는 시대입니다. 개발자 한 명이 하루에 생성하고 검토하는 코드 양이 몇 년 전과는 비교가 안 되는데요. 문제는 양이 늘수록 사람이 검증할 수 있는 비율은 오히려 떨어진다는 점입니다. AI가 짠 그럴듯한 코드가 미묘한 경계 조건에서 조용히 어긋난다면, 그걸 누가 어떻게 잡아낼까요.

바로 여기서 형식 검증이 다시 소환됩니다. “많이 만드는 것"의 반대편에서 “확실하게 옳은지 증명하는 것"의 가치가 상대적으로 올라가는 거죠. 코드를 열 배 빠르게 생성할 수 있게 됐다면, 그 코드가 맞다는 걸 보장하는 수단도 그만큼 중요해집니다. SQLite 사례는 그 논점을 완벽하게 보여주는 상징적인 사건이 된 셈입니다.

그렇다고 만능은 아닙니다

물론 냉정하게 짚을 부분도 있습니다. 참고로 이번 주제는 최근 30일 커뮤니티 논의가 많지 않아, 기술의 본질과 맥락 위주로 정리한 점을 미리 밝혀둡니다.

TLA+ 같은 형식 검증은 진입 장벽이 상당히 높습니다. 시스템을 수학적 명세로 옮기는 작업 자체가 별도의 전문성을 요구하는데요. 아무 프로젝트에나 붙일 수 있는 도구가 아닙니다. 게다가 검증하는 건 “명세대로 짰는가"이지, “명세 자체가 옳은가"는 또 다른 문제입니다. 모델과 실제 코드 사이의 간극도 늘 존재하고요.

그래서 현실적인 그림은 이렇습니다. 형식 검증이 모든 테스트를 대체하는 게 아니라, WAL처럼 동시성이 얽힌 핵심 로직에 선택적으로 투입되는 정밀 무기에 가깝습니다. 비싸고 어렵지만, 한번 제대로 쓰면 사람이 16년간 못 본 걸 찾아주는 도구인 거죠.

마무리하며

이번 사건이 던지는 메시지는 분명합니다. 코드를 빠르게 만드는 능력과, 그 코드가 옳음을 증명하는 능력은 전혀 다른 문제라는 것입니다. AI가 생산성의 축을 앞으로 밀어붙일수록, 검증의 축을 붙잡아줄 오래된 수학의 가치는 역설적으로 더 빛나는데요.

여러분의 팀은 지금 코드를 “얼마나 빨리 만드느냐"에 자원을 쓰고 있나요, 아니면 “얼마나 확실히 맞는지"에도 투자하고 있나요. 이 균형을 어떻게 잡느냐가, 앞으로 소프트웨어 품질을 가르는 진짜 분기점이 될지도 모르겠습니다.