코드 생성 뒤의 검증도 자동화한다
Anthropic은 2026년 10월 22일 Theorem과 함께 Claude를 이용해 오픈소스 라이브러리 123개의 특정 보안 속성을 증명했다고 발표했다. 기존 퍼즈 테스트를 명세로 바꾸고, AI가 만든 증명을 외부 증명 검사기로 확인하는 방식이다. 테스트에서 발견되지 않은 오류를 찾는 것뿐 아니라 정의한 조건에서 오류가 없음을 보이려는 시도다.
다만 증명은 단일 스레드의 정적 RISC-V 바이너리, 모델링된 Linux 동작과 메모리 조건, 64MB 미만 입력 등 정해진 가정을 따른다. 모든 진입점이나 라이브러리 전체를 증명한 것이 아니며, 일반적인 x86·ARM 배포가 자동으로 같은 보장을 받는 것도 아니다. 회사가 수행한 연구 결과이고 일부 증명과 실행 의미론을 공개했다는 범위로 읽어야 한다.
증명 검사기는 명세의 적절성까지 보장하지 않는다
이번 연구의 의미는 AI 코딩의 완료 조건을 “테스트가 통과했다”에서 더 명시적인 속성 검사로 확장한다는 데 있다. 그러나 기계가 확인한 증명도 명세가 실제 요구와 다르면 부족할 수 있다. 개발팀은 어떤 입력·환경·호출 규약을 다뤘는지 먼저 확인하고, 배포 조건이 달라지거나 의존성이 바뀔 때 증명을 재검토해야 한다. 이를 모든 소프트웨어가 무결점이 됐다는 선언이나 기존 보안 검토를 생략할 근거로 사용해서는 안 된다.