LLM으로 대규모 formal verification이 가능해졌다
LLMs are making formal software verification feasible at a much larger scale
TL;DR Highlight
Claude로 오픈소스 라이브러리 123개의 no-crash 증명을 만들고 버그도 찾았다
Who Should Read
C/C++ 라이브러리의 fuzz test를 운영하며 LLM으로 코드 정확성을 더 높이고 싶은 백엔드·보안 개발자
Core Mechanics
- fuzz test를 증명 대상 스펙으로 바꿨다
- 기존 fuzz test를 'RISC-V 컴파일 바이너리가 어떤 입력에서도 크래시하지 않는다'는 스펙으로 자동 변환했다.
- Claude가 이 스펙의 증명을 쓰고, Rocq 증명 검사기(proof checker)가 맞는지 기계적으로 확인한다.
- 123개 라이브러리, 239개 진입점을 증명했다
- 64MB 미만의 모든 입력에서 크래시하지 않음을 몇 주 만에 증명했다.
- 증명은 약 1억 8천만 줄의 Rocq이고, 증명 하나는 보통 약 60만 줄이다.
- 대상 바이너리의 중간 길이는 RISC-V 명령어 18,000개다.
- 증명 시도 자체가 버그를 찾아냈다
- Claude가 버그를 발견하면 직접 패치하고, 스펙을 다시 만든 뒤 증명을 이어 갔다.
- 약 20MB 입력에서만 터지는 카운터 언더플로 같은 버그는 fuzzer가 찾기 어려운 유형이라고 밝혔다.
- 크래시하지 않는 로직 버그도 찾았다. 파일 로드 제한 기능이 항상 적용되지는 않았다.
- 믿어야 할 것은 세 가지뿐이다
- RISC-V·Linux 프로세스의 형식 모델, 증명한 정리(theorem) 문장, Rocq 증명 검사기만 신뢰하면 된다.
- 증명 수십만 줄을 사람이 검토할 필요는 없다고 한다.
- 이 라이브러리들에 버그가 없다는 뜻은 아니고, 위 구성요소나 증명 범위 밖에 남을 수 있다.
- 증명은 단일 스레드 정적 바이너리 전제다
- 고정 메모리 예산의 RISC-V CPU와 Linux OS 위에서 실행되는 경우만 증명했다.
- 다른 아키텍처와 OS로 넓히려면 해당 의미론(semantics)을 표준화해야 한다.
- 새 모델은 토큰을 덜 쓰고 증명은 재사용된다
- 36개 검증 과제에서 Opus 5.5는 절반을 Opus 5 대비 약 40% 적은 토큰으로 증명했다.
- 에이전트끼리 증명을 복사할 수 있게 하니 혼자 할 때보다 토큰이 17% 줄었다.
- 증명에는 여전히 수억 토큰이 들 수 있다는 점을 한계로 꼽았다.
Community Reactions
- 스펙이 맞는지가 핵심이라는 의견
- 증명이 완벽해도 스펙이 잘못 모델링되면 엉뚱한 문제를 푼 것이라는 의견이 있었다.
- LLM이 증명한 내용이 내가 원한 것인지 어떻게 아느냐는 질문이 여러 번 나왔다.
- 실무에서 쓰고 있다는 경험
- 에이전트가 SIMD·CUDA로 함수를 빠르게 만든 PR에 원본과 동작이 같다는 Rocq 증명을 붙여 자신 있게 머지한다는 경험이 있었다.
- Rust로 다시 쓴 Postgres를 Rust와 C를 Lean으로 옮겨 비교했더니 코드의 약 12%(약 7만 줄 C)가 같은 동작임을 증명했고, 부동소수점 차이 같은 작은 차이만 나왔다는 경험이 있었다.
- 확장성에 회의적인 의견
- 부록에 따르면 에이전트가 장황한 증명 스타일로는 복잡도 한계에 부딪힐 수 있어, 모듈식 추상화가 필요할 수 있다는 의견이 있었다.
- ASan에 의존하는 스펙 구조가 생각보다 덜 일반적이며, 메모리 접근을 직접 모델링하면 더 단순해질지 궁금하다는 의견이 있었다.
- 검증과 검증 대상 신뢰에 대한 반론
- fuzz로 크래시를 고친 뒤 그걸 증명하는 게 무의미하지 않느냐는 반론이 있었다.
- 검증은 '제대로 만들었나', 유효성 검증은 '맞는 걸 만들었나'로 구분해야 한다는 의견이 있었다.
How to Apply
- 내 fuzz test 하나를 스펙 후보로 골라 보기
- 오늘 OSS-Fuzz나 자체 fuzz 진입점 하나를 골라 '64MB 미만 어떤 입력에도 크래시하지 않는다'로 적어 보자.
- 이 문장이 증명할 스펙이 되는지 팀과 확인하자.
- 핵심 순수 함수에 동치 증명 붙이기
- 최적화한 함수는 원본과 동작이 같다는 증명을 PR 조건으로 요구하자.
- 댓글 사례처럼 LLM이 만든 Rocq·Lean 증명을 검사기로 통과시키는 방식으로 시작하자.
- 신뢰해야 할 구성요소를 문서로 고정하기
- 정리 문장, 사용한 형식 모델, 증명 검사기를 한 문서에 적어 두자.
- 증명 전체가 아니라 이 세 가지만 리뷰 대상으로 삼자.
- Theorem의 Claude skill로 시작하기
- 공개된 skill로 자기 오픈소스 프로젝트 한 곳의 검증을 시도하자.
- 실패한 증명에서 나온 버그부터 먼저 고치자.
Try It
# Claude 또는 Claude Code에 붙여넣기 (원문 방법의 간이 버전: 실제 증명은 하지 않고 스펙 후보와 위험 경로를 점검)
아래는 내 라이브러리의 fuzz test 진입점이다.
{{fuzz_target 코드}}
이 진입점에 대해 다음을 해줘.
1. '64MB 미만의 어떤 입력에서도 크래시하지 않는다'는 스펙을 한 문장으로 쓰기
2. 이 스펙이 깨질 수 있는 경로(카운터 언더플로, 범위 밖 읽기·쓰기, 깊은 재귀 등)를 코드에서 찾아 줄 번호와 함께 나열하기
3. 각 경로가 fuzzer가 찾기 어려운 이유(큰 입력, 희귀한 호출 순서 등)를 설명하기
이어서 해 볼 것: 찾은 경로 중 하나에 대해 재현 입력이나 단위 테스트를 만들어 달라고 요청해 보세요.Terminology
관련 논문
PHP2Shell: AI가 찾아낸 PHP 코어 RCE 취약점
Wiz가 AI로 PHP 코어의 10년 묵은 RCE를 찾아 익스플로잇까지 만들었다
LLM에게 confidence 점수를 물어보면 안 되는 이유
LLM이 말한 confidence 숫자는 측정값이 아니라 그럴듯한 텍스트일 뿐이다
The Judge Can Debias Itself: LLM-as-a-Judge가 스스로 편향을 고치게 하는 법
심사 프롬프트에 편향 경고를 넣거나 스스로 비판시켰더니 21개 중 20개 조합에서 정확도가 올랐다
미국 노동시간의 90%는 AI 벤치마크가 제대로 다루지 못하는 일이다
벤치마크 29개를 직업 과제에 매핑했더니 노동시간 90%가 커버 밖
Postgres 19, AI 코드 리뷰가 버그를 너무 많이 찾아 출시 연기
LLM 코드 리뷰가 버그를 쏟아내 Postgres 19가 11월로 밀리고 기능 8~10개가 빠졌다
StarSkirmish Bench v0.2: LLM이 1시간 만에 짜는 StarCraft 봇 대결
LLM에게 1시간 동안 StarCraft 봇을 짜게 했더니 GPT-6 Astra가 1위
그럴듯한 설명 하나면 멀티모달 LLM 심사위원도 속는다 (JUPE 벤치마크)
정답은 그대로 두고 설명만 붙였더니 MLLM 심사위원의 오답 거절률이 12.7~13.8%p 떨어졌다
신경망은 이미 깔끔하다: polysemanticity의 원인 재해석
뉴런을 직접 들여다봤더니 대부분 한 가지 역할이 있었다는 주장