zakrad/certora-prover-skill

Certora Prover (CVL / EVM)

Certora Prover는 스마트 컨트랙트를 공식 검증합니다: CVL(Certora Verification Language)로 속성(규칙 및 불변량)을 설명하는 스펙을 작성하면, Prover가 모든 입력과 상태에 대해 이를 증명하거나 구체적인 **반례(CEX)**를 반환합니다.

핵심 개념 — 먼저 읽어야 할 내용:

• 증명하라, 테스트하지 마라. 단위 테스트나 퍼징(일부 입력만 샘플링)과 달리 Prover는 모델이 허용하는 모든 입력, 호출자, 저장소 상태에 대해 기호적으로 추론합니다.
• 건전하지만 불완전합니다. 모델 내에서는 위반을 놓치지 않지만, 시간 초과가 발생할 수 있으며 스펙이 실제로 주장하는 내용만 확인합니다. 빈/약한 스펙은 유용한 것을 증명하지 못합니다.
• "검증됨" = 모델 내에서, 가정에 따라 반례 없음. 모든 require, 요약, 루프 언롤링, 낙관적 플래그는 모델을 좁힙니다. 녹색 체크 표시는 이러한 가정만큼만 강력합니다. 이를 올바르게 설정하는 것이 전체 게임입니다.

처음부터 앱 검증 워크플로우

1. 설치 + 키. pip install certora-cli; CERTORAKEY 설정. (→ references/running-and-config.md)
2. 프로젝트 레이아웃. 컨트랙트는 src/, 스펙은 certora/specs/, 대상별 .conf 파일을 배치합니다. (→ references/running-and-config.md)
3. 첫 번째 기초/파라메트릭 규칙 작성. 아주 작게 시작하세요: 모든 함수 이후에 기본 속성이 유지됨을 주장하는 파라메트릭 규칙(method f)을 작성하여 하네스가 컴파일되고 실행되는지 확인합니다. (→ references/rules-invariants.md, references/spec-patterns-cookbook.md)
4. 실행. certoraRun MyContract.conf (또는 .sol/.spec을 직접 전달) 실행 후 보고서 링크를 엽니다. (→ references/running-and-config.md)
5. 보고서 읽기. CEX 호출 추적 및 저장소를 검사합니다. 스펙을 수정하거나 실제 버그를 확인합니다. (→ references/running-and-config.md, references/debugging-and-timeouts.md)
6. 불변량 + 고스트 추가. 실제 속성을 명시합니다: 유도 불변량과 회계를 위한 고스트/후크(예: sumOfBalances == totalSupply). (→ references/rules-invariants.md, references/hooks-and-ghosts.md)
7. 건전성 + 기초 검증 강화. 항상 --rule_sanity basic을 실행하고, 모든 요약과 가정을 검토하며, 건전하지 않은 단축키를 제거하거나 정당화합니다. (→ references/soundness-and-approximations.md, references/methods-and-summaries.md)
8. 돌연변이 테스트. Gambit을 사용하여 규칙이 실제로 주입된 버그를 잡아내는지 확인합니다. 돌연변이를 살아남는 스펙은 과도하게 가정하고 있는 것입니다. (→ references/debugging-and-timeouts.md)

10초 퀵스타트

pip install certora-cli
export CERTORAKEY=<your-key>

// Counter.spec — increment()가 값을 엄격히 증가시킴을 증명
methods {
    function get() external returns (uint256) envfree;
}

rule incrementIncreases(env e) {
    uint256 before = get();
    increment(e);
    assert get() > before, "increment must increase the counter";
}

certoraRun src/Counter.sol:Counter \
    --verify Counter:certora/specs/Counter.spec \
    --solc solc8.20 \
    --rule_sanity basic \
    --msg "counter increment"

이 스킬 사용법 / 참조 맵

현재 작업과 일치하는 파일을 읽으세요:

