코드가 명세대로 동작함을 수학적으로 증명하는 형식 검증은 오랫동안 보안의 최고 기준이었지만 거의 모두에게 너무 비쌌습니다. Anthropic은 분명한 예를 듭니다. seL4 커널은 작성에 2인년, 검증에 20인년이 걸렸습니다. Anthropic은 검증 전문 기업 Theorem과 함께 Claude가 몇 년 전만 해도 상상하기 어려웠던 규모로 이런 증명을 만들어 냈다고 보고합니다.
비결은 명세를 손으로 쓰지 않은 데 있습니다. 팀은 Google OSS-Fuzz 프로그램의 퍼즈 테스트, 즉 어떤 충돌이든 버그로 치는 작은 진입점들을 가져와 각각을 형식적 주장으로 바꿨습니다. 컴파일된 RISC-V 바이너리는 64 MB 미만의 어떤 입력에서도, AddressSanitizer가 잡는 메모리 안전 오류를 포함해 충돌하지 않는다는 것입니다. 몇 주 동안 Claude는 123개 라이브러리의 239개 진입점에 대해 이를 증명했고, 그 과정에서 찾은 버그를 고쳤습니다. 증명은 주로 증명 보조기 Rocq로 작성됐으며 모두 약 1억 8,000만 줄입니다. 전형적인 증명은 명령어 수 중앙값이 18,000개인 바이너리에 대해 약 600,000줄입니다. 사람이 읽을 필요는 없고 Rocq 검사기가 확인합니다.
당장의 성과는 버그입니다. 일부는 퍼저로는 좀처럼 찾기 어려운 것이었습니다. 예를 들어 한 압축 해제기의 범위 밖 쓰기는 특정 구조를 가진 약 20 MB 입력에서만 나타났습니다. 별도 실험에서는 Linux 커널의 zlib을 RFC 1950의 형식 버전에 비추어 증명했고, Python 일부를 처리하는 Rust 인터프리터를 검증해 170만 개 무작위 프로그램의 99.95%에서 CPython과 같게 동작함을 확인했습니다. 비용도 내려가고 있습니다. 36개 소규모 과제에서 Claude Opus 5.5는 Opus 5보다 약 40% 적은 토큰으로 절반을 증명했고, 에이전트끼리 증명을 공유하자 17%가 절약됐습니다.
라이브러리 관리자에게 이는 퍼징이 그랬듯 기계로 검증된 보장이 흔한 라이브러리에서 일상이 될 수 있다는 지금까지 가장 강력한 근거입니다. Theorem은 다른 오픈 소스 프로젝트에도 이 과정을 돌려 주겠다고 제안했고 Claude 스킬도 공개했습니다.
저자들은 한계에 대해 신중하며, 독자도 그래야 합니다. 검증됐다는 것은 버그가 없다는 뜻이 아닙니다. 증명은 musl에 정적으로 링크된 단일 스레드 RISC-V 빌드를 대상으로 하지만, 대부분의 사용자는 이 라이브러리를 x86이나 ARM에서 glibc와 함께 씁니다. AddressSanitizer가 모든 메모리 버그를 잡지는 못하고, 모든 진입점을 다룬 것도 아니며, 호출하는 쪽이 라이브러리를 잘못 쓸 가능성도 남습니다. 증명에 수억 토큰이 들 수 있다는 점도 생태계 전체로 넓히는 데 진짜 장벽입니다.