앤트로픽은 정리증명 전문 시어럼과 함께 OSS-Fuzz에 등록된 오픈소스 라이브러리들을 대상으로 대규모 형식 검증을 진행했다고 밝혔다. 클로드는 기존 퍼즈 테스트를 기준으로 삼아, 컴파일된 RISC-V 어셈블리 코드를 수학적 명제로 바꾼 뒤 64MB 미만의 모든 입력에서 테스트가 충돌 없이 끝나는지 증명했다. 검증은 123개 라이브러리의 239개 테스트 진입점에 대해 이뤄졌고, 메모리 안전성 오류나 단언문 실패가 없다는 조건도 포함됐다. 생성된 증명은 로크 형식으로 작성됐으며, 결과 확인은 증명 검사기가 맡는다.
형식 검증은 코드가 항상 규칙을 지키는지 수학적으로 확인하는 방식이지만, 보통 많은 시간과 전문성이 필요해 적용 범위가 좁았다. 이번 작업은 AI를 이용해 실제 운영 환경에 쓰이는 소프트웨어를 어셈블리 코드 수준에서 대규모로 검증한 사례로 제시됐다. 또한 클로드는 증명 과정에서 발견한 문제를 수정하고 다시 검증했으며, 수백 건의 버그를 찾아냈다. 여기에는 큰 입력 크기, 복잡한 메모리 조건, 특정 호출 순서, 깊게 중첩된 입력에서만 드러나는 오류가 포함돼, 퍼즈 테스트만으로 놓칠 수 있는 문제를 보완했다.