Harnessing Code Agents for Automatic Software Verification

초보자용 해설

이 논문은 AI가 수학 증명처럼 엄격한 소프트웨어 검증(Coq, Lean)을 '완전 자동'으로 할 수 있음을 보여줍니다. 기존엔 전문가가 일일이 증명 전략을 짜야 했지만, Claude Code 같은 범용 코드 에이전트에게 '이 렘마 증명해줘'라고만 맡기고, 검증 하네스(자동 채점기)가 통과할 때까지 피드백 루프를 돌리면 됩니다. 그 결과, 동시성/메모리 검증의 표준인 Iris 라이브러리 4,257개 렘마, Rust 표준 라이브러리 검증 217개, 기존 LLM 증명기가 8분의 1만 풀던 reglang 318개, Lean 4로 포팅 중인 iris-lean 72개를 모두 100% 자동으로 증명했습니다. 전문가 개입 제로, 실패 제로.

실무자 관점 요약

Aria라는 검증 하네스 + 범용 코드 에이전트(Claude Code) 조합으로 interactive theorem proving(ITP)의 병목인 '증명 엔지니어링'을 완전 자동화. 핵심은 인간 설계 전략(tactic prediction, divide-and-conquer 등)을 강제하지 않고, 에이전트가 자유롭게 증명 스크립트를 작성하게 하되, 커널 체크·완전성·종료성을 하네스가 강제하는 피드백 루프만 제공한다는 점. Coq(Iris, reglang)과 Lean 4(iris-lean) 양쪽에서 SOTA 대비 압도적 커버리지 달성. LLM이 formal verification의 '코딩 에이전트'로서 실용적 임계점을 넘었음을 입증.

왜 지금 봐야 하나요?

지금까지 'LLM으로 Coq 증명 자동화'는 틈새 연구였음. 이 논문은 범용 코드 에이전트(이미 개발자가 쓰는 도구) + 얇은 하네스만으로 실무 규모 검증 라이브러리 전체를 커버함을 보임. 즉, '정형 검증의 대중화'가 LLM 에이전트 시대와 맞물려 지금 일어나고 있음. Rust, 동시성, 메모리 안전성 검증이 필요한 모든 시스템 소프트웨어 팀이 당장 도입 검토해야 할 시점.

직접 구현해볼 아이디어

작은 Lean 4/Coq 프로젝트(예: 정렬 알고리즘 정확성 증명, 간단한 상태 머신 불변식)에 대해 Claude Code + 커스텀 하네스(빌드 실패 시 에러 메시지 파싱→재시도 루프) 구성해보기. 50~100줄 렘마 단위로 '자동 증명 파이프라인' 미니 버전 구현

서비스 아이디어로 바꾸면

VeriAgent: 개발자가 Rust/Go/C++ 코드에 주석으로 스펙(전조건/후조건/불변식)만 적으면, 백엔드에서 Iris/Lean/Coq로 변환→코드 에이전트가 자동 증명→검증 리포트(증명된 것/실패한 것/수동 필요 것) 반환하는 SaaS. '정형 검증 CI/CD 플러그인'으로 GitHub Actions/GitLab CI 연동 제공. 초기 타겟: 메모리 안전성·동시성 버그 비용이 큰 임베디드, 블록체인, 커널 모듈 팀