Claude가 소프트웨어의 특정 오류가 없음을 증명한 방법

배경과 문제

성숙하고 광범위하게 테스트된 소프트웨어에도 버그는 존재한다. 예를 들어 Linux 커널은 최근 1,000개 이상의 취약점이 공개되었는데, 이는 수십억 대의 기기에 배포된 코드에서도 결함이 흔하다는 것을 보여준다. LLM은 이런 버그를 찾는 데 점점 능숙해지고 있으며, 겉보기에 무해한 버그들을 연결해 심각한 공격으로 만드는 능력도 향상되고 있다. 따라서 버그를 악용되기 전에 탐지하고 수정할 수 있는 기술이 필요하다.

정형 검증(formal verification)은 프로그램과 실행 환경을 수학적으로 표현하고, 정해 둔 규칙을 만족함을 증명하는 방법이다. 증명 시도에서 버그가 드러날 수 있지만, 증명에 실패했다고 반드시 버그가 있다는 뜻은 아니다. 증명 방법이나 계산 자원이 부족할 수도 있다. 저자들이 드는 과거 사례인 seL4 운영체제 커널은 구현에 2인년, 검증에 20인년이 들었다. 사람이 직접 긴 증명을 만드는 비용 때문에 안전이 특히 중요한 항공전자 코드 같은 영역에서 주로 사용됐고, 이번 연구는 AI로 그 작업을 확장하려는 시도다.

기존 접근의 한계

퍼징(fuzzing)은 개발자가 마련한 테스트 진입점에 무작위로 만들거나 변형한 입력을 대량으로 넣어 충돌을 찾는 기법이다. 오래 실행하면 더 많은 경우를 시험할 수 있지만, 시험하지 않은 입력이나 코드 경로에 문제가 없다고 보장하지는 못한다. 입력 크기를 제한하더라도 가능한 조합은 매우 많다. 이번 연구는 이런 테스트의 조건을 명시적인 수학 명제로 바꿔, 정해진 범위의 입력 전체를 다루려 한다.

정형 검증은 이런 한계를 극복할 수 있지만, 전통적으로는 증명을 작성하는 데 전문가의 수년간 노력이 필요했다. 증명은 코드보다 훨씬 길고, 수만 개의 어셈블리 명령어가 모든 입력과 운영체제 응답에 대해 어떻게 동작하는지 포괄하는 논증을 작성하는 것은 매우 어렵다. 이 때문에 대부분의 실제 프로젝트에는 비현실적이었다.

연구방법을 단계별로

첫 단계는 기존 퍼즈 테스트를 명세(specification)로 바꾸는 일이다. 여기서 명세는 어떤 실행 환경과 입력을 허용하고, 무엇을 오류로 볼지 정한 진술이다. 부록은 입력을 64MiB 미만으로 제한한다. 본문이 쓴 64MB보다 부록의 단위를 따르는 편이 정확하다. 이 조건 안에서 충돌이 없음을 증명하면 동일한 실행 파일·모델·진입점·입력 범위를 다시 퍼징해도 해당 종류의 충돌은 찾지 못한다. 다른 환경이나 검증하지 않은 기능의 테스트까지 필요 없어지는 것은 아니다.

둘째, 오픈소스 라이브러리와 테스트를 RISC-V 실행 파일로 컴파일한다. 실행 파일, Theorem의 CPU·운영체제 형식 의미론, 원하는 무충돌 속성에서 명세를 만들고 Claude가 증명을 작성한다. Rocq 검사기는 그 증명이 명세를 만족하는지 확인한다. 실제 대상은 Linux에서 musl libc에 연결한 단일 스레드 정적 바이너리이며, 고정된 메모리 예산과 모델이 허용한 운영체제 응답·메모리 배치가 전제다. AI가 옳다고 주장하는 것만으로 통과시키는 방식은 아니다.

