Anthropic과 Theorem은 Claude로 오픈소스 라이브러리 123개의 퍼징 진입점 239개를 수정하고, 64MB 미만 입력에서 충돌하지 않는다는 증명을 만들었다. 약 1억8000만 줄의 Rocq 증명 코드를 검사기가 검증한다. 보장은 고정 메모리의 단일 스레드 정적 RISC-V 바이너리와 Linux 모델에 한정되며 라이브러리 전체의 무결함을 뜻하지 않는다. 별도 Vero 평가도 개별 명세 통과율과 저장소 전체 증명 완료가 다름을 보여 줘, 증명 범위와 신뢰 기반을 확인하는 일이 중요하다.