LLM으로 대규모 소프트웨어 형식 검증이 현실화되다

핵심 요약

• Anthropic과 Theorem이 협력해 Claude로 100개 이상의 실제 오픈소스 라이브러리 어셈블리 코드(RISC-V)에 대한 형식 증명을 생성했으며, 이는 AI를 활용한 프로덕션 소프트웨어의 대규모 형식 검증 최초 사례다.
• 개발자의 퍼지 테스트(fuzz test)를 자동으로 형식 사양으로 변환해 증명했으며, 239개 엔트리포인트에서 64MB 이하 모든 입력에 대해 크래시가 없음을 증명했다.
• 총 약 1억 8천만 줄의 Rocq 증명을 작성했고, 전형적인 증명은 약 60만 줄의 코드로 18,000개 RISC-V 명령어에 대한 보안 보장을 제공한다.
• Claude는 증명 과정에서 수년 동안 발견되지 않은 버그들을 찾았는데, 20MB 크기 입력이나 64MB 입력, 특정 파일 호출 시퀀스, 깊게 중첩된 입력 등 퍼지가 놓치기 쉬운 조건에서만 나타나는 버그들도 포함됐다.
• 증명은 RISC-V 명령어와 Linux 프로세스 의미론(semantics)으로 구현되며, 현재는 단일 스레드 정적 바이너리이면서 고정 메모리 예산을 가진 RISC-V CPU 상 Linux OS 환경을 가정한다.
• 개발자가 신뢰해야 할 대상은 RISC-V와 Linux 형식 모델, 증명된 정리 명제, Rocq 증명 검사기 3가지뿐이며, 1억 8천만 줄의 증명 코드는 자동으로 검증되므로 수동 검토가 거의 필요 없다.
• RFC 1950을 따르는 zlib 압축 형식의 형식 사양을 작성하고 Linux 커널의 zlib 구현을 x86 바이너리 수준에서 증명했으며, 과정 중 여러 미개발된 버그를 발견했다.
• Python 인터프리터를 Rust로 구현해 CPython 의미론을 Verus로 증명했고, 170만 개의 무작위 Python 프로그램 실행 결과 99.95%에서 동일한 동작을 확인했다.
• Opus 5.5는 이전 모델 대비 약 40% 더 적은 토큰으로 검증 작업을 완료하며, 증명을 공유하는 에이전트 팀은 단독 작업보다 17% 적은 토큰을 사용했다.
• 형식 증명은 재사용 가능하며, 프로그램 초기화 코드 같은 공통 부분이 많아서 새 프로그램에 기존 증명을 복사해 적응시키는 방식으로 효율성을 높일 수 있다.
• 형식 검증의 한계는 증명이 단일 스레드 정적 RISC-V 바이너리만 다루고, 실제 배포 시스템(x86, ARM, glibc 동적 링크)과 다르며, 64MB 이상 입력이나 모든 엔트리포인트를 검증하지 않는다는 점이다.
• 형식 검증된 코드가 버그가 없다는 뜻이 아니라, 증명이 형식 사양 충족을 검증할 뿐 사양이 현실 기계의 모든 측면을 반영하는지는 증명 검사기가 판단할 수 없다.
• Anthropic은 증명된 라이브러리의 부분 집합을 공개하며, Theorem과 협력해 다른 오픈소스 프로젝트에도 같은 파이프라인을 적용할 계획이고, 개발자가 자체 코드 검증을 시작할 수 있도록 Claude 기술을 제공한다.