셋째, 증명 도중 버그를 발견하면 Claude가 코드를 패치하고 바뀐 코드의 명세를 다시 만든다. 다만 프로그램을 아무 일도 하지 않게 고치면 충돌만 피하는 쉬운 답이 될 수 있다. 연구팀은 이런 보상 해킹을 줄이려고 패치에 불이익을 주고, 어떤 입력의 동작을 얼마나 적게 바꿨는지 증명하면 추가 점수를 주며 변경 내용을 기록·감사했다. 이런 장치를 두었다는 것이 부적절한 수정 가능성을 완전히 제거했다는 뜻은 아니다.

결과와 숫자의 의미

몇 주에 걸쳐 Claude는 123개 OSS-Fuzz 라이브러리의 239개 진입점에 대해 충돌 없음을 증명했다. 이 증명들은 약 1억 8천만 줄의 Rocq 코드로 구성되며, 대표적인 증명은 약 60만 줄에 달한다. 증명 대상 바이너리의 중앙값 길이는 18,000개의 RISC-V 명령어이다. 증명 검사기는 하나의 증명을 검사하는 데 CPU 시간으로 30분에서 수 시간이 걸릴 수 있다.

보장은 세 부분으로 나뉜다. ASan(AddressSanitizer) 검사를 넣은 바이너리가 메모리 접근 fault, 단언 실패에 따른 abort, 모델 밖 동작을 일으키지 않는지 보인다. 이어 검사를 넣지 않은 일반 바이너리와 관찰 가능한 입출력·종료 유형·파일시스템 상태가 같음을 보이고, 일반 바이너리도 충돌하지 않음을 별도로 증명한다. 부록의 동작 동등성은 침묵하는 무한 반복과 충돌을 구별하지 못할 수 있어 마지막 증명이 필요하다. 따라서 이를 모든 실행이 반드시 끝난다거나 모든 기능이 의도대로 동작한다는 보장으로 읽어서는 안 된다.

증명 시도는 드문 입력이나 특정 호출 순서에서만 드러나는 메모리 오류와 논리 오류도 찾았다. 이는 보통의 테스트가 우연히 도달하기 어려운 조건을 따져 보는 과정의 이점이다. 다만 약 10억 줄의 생성 시도 가운데 약 1억 8천만 줄이 성공한 증명에 포함됐다는 것은 코드의 분량이다. 전체 시도에서 성공한 과제의 비율이나 전체 라이브러리 코드의 검증 비율로 환산할 수 없다.

구체적인 예시

LZO 압축 테스트는 입력을 압축한 뒤 다시 풀면서 과정이 성공하는지, 되돌아온 바이트 수가 원래 길이와 맞는지 단언한다. 단언이 실패하면 충돌로 처리하므로, 이 테스트가 충돌하지 않음을 증명하려면 단순히 메모리를 안전하게 읽는 것 이상의 계산 성질을 보여야 한다. 어떤 높은 수준의 성질이 보장되는지는 테스트의 단언과 실제로 증명한 명제에 달려 있다.

cpp-httplib의 증명에서는 std::set 소멸자의 과도한 재귀로 인한 스택 오버플로 가능성을 배제해야 했다. 이 재귀 깊이는 트리의 최대 깊이에 의해 제한되므로, Claude는 기계 코드 수준에서 libc++의 레드-블랙 트리 재균형 알고리즘이 트리 깊이를 로그적으로 유지하도록 올바르게 최적화되어 있음을 증명해야 했다.

별도 사례에서는 Python의 지원 부분집합을 안전한 Rust로 구현하고 Verus로 검증했다. 증명한 것은 해석기가 결과를 반환한다면 그 결과가 채택한 형식 의미론과 일치한다는 부분적 정확성이다. 실제 CPython과의 연결은 주로 무작위로 만든 170만 개 이상의 프로그램에서 99.95%가 같은 동작을 보였다는 경험적 시험으로 확인했다. 모든 Python 프로그램의 정답률을 수학적으로 99.95% 보장한 것은 아니다. 초기 버전에 주입한 7개 오류 중 5개는 무작위 테스트를 통과했지만 7개 모두 증명을 실패시켰다.

