Anthropic과 Theorem이 Claude를 활용하여 오픈소스 라이브러리의 정형 검증을 수행한 연구 결과를 소개해 드립니다. 이번 실험에서는 123개의 라이브러리에서 수백 개의 버그를 발견했으며, 기존의 퍼징 테스트를 명세로 변환하여 RISC-V 바이너리 수준에서 증명하는 방식을 사용했습니다. 비록 막대한 토큰 비용이 발생하지만, 모델 개선과 증명 재사용을 통해 효율성을 높일 수 있음을 보여주었습니다. 정형 검증이 모든 버그를 완벽히 제거하는 것은 아니지만, 향후 개발 프로세스에 내장된 핵심 도구로 발전할 가능성이 매우 높습니다.