• references/cvl-language.md — 읽어야 할 때: CVL 구문이 필요할 때: 파일 구조, 타입(mathint/env/method/calldataarg/storage), 캐스트 및 건전성, 연산자/수량자, require vs assert vs satisfy vs havoc, 함수 vs 정의, 컨트랙트 메서드 호출 방법(env, envfree, withrevert, lastReverted).
• references/rules-invariants.md — 읽어야 할 때: 규칙, 파라메트릭 규칙(method f), satisfy 증인, preserved 블록과 requireInvariant를 사용한 유도 불변량을 작성할 때.
• references/methods-and-summaries.md — 읽어야 할 때: methods 블록을 설정할 때: 진입 종류, envfree/optional, 전체 요약 카탈로그 + 건전성 테이블, 표현식/고스트 요약, 다중 컨트랙트 설정(using, links, DISPATCHER).
• references/hooks-and-ghosts.md — 읽어야 할 때: 저장소를 미러링하거나 회계를 증명해야 할 때: 저장소/연산코드/일시적 후크, 고스트 변수/함수, 합계 고스트, persistent 고스트.
• references/running-and-config.md — 읽어야 할 때: 설치, certoraRun 실행, .conf 파일 작성, 플래그 선택, 프로젝트 레이아웃 설정, 웹 보고서 해석할 때.
• references/spec-patterns-cookbook.md — 읽어야 할 때: 바로 사용할 수 있는 레시피가 필요할 때: 접근 제어, "무엇이 바뀔 수 있는가", 잔액 합계, 단조성, 프레임 조건, 상태 머신, 왕복, 교환 법칙, 복귀 조건, 단위 테스트 스타일 규칙.
• references/advanced-defi-patterns.md — 읽어야 할 때: 실제 프로토콜을 검증하고 기본 요리책이 충분하지 않을 때: ERC4626 금고 환율 단조성(교차 곱셈, 무료 점심 없음, 미리보기 경계), AMM k-불변량 및 가치 추출 방지, 대출 지급능력/건전성/"나쁜 부채 없음" 및 잠금 방지 활성성, 보상 드리프트 회계, 재진입-as-CEI, 대규모 역할 기반 접근 제어 — 각 관용구는 출처가 되는 프로덕션 저장소(Morpho/OZ/Aave/Certora)에 귀속됩니다.
• references/tooling-and-ecosystem.md — 읽어야 할 때: Certora를 CI(GitHub Actions, 캐싱, PR 게이팅)에 연결하거나 속성에 맞는 도구를 결정할 때: Certora vs Halmos vs Foundry(불변량/퍼즈) vs Echidna 결정 가이드 및 각 도구의 장단점.
• references/learning-resources.md — 읽어야 할 때: 더 깊이 배우거나 온보딩할 때: 엄선된 외부 링크 — RareSkills/Certora 튜토리얼, 공식 문서, 강연, 실제 공개 스펙 저장소(Morpho, Aave, OpenZeppelin, Compound)로 작업 예제.
• references/soundness-and-approximations.md — 읽어야 할 때: 무엇을 가정하고 주장할지 결정할 때: 건전/비관적 vs 불건전/낙관적, 루프/해싱/혼란 근사, 낙관적 플래그 패밀리, 통과 규칙이 보장하는 것, 건전성 검토 체크리스트.
• references/debugging-and-timeouts.md — 읽어야 할 때: 규칙이 공허하거나, 느리거나, 의심스러울 때: --rule_sanity, 시간 초과 완화(요약, 분할, 범위 제약), TAC 난이도 보고서, Gambit 돌연변이 테스트, VSCode LSP, "이 통과를 신뢰해야 할까?" 체크리스트.
• cheatsheet.md — 읽어야 할 때: 한 페이지 빠른 참조가 필요할 때: 가장 많이 사용되는 CVL 키워드, 규칙/불변량 골격, 일반적인 certoraRun 플래그, 주요 함정.
• examples/ERC20.spec — 읽어야 할 때: 완전한 작업 스펙이 필요할 때: methods 블록, 잔액 합계 고스트+후크, 공급 불변량, 파라메트릭/무결성/복귀/가산성 규칙, 민트 접근 제어.
• examples/ERC20.conf — 읽어야 할 때: 모든 일반 키(files, verify, solc, packages, optimistic_loop, rule_sanity, ...)를 포함하는 실행 가능한 JSON5 conf 템플릿이 필요할 때.

황금률 / 일반적인 함정

• require ≠ 복귀(revert). require는 사실을 가정합니다(모델을 가지치기합니다). 컨트랙트 복귀를 확인하지 않습니다. 복귀에 대해 추론하려면 withrevert + lastReverted를 사용하세요.
• 공허성( vacuity) 주의. 과도하게 제약된 require는 입력이 살아남지 못해 규칙이 사소하게 통과되게 만들 수 있습니다. 항상 --rule_sanity basic을 실행하세요(advanced 권장).
• 낙관적 플래그는 건전하지 않습니다. --optimistic_loop, --optimistic_hashing, --optimistic_fallback 등은 경우를 가정하여 제거합니다. 의도적으로 사용하고, 이유를 문서화하며, 필요성을 제거하는 것을 선호하세요.
• filtered보다 preserved를 선호하세요. 불변량의 경우, 메서드를 조용히 제외하는 대신 preserved 블록( requireInvariant 포함)에서 가정을 인코딩하세요.
• 누산기에는 mathint를 사용하세요. uint256의 합계와 카운터는 오버플로되어 가짜 CEX를 생성하거나 실제 CEX를 숨길 수 있습니다. 무제한 mathint로 계산하고 경계에서 캐스트하세요.
• 통과하는 규칙은 가정만큼만 좋습니다. 모든 요약, 링크, 루프 경계, require는 증명의 구멍입니다. 돌연변이 테스트를 통해 규칙이 실제로 실패할 수 있는지 확인하세요.

---

가장 많이 사용되는 파일: 적절한 레시피를 위해 references/spec-patterns-cookbook.md에서 시작하고, 전체 작업 스펙을 위해 examples/ERC20.spec을 참조하세요.