LLM이 훨씬 더 큰 규모의 소프트웨어 정형 검증을 가능하게 하고 있음

Anthropic 연구 글의 앞부분(요약, 도입, "테스트를 증명으로" 도입부)을 기준으로 옮겼어요. 퍼즈 테스트 이후의 세부 실험과 zlib·Python 인터프리터 사례 본문은 읽지 못했어요.

요약

대부분의 소프트웨어에는 버그가 가득하고, 이제 AI가 그걸 쉽게 찾아 악용할 수 있어요. Anthropic은 기존 방어로는 부족하고 코드에 버그가 없다는 걸 증명할 방법이 필요하다고 말해요. 정형 검증(formal verification)이 그런 보장을 줄 수 있지만 전문가가 수년을 들여야 해서 대부분 프로젝트에는 비현실적이었어요.

Anthropic은 Theorem과 협업해 이게 더는 사실이 아니라고 보여 줘요. Claude로 실제 오픈소스 라이브러리 100개 넘게(본문 기준 123개)에서 RISC-V 어셈블리 수준의 보안 속성을 증명했고, 아는 한 AI로 프로덕션 소프트웨어에 어셈블리 수준 정형 검증을 대규모로 적용한 첫 사례래요. 증명을 쓰는 동안 수조 번의 테스트 실행에도 수년간 안 잡힌 버그도 찾았어요.

왜 필요한가요

수십억 기기에 깔린 Linux 커널도 최근 1,000개 넘는 취약점이 공개됐어요. 프런티어 모델이 무해해 보이는 버그를 엮어 치명적 익스플로잇을 만드는 능력도 커지고 있어요. 정형 검증은 코드를 수학 모델로 옮겨 정해진 보안 규칙을 항상 지키는지 증명하는 방식이에요. 증명이 실패하면 그 원인이 버그의 단서가 되고, 원인을 없애며 반복하면 규칙을 어기는 버그가 없다는 증명에 이르러요.

문제는 비용이에요. seL4 운영체제 커널은 구현에 2인년, 정형 검증에 20인년이 들었어요. 그래서 Airbus 항공전자 코드처럼 정말 중요한 곳에서만 쓰였어요.

무엇을 증명했나요

일부 실행 파일이 특정 조건에서 절대 크래시하지 않는다는 걸 보였어요. 64MB 미만의 모든 입력, 모델링한 모든 Linux OS 응답과 메모리 배치에서, 메모리 안전 오류나 assertion 실패 없이 정상 종료한대요. 가정은 단일 스레드 정적 바이너리, 고정 메모리 예산, RISC-V CPU의 Linux 실행이에요. 모든 버그를 없앤 건 아니지만 훨씬 가까워졌다고 해요.

일부 증명과 RISC-V·OS 의미론을 누구나 검증·재사용하도록 공개했고, Theorem은 다른 오픈소스 프로젝트에도 같은 파이프라인을 돌려 주겠다며 Claude 스킬도 공개했어요.

테스트를 명세로

정형 검증의 큰 장애물은 "올바름"을 정의하는 명세예요. 그래서 이미 있는 테스트 스위트를 "이 테스트는 항상 통과한다"는 명세로 자동 변환했고, 먼저 퍼즈 테스트에서 시작했어요. 수만 개의 어셈블리 명령에 대한 증명은 예전엔 감당이 안 됐지만, 분명한 목표를 향해 수백만 줄을 훑는 일은 LLM에 잘 맞는대요. 모델이 똑똑해질수록 증명 비용이 내려가니, 예전에 약한 모델로 시도해 실패한 개발자도 다시 해 보라고 권해요.