Claude, 오픈 소스 소프트웨어에 대한 최초의 대규모 AI 공식 검증에서 1억 8천만 줄의 수학적 증명 작성

전체 보고서

Anthropic은 10월 22일 공식 연구 페이지에서 다음과 같이 발표했습니다. Claude는 소프트웨어 검증 회사인 Theorem과 협력하여 Google의 OSS-Fuzz에서 가져온 123개의 실제 오픈 소스 라이브러리에 걸쳐 RISC-V 어셈블리 수준에서 보안 속성을 공식적으로 검증했으며, 이는 239개의 프로그램 진입점을 포함합니다. 회사는 이를 "AI를 사용해 어셈블리 코드 수준에서 생산 소프트웨어에 형식 검증을 적용하려는 최초의 대규모 노력"이라고 부릅니다.

그 규모는 놀랍습니다. 약 1억 8천만 라인의 Rocq 증명이 있으며, 일반적인 증명은 약 600,000라인에 달하며 중간 길이가 18,000 RISC-V 명령어인 바이너리를 포함하며 모두 몇 주 만에 완료됩니다. Rocq 커널은 각 증명을 독립적으로 확인하므로 수동으로 한 줄씩 검토할 필요가 없습니다.

이 방법은 기존 퍼지 테스트를 수학적 사양으로 변환합니다. 64MB 미만의 입력에 대해 Linux의 단일 스레드 정적으로 링크된 RISC-V 바이너리는 메모리 안전 위반 없이 항상 정상적으로 종료되어야 합니다. Claude는 중간에 버그를 의심했을 때 코드를 직접 패치하고 새로운 사양을 다시 입증했습니다.

범위를 벗어난 쓰기로 이어지는 압축 해제기 복사본의 카운터 언더플로우(드물게 하나의 레이아웃에서 최대 20MB 입력으로만 트리거됨), 이미지 디코더의 범위를 벗어난 읽기, libexpat에서 CVE-2026-56132의 재발견 등 수백 가지 버그가 표면화되었습니다. 일부 취약점은 수년 동안 숨어 있었습니다.

Anthropic은 한계 자체를 인정합니다. 공식 검증을 통과했다고 해서 버그가 없다는 의미는 아닙니다. 검증에서는 단일 스레드 정적 RISC-V 바이너리만 다루고 대부분의 코드는 실제로 x86/ARM에서 실행됩니다. 독립적인 검증을 위해 GitHub에 증명의 하위 집합을 게시했으며 Theorem은 다른 오픈 소스 프로젝트에서도 동일한 파이프라인을 실행할 것이라고 말했습니다.

부작용도 주목할 만합니다. Linux 커널의 zlib 구현은 x86 바이너리 수준에서 RFC 1950을 준수하는 것으로 입증되었으며 Rust로 작성된 Python 인터프리터의 대규모 하위 집합은 170만 개 이상의 무작위 프로그램 중 99.95%에서 CPython의 동작과 일치했습니다.