한계와 오해하기 쉬운 점

정형 검증은 명세가 현실과 일치하는지까지 자동으로 보장하지 않는다. CPU와 운영체제의 형식 모델, 실제 증명한 명제, Rocq 검사기와 그 기반 환경에 대한 신뢰가 남는다. 이 연구의 단일 스레드 정적 RISC-V·musl 환경은 사람들이 흔히 쓰는 x86·ARM·동적 glibc 환경과 다르다. 또 검증된 코드에서 발견되는 모든 문제가 모델의 오류인 것만도 아니다. 애초에 명세가 다루지 않은 기능이나 보안 성질일 수 있다.

증명이 다루는 범위도 제한적이다. ASan은 모든 메모리 안전 버그를 감지하지 못하며, 각 라이브러리의 모든 진입점을 검증한 것도 아니다. 모든 진입점을 검증하더라도 죽은 코드(dead code)가 있다면 전체 라이브러리가 커버되지 않을 수 있다. 또한 실제 프로그램이 라이브러리를 오용하면 호출자(caller)에서 메모리 손상이 발생할 수 있다. 이 격차를 메우려면 각 공개 함수에 대해 호출자가 지켜야 할 사항을 명시하고 호출자가 이를 엄격히 준수해야 한다.

비용 실험은 실제 239개 진입점 전체와 구별해야 한다. 별도로 줄인 36개 과제에서는 입력을 64바이트로 제한하고 작은 검사 런타임을 썼다. 각 과제에 독립 단일 에이전트 시도 3개를 주고 각각 500만 토큰까지 허용했으며 첫 성공을 기준으로 집계했다. 이 조건에서 Opus 5.5는 Opus 5보다 약 40% 적은 토큰으로 과제 절반을 해결했다. 공유 작업공간에서 증명을 재사용하는 비교는 약 17%의 토큰 감소를 보고했다. 두 수치를 더하거나 실제 운영 전체의 비용 절감률로 일반화할 수 없다.

실제로 어떻게 활용할까

개발자가 적용할 때는 먼저 실패하면 안 되는 성질과 실행 환경을 좁혀 정하는 것이 출발점이다. 기존 코드를 다른 언어로 전부 다시 쓰지 않고 바이너리 수준에서 접근할 수 있어, 여러 서비스가 공통으로 쓰는 의존성을 우선 검증하는 전략이 가능하다. Theorem이 제시한 Nix 생태계 로드맵에는 glibc·OpenSSL·cURL 같은 기반 소프트웨어가 포함되지만, 이는 앞으로의 계획이지 이번에 그 생태계 전체의 검증을 마쳤다는 뜻은 아니다.

증명 재사용은 같은 기반 코드를 매번 처음부터 증명하는 비용을 줄이는 방향이다. 실제 OSS-Fuzz 작업에서도 C 런타임과 ASan 초기화처럼 여러 프로그램에 공통인 부분의 증명이 겹쳤다. 다만 부록의 전문가 평가는 AI 증명이 반복적이고 장황하며, 더 큰 프로그램으로 확장하려면 사람이 쓰는 모듈화와 추상화가 필요할 수 있다고 지적한다. 단순히 더 많은 토큰을 넣으면 언제나 해결된다는 결론은 아니다.

Theorem은 다른 오픈소스 프로젝트에 같은 파이프라인을 적용하는 지원과 개발용 Claude 스킬을 소개했다. 연구팀은 형식 모델과 공개 가능한 증명도 내놓았지만, 패치가 필요 없었던 테스트의 증명 등 일부만 공개했다. 아직 고치지 않은 취약점을 드러낼 수 있는 증명은 공개하지 않았다. 따라서 독자는 공개 자료의 조건과 명세부터 확인해야 하며, 이 해설이 전체 증명 코드를 독립적으로 실행·검증한 것은 아니다.