앤트로픽, 클로드로 오픈소스 123개 '충돌 없음' 증명…증명 코드만 1억8천만줄

앤트로픽이 클로드로 오픈소스 라이브러리 123개가 어떤 입력에도 충돌하지 않는다는 사실을 형식 검증(formal verification)으로 증명했다고 밝혔다. 증명을 쓰는 과정에서 수년 동안 드러나지 않던 버그 수백 개도 찾아 고쳤다.

22일(현지시간) 앤트로픽 프런티어 레드팀 블로그에 따르면 클로드는 몇 주 동안 구글 오픈소스 퍼징 프로젝트(OSS-Fuzz)의 라이브러리 123개, 테스트 진입점 239개를 증명했다. 64MB 이하 입력이면 메모리 오류나 단정(assertion) 실패 없이 끝난다는 내용이다. 증명은 컴파일된 RISC-V 기계어를 대상으로 했고, 분량은 증명 언어 로크(Rocq)로 1억8천만줄에 이른다. 스타트업 시어럼(Theorem)과 함께 진행했다. 20MB짜리 특정 입력에서만 터지는 압축 해제 버그처럼 퍼저로는 찾기 어려운 것들이 나왔고, 한 PDF 리더에서는 보통 1년 동안 보고되는 만큼의 보안 버그를 일주일 만에 찾았다고 덧붙였다.

형식 검증은 운영체제 커널 seL4를 만드는 데 2인년, 검증하는 데 20인년이 들 만큼 비싼 작업이었다. 앤트로픽은 형식 검증이 "곧 지금의 퍼징만큼 실용적이 될 것"이라고 전망했다. 오퍼스 5.5는 같은 검증 과제를 오퍼스 5보다 토큰을 40% 적게 쓰고 풀었다. 다만 증명 하나에 토큰 수억 개가 들고, 단일 스레드·정적 링크 RISC-V 리눅스라는 가정 아래 결과여서 x86·ARM 실제 환경과는 차이가 있다는 한계도 밝혔다. 시어럼은 다른 오픈소스에도 같은 작업을 돌려 주겠다며 클로드 스킬을 공개했다. 공식 X 글은 조회 16만회를 넘겼다.