클로드 정형 검증, 서비스 테스트를 대체할 수 있을까?

검증된 라이브러리를 가져와도 서비스 전체가 검증되지는 않는다

클로드의 정형 검증 소식만으로 서비스 테스트를 없앨 수는 없다. 증명이 성립하는 대상은 정해진 조건으로 만든 실행 파일과 그 파일이 지켜야 할 명세다. 그 라이브러리를 다른 환경에서 빌드하고 앱에 연결했을 때의 모든 동작까지 한꺼번에 보장하지 않는다.

Anthropic과 Theorem의 10월 22일 발표는 특정 테스트 진입점을 대상으로 한 증명을 다뤘다. 연구진은 클로드로 오픈소스 라이브러리의 테스트 진입점에 관한 증명을 작성하고, Rocq라는 증명 검사기로 확인했다. AI가 ‘안전하다’고 대답하는 데서 끝나는 코드 리뷰와는 다른 방식이다.

개발자의 판단 기준도 달라진다. 라이브러리에 검증 이력이 있는지를 넘어, 내가 사용하는 실행 파일과 환경, 보장받고 싶은 속성이 그 증명 안에 들어 있는지를 봐야 한다.

기존 테스트가 ‘무엇을 증명할지’를 제공한다

퍼징은 생성하거나 변형한 입력을 테스트 진입점에 넣어 실패를 찾는다. 진입점은 입력을 받아 라이브러리의 기능을 호출하는 작은 테스트 프로그램이다. 많이 실행할수록 더 많은 경우를 살피지만, 시도하지 않은 입력은 남는다.

이번 연구는 그 테스트를 컴파일한 RISC-V 실행 파일을 대상으로, 명세의 조건에 해당하는 모든 입력에서 정해진 오류가 발생하지 않는다는 증명을 만드는 접근이다. 테스트가 검사하던 속성이 증명의 출발점이 된다. Theorem의 설명처럼 어떤 조건 위반을 테스트의 실패로 표현하느냐가 증명으로 얻을 답을 결정한다.

실행 환경도 수학적으로 표현해야 한다. Linux Process Semantics 모델은 RISC-V 프로그램의 실행과 외부에서 관찰할 수 있는 동작을 기술한다. 증명 검사기는 이 모델과 정리에 맞는 논증인지를 검사한다. 현실의 운영체제와 모델이 일치하는지까지 자동으로 해결해 주는 것은 아니다.

연구 전체는 123개, 공개 증명은 25개 라이브러리다

Anthropic의 연구 전체 수치와 공개 저장소의 범위는 다르다. 2026년 10월 26일 기준으로 확인할 내용은 다음과 같다.

마지막 차이는 크다. 오류 없이 실행한다는 속성과 언젠가 반드시 끝난다는 속성은 다르다. 저장소는 이번 공개본에는 모든 실행이 끝난다는 증명을 포함하지 않았다고 명시한다. 이를 ‘어떤 입력에서도 반드시 정상 종료한다’고 읽으면 보장 범위를 넓히게 된다.

검사 기능이 잡지 못하는 잘못된 계산 결과나 메모리 누수까지 모두 배제하는 것도 아니다. 특정 진입점에서 도달하지 않는 코드, 다른 빌드와 실행 환경은 별도로 봐야 한다. 라이브러리 이름 하나가 전체 품질 인증서가 되는 방식은 아니다.

기존 퍼징 타깃에서 출발하되, 배포 환경의 테스트는 남긴다

이 기술을 도입하려는 오픈소스 유지보수자에게는 기존 퍼징 타깃이 출발점이다. Theorem은 조건을 충족하는 오픈소스 프로젝트에 무료 검증 프로그램을 제공한다. 참여는 프로젝트 정보, 빌드 환경을 만드는 Dockerfile, 테스트 타깃을 빌드하는 스크립트를 저장소에 PR로 제출하는 방식이다. 기존 OSS-Fuzz 프로젝트라도 정적 riscv64 빌드에 맞추는 작업이 필요할 수 있다.

산출물을 받으면 진입점, 대상 바이너리, 정리의 입력·메모리 조건을 실제 사용 환경과 연결해야 한다. x86이나 ARM에서 빌드한 서비스라면 RISC-V 바이너리에 관한 증명을 그대로 적용할 수 없다. 앱이 라이브러리를 호출하는 방식과 검증되지 않은 동작도 계속 시험해야 한다.

증명이 제공하는 것은 확인된 조건 안의 더 강한 보장이다. 테스트는 그 밖의 환경과 요구사항을 다룬다. 두 범위를 정확히 연결할 때 AI가 쓴 증명을 실제 소프트웨어의 품질 관리에 사용할 수 있다.

자주 묻는 질문