Boris Cherny의 Claude 형식 검증, proof-skills·agent-formal-verify 활용

출발점은 Boris Cherny의 2026년 9월 22일 X 게시물이다. 그는 Claude로 Claude Agent SDK를 Lean으로 형식 검증해 버그와 경쟁 상태를 고쳤다고 보고했고, TLA+도 함께 활용한다고 설명했다. 후속 설명에서 밝힌 흐름은 복잡한 상태 머신이나 경쟁 상태가 생기기 쉬운 부분을 모델로 만들고, 모델에서 찾은 반례를 실제 코드에서 재현한 뒤 수정하는 것이다. 전체 코드베이스의 정확성을 증명했다는 뜻은 아니라고도 덧붙였다.

목차

Boris Cherny 사례에서 나온 커뮤니티 스킬

이 사례를 참조해 Opum AI가 공개한 proof-skills와 Michael Denyer가 공개한 agent-formal-verify는 별도의 커뮤니티 프로젝트다. 두 스킬은 Anthropic 공식 도구가 아니며, 2026년 10월 22일 발표된 Anthropic·Theorem의 형식 검증 연구를 오픈소스화한 것도 아니다. 두 저장소는 각각 9월 25일과 10월 1일에 첫 공개 커밋이 올라와, 그 연구보다 앞선다.

이 글은 2026년 10월 28일에 내려받은 두 저장소의 README와 스킬 문서를 대조해 정리했다. 직접 설치하거나 검증을 실행한 후기나 성능 비교는 아니다. Cherny의 사례를 그대로 재현한다고 보장하는 것도 아니다. 설치 조건과 검증 범위, 결과를 받아들이는 기준에 초점을 맞췄다.

두 스킬은 무엇이 다른가?

지원하는 호스트, 스킬 구성, 실제 코드를 검사하는 수단이 다르다. Claude Code를 쓴다면 두 저장소를 모두 검토할 수 있고, Codex나 Pi를 쓴다면 agent-formal-verify가 대상이다.[1][8]

모바일에서는 표를 좌우로 밀어 마지막 열까지 확인할 수 있다.

proof-skills는 formal-verify가 진입점이고 나머지 세 스킬이 도구별 작업을 맡는다. tlaplus-model은 TLA+ 모델링과 TLC 검사를 맡는다. lean-model은 Lean 4 모델링, proof-simplify는 증명된 사실을 근거로 불필요한 코드를 덜어내는 단순화 담당이다. 문서에 정리된 워크플로는 여덟 가지다. 버그 탐색, PR 레이스 리뷰, 설계 검증, 증명 기반 단순화, CI 회귀 방지, 스펙과 코드의 드리프트 점검, TLA+에서 Lean으로의 확대, TLC 트레이스 설명이다.[1][3][4][5][6]

agent-formal-verify는 TLA+/TLC로 스레드 실행 순서와 종료, 자원 소유권을 모델링하고, Lean 4로 산술·범위·순차 상태 전이를 증명한다. Kani는 입력과 반복 한계를 정한 Rust 함수를 실제 코드 그대로 검사한다.[8] 여러 호스트에서 함께 쓰거나 Rust 함수를 직접 검사해야 할 때 살펴볼 만하다. 어느 쪽이 더 빠르거나 버그를 더 많이 찾는지는 이 자료로 판단할 수 없다.

proof-skills 설치와 시작: 플러그인과 도구 준비는 별개

proof-skills는 Claude Code 안에서 플러그인을 설치하고, 검사 도구는 별도 스크립트로 준비한다. 플러그인을 설치한 것과 검사 도구가 준비된 것은 다른 상태다.[1]

플러그인 설치

Claude Code 안에서 다음 두 명령을 순서대로 입력한다.

/plugin marketplace add opum-ai/opum-marketplace
/plugin install proof-skills@opum

이미 opum marketplace를 추가해 둔 상태라면 add 명령은 아무 일도 하지 않는다. 이 경우 설치 전에 /plugin marketplace update opum으로 갱신하라고 README가 안내한다.

검사 도구 준비

도구는 README의 아래 명령으로 준비한다. 캐시 경로에서 스킬 디렉터리를 고르고, 설치 상태 확인(doctor)과 TLA+·Lean 설치 스크립트를 차례로 실행한다. 한 줄이 긴 명령은 코드 블록을 좌우로 밀어서 볼 수 있다.[1]

