Claude, 오픈소스 123개 '충돌 없음' 증명…버그 수백 건 찾아

Anthropic은 10월 22일(현지시간) Claude로 오픈소스 라이브러리 123개의 컴파일된 기계어 코드가 충돌하지 않는다는 사실을 수학적으로 증명했다고 밝혔다. 형식 검증 기업 Theorem과 함께 진행한 이 작업에서 Claude는 증명을 쓰는 과정에서 수년간 발견되지 않던 버그 수백 건도 찾아냈다.

핵심 정리

• Anthropic Frontier Red Team은 Google OSS-Fuzz에 등록된 라이브러리 123개, 진입점 239개에 대해 RISC-V 바이너리 수준의 보안 증명을 몇 주 만에 완성했다.
• 증명은 64MB 미만의 어떤 입력에도 프로그램이 메모리 안전성 오류나 단언 실패로 멈추지 않는다는 내용이며, 전체 분량은 Rocq 코드 약 1억8천만 줄이다.
• Theorem은 증명 일부와 RISC-V·리눅스 의미론을 GitHub에 공개하고 오픈소스 프로젝트 대상 무료 검증 서비스 OSS Verify를 열었다.

Claude 형식 검증, 무엇을 증명했나

Claude가 증명한 성질은 "퍼즈 테스트 대상 함수가 64MB 미만의 어떤 입력을 받아도 충돌하지 않는다"는 것이다. Anthropic이 공개한 연구 보고서에 따르면 증명 대상은 소스 코드가 아니라 컴파일을 마친 RISC-V 바이너리다. 메모리 안전성 위반과 단언 실패가 모두 '충돌'에 포함된다. 운영체제가 돌려줄 수 있는 모든 응답과 메모리 배치까지 모델에 넣었다.

규모도 컸다. 증명 하나는 보통 약 60만 줄이고, 검증한 바이너리의 길이는 중앙값 기준 RISC-V 명령어 1만8천 개다. 증명은 Rocq 증명 검사기가 기계적으로 확인한다. Anthropic은 AI로 실제 운영 소프트웨어를 어셈블리 수준에서 대규모로 형식 검증한 첫 사례로 알고 있다고 설명했다.

증명하다 찾은 버그 수백 건

증명이 막히는 지점이 곧 버그였다. Anthropic은 명세를 증명하려는 과정에서 버그 수백 건을 발견했고, Claude가 이를 패치한 뒤 명세를 다시 만들어 재증명했다고 밝혔다. 이미 수조 번의 퍼징 테스트를 거친 코드에서도 문제가 나왔다.

공개된 사례 가운데 하나는 압축 해제 라이브러리의 카운터 언더플로였다. 약 20MB 크기 입력이 특정한 형태로 배치될 때만 경계 밖 쓰기로 이어지는 버그다. 이미지 디코더에서는 64MB 입력과 2GB 넘는 메모리가 있어야 드러나는 경계 밖 읽기가 나왔다. libexpat의 기존 취약점 CVE-2026-56132도 다시 찾아냈다.

형식 검증이 왜 어려웠나

형식 검증은 그동안 비용 때문에 일부 핵심 시스템에만 쓰였다. Anthropic은 운영체제 커널 seL4를 예로 들며 구현에 2인년, 검증에 20인년이 들었다고 짚었다. AI가 버그를 쉽게 찾고 악용하는 시대에는 테스트만으로 방어가 부족하다는 것이 연구진의 문제의식이다.

모델 효율도 개선됐다. 작은 과제 36개로 시험한 결과 Claude Opus 5.5는 그중 절반을 Opus 5보다 약 40% 적은 토큰으로 증명했다. 여러 AI 에이전트가 작업 공간을 공유하면 단독 작업보다 토큰을 17% 덜 썼다. 다만 증명 하나에 토큰 수억 개가 들 수 있다고 덧붙였다.

한계와 오픈소스 공개 범위

Anthropic은 "형식 검증됨"이 "버그 없음"을 뜻하지 않는다고 못 박았다. 증명은 musl로 정적 링크한 단일 스레드 RISC-V 바이너리를 전제로 하는데, 실제 배포 환경은 대부분 x86·ARM과 동적 링크 glibc다. 명세나 기계 모델이 현실과 어긋나는 곳에는 버그가 남을 수 있다. Claude가 코드를 고쳐 증명을 쉽게 만드는 '보상 해킹'을 막으려고 패치를 감점하고 모두 기록해 검토했다.

공개 자료는 GitHub에 올라왔다. oss-verify-proofs 저장소에는 openssl, zstd, mbedtls 등 25개 라이브러리 60개 진입점의 증명이 MIT 라이선스로 공개됐다. 아직 패치되지 않은 버그를 드러낼 수 있는 증명은 공개하지 않았다.

개발자에게 달라지는 점

Theorem은 핵심 메인테이너가 신청하면 프로젝트를 무료로 검증해 주는 OSS Verify를 열었다. 발견한 버그는 메인테이너에게 비공개로 알린다. AI가 만든 보안 패치가 다른 기능을 깨뜨린다는 Trail of Bits의 재검증 결과처럼 AI 코드의 신뢰성 문제가 커지는 가운데, 연구진은 형식 검증이 지금의 퍼징만큼 일상적인 도구가 될 수 있다고 내다봤다.

자주 묻는 질문

Claude가 검증한 라이브러리는 이제 버그가 없나?

아니다. 증명은 64MB 미만 입력에서 충돌하지 않는다는 성질만 다루며, 정적 링크 RISC-V 바이너리라는 가정 위에서 성립한다. Anthropic도 명세나 기계 모델이 현실과 다르면 버그가 남을 수 있다고 밝혔다.

내 오픈소스 프로젝트도 검증받을 수 있나?

Theorem의 OSS Verify에 신청하면 된다. 핵심 메인테이너가 theorem-labs/oss-verify 저장소에 프로젝트 설정 파일을 담은 풀 리퀘스트를 올려야 하며, Theorem이 성숙도와 사용 범위 등을 보고 개별 심사한다. 비용은 무료다.

형식 검증에는 어떤 도구가 쓰였나?

증명은 Rocq(옛 Coq) 증명 검사기로 확인했고, 기계 모델로는 Theorem이 만든 RISC-V 명령어·리눅스 프로세스 의미론을 썼다. Rust로 만든 파이썬 인터프리터 실험에는 Verus가 쓰였다.