퍼징으로 찾기 어려운 버그까지 —Claude, 오픈소스 123개 라이브러리 239개 진입점에 '64MB 안 어떤 입력에도 안 멈춘다' 증명
Anthropic이 10월 22일 연구 글에서 Theorem과 함께 Claude로 오픈소스 라이브러리의 '절대 멈추지 않음(no-crash)'을 기계가 검사하는 수학 증명으로 만들었다고 밝혔어요. 증명하는 동안 수년간 안 잡히던 버그도 찾아 고쳤어요.
- Anthropic과 Theorem이 Claude로 Google OSS-Fuzz의 오픈소스 라이브러리 123개, 진입점 239개에 대해 '64MB보다 작은 어떤 입력에도 멈추지 않는다'는 증명을 몇 주 만에 만들었어요(찾은 버그는 고친 뒤).
- 증명은 소스 코드가 아니라 컴파일된 RISC-V 기계어를 대상으로 하고, Rocq 증명 검사기가 확인해요. 전체 약 1억 8천만 줄, 증명 하나는 보통 약 60만 줄이에요.
- 증명하는 과정에서 퍼저(무작위 입력 테스트)로는 잘 안 잡히는 버그도 나왔어요. 약 20MB 입력에서만 생기는 범위 밖 쓰기 같은 것들이에요. 다만 원문은 '검증됨'이 '버그 없음'은 아니라고 선을 그었어요.
C · C++ 라이브러리를 OSS-Fuzz 방식 퍼즈 테스트로 관리하고 있다면, Theorem의 OSS Verify에 무료로 신청해 '이 퍼즈 테스트는 어떤 입력에도 멈추지 않는다'는 증명과 버그 제보를 받아 볼 수 있어요(심사 있음 · 핵심 메인테이너만 신청).
퍼징을 오래 돌려도 1MB 넘는 큰 입력이나 드문 호출 순서에서만 나는 버그는 놓칠 수 있다는 사례로 읽어 두면 좋아요. 쓰는 라이브러리가 공개된 증명 목록에 있는지도 확인해 볼 만해요.
직접 쓸 도구는 아니에요. 'AI가 코드를 고치는 것'을 넘어 '버그가 없다는 걸 증명하는 것'까지 가고 있다는 흐름으로 보면 돼요.
OSS Verify 신청(Theorem 안내 그대로): 1) theorem-labs/oss-verify 저장소에 pull request를 연다 2) projects/<your-project>/ 폴더에 project.yaml · Dockerfile · build.sh 세 파일을 넣는다 3) 이미 OSS-Fuzz에 있는 프로젝트면 그 파일에서 시작한다 — 다만 OSS Verify는 static riscv64 바이너리가 필요해 빌드를 옮겨야 할 수 있어요. 자세한 건 공식 안내를 따르세요.
직접 관리하는 C · C++ 오픈소스가 있다면 OSS Verify 무료 신청에 써 보면 좋을 것 같아요. 그 밖의 작업자에겐 당장 쓸 곳은 적어 보여요. 다만 AI 코드 검증이 어디까지 왔는지 보여 주는 기준점으로 기억해 둘 만해요.
Anthropic이 10월 22일 연구 글 「LLMs are making formal software verification feasible at a much larger scale」에서 Theorem과 함께 Claude로 형식 검증(formal verification · 코드가 정한 규칙을 늘 지킨다는 걸 수학 증명으로 보이는 방법)을 큰 규모로 해냈다고 밝혔어요. Anthropic은 '알기로는 AI로 실제 쓰이는 소프트웨어를 어셈블리 수준에서 대규모로 형식 검증한 첫 시도'라고 적었어요.
무엇을 증명했나
출발점은 퍼즈 테스트(fuzz test)예요. 개발자가 입력을 받는 진입점(entry point)을 만들어 두면, 퍼저가 반쯤 무작위로 바꾼 입력을 엄청나게 넣어 멈추는(crash) 입력을 찾아요. 오래 돌릴수록 많이 찾지만, 모든 경로를 지나간다는 보장은 없어요.
이번엔 퍼즈 테스트를 '64MB보다 작은 어떤 입력에도 멈추지 않는다'는 명세로 바꾸고, Claude가 그 증명을 썼어요. Google의 OSS-Fuzz(오픈소스 프로젝트에 퍼징을 계속 돌려 주는 프로그램)에 있는 프로젝트가 대상이었어요.
- 규모: 몇 주 동안 라이브러리 123개 · 진입점 239개. 찾은 버그는 Claude가 먼저 고치고 나서 증명했어요.
- 대상: 소스 코드가 아니라 컴파일된 RISC-V 명령어(실행 파일). 메모리 오류를 잡는 AddressSanitizer(ASan) 충돌도 포함해요.
- 분량: Rocq(증명 도구) 코드 약 1억 8천만 줄. 증명 하나는 보통 약 60만 줄이고, 대상 바이너리는 중간값 1만 8천 개 RISC-V 명령어예요.
- 검사: 증명은 Rocq 증명 검사기가 확인해요. 그래서 사람이 믿어야 하는 건 RISC-V · Linux 프로세스 모델, 증명한 정리 문장, Rocq 검사기 자체라고 해요.
퍼징이 놓친 버그
증명을 시도하는 과정에서 버그가 수백 개 나왔다고 해요. 원문은 그중 많은 수가 퍼저로는 찾기 어려운 것이라고 했어요. 퍼저는 보통 1MB 이하의 작은 입력을 바꿔 가며 쓰기 때문이에요. 원문이 든 예는 이래요.
- 한 라이브러리 안 압축 해제 코드에서, 약 20MB에 드문 배치를 가진 입력에서만 생기는 범위 밖 쓰기
- 이미지 디코더에서 64MB 입력과 2GB 넘는 메모리가 있어야 생기는 범위 밖 읽기
- 같은 파일에 대한 두 핸들에 특정 순서로 호출해야 생기는 범위 밖 읽기
- 깊게 중첩된 입력이 필요한 libexpat의 CVE-2026-56132 재발견
- 멈추지는 않는 논리 버그 — 앱이 불러올 수 있는 파일을 제한하는 기능이 늘 적용되지는 않는 문제
다른 실험들
- zlib: Claude가 RFC 1950(zlib 형식 문서)의 형식 명세를 쓰고, Linux 커널 안 zlib 구현이 그 명세를 지킨다는 걸 x86 바이너리 수준에서 증명했어요.
- Rust로 만든 Python 인터프리터: Claude가 만들고 Verus로 증명했어요. 무작위 Python 프로그램 170만 개 넘게 돌려 보니 99.95%에서 CPython과 똑같이 동작했어요.
- PDF 리더: 검증 시도 일주일 동안 보통 1년에 보고되는 만큼의 보안 버그를 찾았다고 해요.
비용은 줄어드는 중
증명 하나에 토큰이 수억 개 들 수 있다는 게 한계예요. 다만 실제 OSS-Fuzz 코드로 만든 작은 검증 과제 36개에서 Opus 5.5는 절반을 Opus 5보다 약 40% 적은 토큰으로 증명했어요. 에이전트끼리 서로의 증명을 베껴 쓸 수 있게 하자 혼자 할 때보다 토큰이 17% 덜 들었어요.
공개된 것 · 신청하는 법
Anthropic은 증명 일부와 RISC-V · OS 모델을 공개했어요. GitHub 저장소 README 기준으로 지금 라이브러리 25개 · 진입점 60개의 증명이 올라와 있어요. Theorem은 같은 과정을 자격을 갖춘 오픈소스 프로젝트에 무료로 돌려 주는 'OSS Verify'를 열었어요. 프로젝트마다 심사하고, 핵심 메인테이너만 신청할 수 있어요. 증명은 며칠이 걸릴 수 있고, 찾은 버그는 메인테이너에게 비공개로 알려 준다고 해요.
읽을 때 주의
원문은 '형식 검증됨이 버그 없음은 아니다'라고 따로 적었어요. 이번 증명은 단일 스레드 · 정적 RISC-V 바이너리 · musl libc를 가정하는데, 실제로는 x86 · ARM에서 glibc와 함께 많이 써요. ASan이 모든 메모리 버그를 잡지는 못하고, 라이브러리마다 모든 진입점을 검증한 것도 아니에요. 또 Claude가 코드를 고치는 과정은 '보상 해킹'(프로그램을 아예 안 멈추게 바꿔 버리는 꼼수)의 여지가 있어, 패치에 벌점을 주고 기록 · 감사했다고 밝혔어요.