S=$(ls -d ~/.claude/plugins/cache/opum/proof-skills/*/skills | tail -1)
$S/formal-verify/scripts/doctor.sh
$S/tlaplus-model/scripts/setup_tla.sh --with-jre
$S/lean-model/scripts/setup_lean.sh

doctor.sh는 설치된 도구를 보여 주고, setup_tla.sh는 TLA+ 도구를, setup_lean.sh는 Lean 설치 관리자 elan을 준비한다. --with-jre는 Java가 없을 때 쓸 휴대용 JRE까지 함께 설치하는 옵션이다.[1][2]

문서상 curl, bash, Python 3.9+, git이 필요하고 약 1GB의 여유 공간이 있어야 한다. 도구는 사용자 디렉터리인 ~/.cache/proof-skills와 ~/.elan에 설치되며 sudo는 필요하지 않다고 안내한다. Quint와 Apalache는 선택 사항이다.[1][2]

시작하기

준비가 끝나면 Claude Code에서 /proof-skills:formal-verify로 시작한다. 동시성이나 상태 버그를 설명하면 스킬이 자동으로 작동할 수도 있다고 README가 안내한다.[1]

처음부터 저장소 전체의 정확성을 묻기보다 위험한 관심사 하나를 정하는 흐름이다. 어떤 상태에서 무엇을 금지할지 먼저 고정하고, 모델의 상태와 전이가 어느 소스에 대응하는지 확인한다.[3]

agent-formal-verify 설치와 시작: Claude Code·Codex·Pi

호스트별 설치 명령은 다르지만, 설치한 뒤 setup을 먼저 실행하고 검증 스킬을 호출하는 순서는 같다.[8]

Claude Code

Claude Code 안에서 다음 명령을 입력한다.

/plugin marketplace add michael-denyer/agent-formal-verify
/plugin install agent-formal-verify@agent-formal-verify

이후 /agent-formal-verify:setup을 한 번 실행하고, 준비가 끝나면 /agent-formal-verify:formal-verify를 호출한다. 이 스킬은 Claude Code 전용이 아니므로 Claude Code에서도 선택할 수 있다.[8][9]

Codex

Codex는 터미널에서 설치한다.

codex plugin marketplace add michael-denyer/agent-formal-verify
codex plugin add agent-formal-verify@agent-formal-verify

설치한 뒤 플러그인의 setup 스킬을 이름으로 요청한다. 검증은 $formal-verify를 입력하거나 formal-verify 스킬을 이름으로 요청하면 된다. Codex 전용 slash command는 제공하지 않으므로 다른 호스트의 호출 구문을 그대로 옮기지 않는다.[8][9]

Pi

Pi도 터미널에서 설치한다.

pi install git:github.com/michael-denyer/agent-formal-verify

설치한 뒤 Pi 안에서 /skill:setup을 먼저 실행하고 /skill:formal-verify로 검증을 시작한다.[8][9]

setup 스킬과 도구 helper의 역할

agent-formal-verify의 setup은 대상 저장소 없이 공유 도구를 준비한다. 다만 모든 도구를 helper가 자동으로 내려받는다는 뜻은 아니다. 대상은 Java/JDK, Python, SHA256 도구, TLC, elan/Lean, Rust/Kani다. 이미 설치된 것은 재사용하고, 설치는 사용자가 허용한 범위를 따른다.[8][10][11]

• TLC: setup 스킬은 설치가 허용된 범위에서 지정된 TLA+ 릴리스(v1.7.4)의 JAR를 확보해 캐시에 저장하도록 에이전트에 지시한다. helper 스크립트 자체는 JAR를 내려받지 않고 SHA256 해시를 검사한다.
• Lean: setup helper가 필요한 버전(pin)을 elan으로 설치할 수 있다.
• Kani: 문서에 고정된 버전(0.68.0)을 Cargo로 설치한 뒤 cargo kani setup을 실행한다. 플러그인의 Kani helper는 확인만 하고 설치하지 않는다.

도입 체크리스트에는 플러그인 등록과 도구 준비를 따로 적어 두면 된다. 도구를 실행할 수 없다는 뜻의 UNAVAILABLE은 통과가 아니라 미검사다. 결과에 성공 표시가 있는지만 볼 것이 아니라 어떤 검사가 실제로 실행됐는지부터 확인해야 한다.[11]

검증을 맡길 때 확인할 것

검사할 속성, 모델과 소스의 대응, 반례가 실제로 일어날 수 있는지를 함께 봐야 한다. 마지막 통과 문구만으로는 무엇을 확인했는지 알 수 없다.

proof-skills는 관심사와 속성을 고정한 뒤 모델/소스 대응표를 만들고, 모델 검사에서 나온 반례를 실제 코드에서 재현하는 흐름이다. 수정을 적용한 모델에서는 통과하고 수정을 뺀 모델에서는 실패하는지, 도달성을 확인하는 설정이 의도대로 실패하는지도 살핀다. 실제 코드에서 재현하지 못한 반례는 확정 버그가 아니라 의심으로 취급한다.[1][3]

agent-formal-verify도 모델이나 Rust 검사 코드(harness)를 만든 뒤 소스 위치와 실제 설정에서의 도달성을 대조하고, 가능하면 재현한다. 반례가 나왔다고 모두 실제 버그는 아니다. 그래서 반례마다 다음 세 가지 표기 중 하나를 붙인다. 이 구분을 지우고 모두 실제 버그로 세면 안 된다.[12]

• reproduced: 같은 조건에서 재현되는 테스트나 레이스 감지 도구가 실제 코드에서 실패한다.
• reachable at shipped settings: 배포 설정과 호출자가 반례를 허용하지만, 실제 코드에서 재현해 확인하지는 않았다.
• model-only: 반례가 나오려면 배포된 코드가 쓰지 않는 설정이나 호출자가 필요하다.

결함 주입 검사(mutation)는 두 저장소 문서에 모두 나온다. 의도적으로 결함을 넣은 복사본이 검사에 걸리는지 확인해, 통과 여부와 함께 검사 자체가 결함을 구별할 수 있는지를 본다. Lean 증명은 미완성 증명(sorry)과 표준 범위를 벗어난 공리를 점검하는 절차가 두 저장소에 모두 있다.[1][3][5][12]

결과를 남기고 코드를 고치는 방식

proof-skills는 증거 파일과 HTML 보고서가 중심이고, agent-formal-verify는 모델 파일과 프로젝트 문서, PR에 사실별로 기록할 위치를 정해 둔다.

proof-skills는 formal/findings.json과 범위·대응표·재현·증거 파일, HTML Artifact 보고서를 남긴다. 확인된 버그마다 재현을 만들고 수정과 재검증까지 흐름에 포함하며, 재현은 기본적으로 기존 테스트 옆의 회귀 테스트가 된다. Artifact 도구가 없으면 로컬 HTML로 저장하고 그 사실을 알린다.[1][3]

agent-formal-verify는 버그마다 보고서 파일을 따로 만들지 않는다. 모델 파일 머리 주석, mutation 파일, 프로젝트의 테스트 문서(있는 경우), PR 설명이 각각 기록 위치다. 코드 수정은 사용자가 요청했을 때만 하고, 커밋과 PR도 요청받았을 때만 만든다. CI는 요청이 있거나 저장소가 이미 모델을 CI에서 돌리고 있을 때만 추가한다.[12]

검증 요청이 곧 코드 수정과 PR 생성에 대한 허용은 아니다. 수정과 PR 생성의 허용 범위는 팀 규칙에 따로 적어 둘 만하다.

무엇을 고르고 어디까지 믿어야 하나?

Claude Code에서 단순화·HTML 보고서를 포함한 네 스킬이 필요하면 proof-skills를 검토할 만하다. 여러 호스트에서 함께 쓰거나 범위를 제한한 Rust 함수를 검사하려면 agent-formal-verify가 후보가 된다. 문서 구성에 따른 선택이지 실측 순위는 아니다.

라이선스도 MIT와 GPL-3.0-only로 다르므로 회사 정책에 맞는지 도입 전에 확인해야 한다. 이 글은 라이선스를 법적으로 해석하지 않는다.[7][13] 두 저장소 모두 버전이 아직 0.x대(proof-skills v0.1.1, agent-formal-verify v0.3.5)다. 도입 전에 최신 README를 다시 확인하는 편이 안전하다.[1][8]

어느 쪽도 전체 프로그램의 정확성을 보장하지 않는다. TLC는 명시한 작은 규모의 모델에서 실행 순서를 탐색한다. Lean은 명시한 가정 아래에서 모든 크기에 성립하는 속성을 증명할 수도 있다. 둘을 똑같이 제한된 입력만 검사하는 도구로 보면 안 된다. 다만 TLA+/Lean 모델은 코드 동작을 옮겨 만든 것이므로, 빠진 상태 전이나 잘못된 가정이 있으면 실제 코드에 적용할 수 있는 결론도 달라진다. Kani 역시 명시한 입력·반복 범위 밖까지 보장하지 않는다. 결과를 읽을 때는 모델과 실제 운영 설정의 차이를 함께 확인해야 한다.[8][12]

소스 반출도 도입 전에 확인할 조건이다. agent-formal-verify는 MCP 서버와 hook을 설정하지 않고 자체 telemetry나 자격증명 요구가 없다고 README에 밝힌다. 그렇더라도 에이전트가 고른 소스 발췌와 모델, 결과는 에이전트의 모델 제공자에게 전달된다. 완전 로컬 실행이나 외부 전송 없음으로 받아들이면 안 된다. proof-skills를 쓸 때도 호스트 에이전트의 전송 범위와 회사의 소스 반출 정책을 별도로 확인해야 한다.[8]

정리: 도입 전에 정해 둘 것

• 검사할 위험한 동작 하나와 지켜야 할 속성
• 플러그인 등록과 도구 준비를 따로 확인했는지
• 실제로 실행된 검사와 UNAVAILABLE로 남은 검사의 구분
• 반례의 상태(reproduced, reachable at shipped settings, model-only)와 수정 전후 검사 결과
• 코드 수정·커밋·PR을 어디까지 맡길지, 소스를 어디까지 모델 제공자에게 보낼지

처음 도입할 때는 위험한 동작 하나를 고르고, 모델과 소스 위치를 연결해 남기는 데서 시작하면 된다. 통과 문구보다 중요한 것은 어떤 가정으로 무엇을 확인했고, 무엇을 확인하지 못했는지다.

연관 글

• 🔗 OpenAI Codex Record & Replay 정리: 작업을 한 번 보여주면 Skill로 재사용하는 방식
• 🔗 Ponytail을 보고 다시 생각한 AI 코딩 설정: 게으른 시니어 개발자의 좋은 습관을 포팅하기

참고 자료