좋은 아침이에요! 오늘은 형식 검증이에요. 새 기술이 아니라 50년 넘은 기술인데, LLM 덕분에 다시 무대 위로 올라왔어요.
뭔가요? 테스트처럼 “몇 가지 입력을 넣어 보니 괜찮더라”가 아니라, 코드가 어떤 성질(예: 절대 크래시하지 않는다)을 모든 입력에 대해 만족한다는 걸 수학적으로 증명하고, 그 증명을 기계(증명 검사기)가 확인하는 방법이에요. 핵심은 증명을 누가 썼든 검사기가 통과시켜야만 인정된다는 점이에요.
시점 정리
– 처음 나온 시기: 호어 논리(Hoare logic)가 1969년, 증명 보조기 Coq(2025년에 Rocq로 개명)가 1989년에 나왔어요. 실전 사례로는 검증된 C 컴파일러 CompCert(2000년대 중후반), seL4 마이크로커널 검증(2009년)이 유명해요. 다만 사람 전문가가 몇 년씩 매달려야 해서 대부분 프로젝트엔 비현실적이었죠.
– 이번에 화제가 된 소식: 2026년 10월 22일(미국 시간), Anthropic과 Theorem이 Claude로 123개 오픈소스 라이브러리, 239개 OSS-Fuzz 진입점에 대해 “64MB 미만 입력에서는 크래시하지 않는다”는 Rocq 증명을 만들었다고 발표했어요(Anthropic 글). 소스코드가 아니라 컴파일된 RISC-V 바이너리 수준에서 증명했고, 그 과정에서 수년간 퍼징으로도 못 찾은 버그도 찾았대요. 같은 주에 AI가 찾은 PHP 취약점으로 유럽 정부 사이트들이 내려가는 일까지 겹쳐서 “테스트로는 부족하다, 증명이 필요하다”는 얘기가 확 커졌어요.
– 단서: 보장은 단일 스레드·정적 바이너리·RISC-V Linux 같은 가정 아래에서만 성립해요. “버그 0″이 아니라 “이 조건에서 이 성질은 확실하다”예요.
Claude만 쓰던 개발자는 어떻게 쓰면 될까요?
– 역할 나누기: 사람은 “무엇을 보장할지”(명세)를 정하고, LLM은 증명을 쓰고, 검사기(Rocq, Lean 등)가 판정해요. LLM의 말을 믿는 게 아니라 검사기 통과 여부를 믿는 구조라서, 환각 걱정이 오히려 적은 분야예요.
– 언제 쓰나: 파서, 직렬화, 암호·인증, 결제 계산처럼 작고 핵심적이며 터지면 큰일 나는 코드에 먼저 써 보세요. Theorem이 공개한 증명 저장소와 Claude 스킬로 시작해 볼 수 있어요.
– 언제 LLM 일반 작업으로 넘기나: UI, 자주 바뀌는 비즈니스 로직, 프로토타입은 증명 비용이 이득보다 커요. 여긴 평소처럼 테스트와 리뷰로 충분해요.
– 팁: 처음부터 증명을 요구하기보다, Claude에게 “이 함수가 지켜야 할 불변식을 명세로 써 줘”부터 시키면 설계 리뷰 도구로도 쓸모가 있어요.
연관 용어
– 명세(Specification): 증명할 성질을 정확하게 적은 것. 명세가 틀리면 증명도 엉뚱한 걸 보장해요.
– 퍼징(Fuzzing)과 OSS-Fuzz: 무작위 입력으로 버그를 찾는 테스트 방식이에요. OSS-Fuzz는 구글이 2016년에 시작했어요. 형식 검증은 “퍼징을 더 안 돌려도 되는” 단계를 노려요.
– 증명 보조기(Proof Assistant): Rocq(구 Coq), Lean 같은 도구로, 증명이 맞는지 기계적으로 검사해요.
오늘도 좋은 하루 보내세요!