zakrad/certora-prover-skill

Certora Prover (CVL / EVM)

O Certora Prover verifica formalmente contratos inteligentes: você escreve especificações em CVL (Certora Verification Language) descrevendo propriedades (regras e invariantes), e o Prover as prova para todas as entradas e estados ou retorna um contraexemplo concreto (CEX).

Modelo mental central — leia isto primeiro:

• Prove, não teste. Diferente de testes unitários ou fuzzing (que amostram algumas entradas), o Prover raciocina simbolicamente sobre todas as entradas, chamadores e estados de armazenamento permitidos pelo seu modelo.
• Sólido mas incompleto. Dentro do modelo não perderá uma violação, mas pode exceder o tempo limite, e verifica apenas o que sua especificação realmente afirma. Uma especificação vazia/fraca não prova nada útil.
• "Verificado" = nenhum contraexemplo dentro do modelo, módulo suas suposições. Cada require, sumário, expansão de loop e sinalizador otimista restringe o modelo. Uma marca de verificação verde é tão forte quanto essas suposições — acertá-las é o jogo todo.

Fluxo de trabalho: verificando um aplicativo do zero

1. Instalação + chave. pip install certora-cli; defina CERTORAKEY. (→ references/running-and-config.md)
2. Estrutura do projeto. Coloque contratos em src/, especificações em certora/specs/, um .conf por alvo. (→ references/running-and-config.md)
3. Escreva uma primeira regra sanitária/paramétrica. Comece pequeno: uma regra paramétrica (method f) afirmando que alguma propriedade básica se mantém após qualquer função, apenas para confirmar que o harness compila e executa. (→ references/rules-invariants.md, references/spec-patterns-cookbook.md)
4. Execute-a. certoraRun MyContract.conf (ou passe o .sol/.spec diretamente), depois abra o link do relatório. (→ references/running-and-config.md)
5. Leia o relatório. Inspecione rastros de chamada CEX e armazenamento; corrija a especificação ou confirme um bug real. (→ references/running-and-config.md, references/debugging-and-timeouts.md)
6. Adicione invariantes + fantasmas. Declare as propriedades reais: invariantes indutivas, além de fantasmas/hooks para contabilidade (ex: sumOfBalances == totalSupply). (→ references/rules-invariants.md, references/hooks-and-ghosts.md)
7. Endureça a solidez + saneamento. Sempre execute --rule_sanity basic; revise cada sumário e suposição; remova ou justifique qualquer atalho insólito. (→ references/soundness-and-approximations.md, references/methods-and-summaries.md)
8. Teste de mutação. Use Gambit para confirmar que suas regras realmente capturam bugs injetados — uma especificação que sobrevive a mutantes está assumindo demais. (→ references/debugging-and-timeouts.md)

INÍCIO RÁPIDO de 10 segundos

pip install certora-cli
export CERTORAKEY=<sua-chave>

// Counter.spec — prove que increment() aumenta estritamente o valor
methods {
    function get() external returns (uint256) envfree;
}

rule incrementIncreases(env e) {
    uint256 before = get();
    increment(e);
    assert get() > before, "increment deve aumentar o contador";
}

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

Como usar esta habilidade / mapa de referência

Leia o arquivo que corresponde à tarefa à sua frente:

• references/cvl-language.md — leia quando precisar de sintaxe CVL: estrutura de arquivo, tipos (mathint/env/method/calldataarg/storage), casts e sua solidez, operadores/quantificadores, require vs assert vs satisfy vs havoc, funções vs definições, e como chamar métodos de contrato (env, envfree, withrevert, lastReverted).
• references/rules-invariants.md — leia quando escrever regras, regras paramétricas (method f), testemunhas satisfy, ou invariantes indutivas com blocos preserved e requireInvariant.
• references/methods-and-summaries.md — leia quando configurar o bloco methods: tipos de entrada, envfree/optional, o catálogo completo de sumários + tabela de solidez, sumários de expressão/fantasma e configurações multi-contrato (using, links, DISPATCHER).
• references/hooks-and-ghosts.md — leia quando precisar espelhar armazenamento ou provar contabilidade: hooks de armazenamento/opcode/transiente, variáveis/funções fantasma, sum fantasmas e fantasmas persistent.
• references/running-and-config.md — leia quando instalar, executar certoraRun, escrever arquivos .conf, escolher sinalizadores, estruturar um projeto ou interpretar o relatório web.
• references/spec-patterns-cookbook.md — leia quando quiser uma receita pronta: controle de acesso, "o que pode mudar", soma-de-saldos, monotonicidade, condições de quadro, máquinas de estado, ida-e-volta, comutatividade, condições de reversão e regras estilo teste unitário.
• references/advanced-defi-patterns.md — leia quando verificar um protocolo real e o cookbook básico não for suficiente: monotonicidade da taxa de câmbio do vault ERC4626 (multiplicação cruzada, sem-almoço-grátis, limites de preview), k-invariante AMM e sem-extração-de-valor, solvência/saúde/sem-dívida-inadimplente de empréstimos & vivacidade anti-bloqueio, contabilidade de drift de recompensas, reentrância-como-CEI e controle de acesso baseado em papéis em escala — cada idioma atribuído ao repositório de produção (Morpho/OZ/Aave/Certora) de onde vem.
• references/tooling-and-ecosystem.md — leia quando integrar Certora ao CI (GitHub Actions, caching, gating PRs) ou decidir qual ferramenta se adequa a uma propriedade: um guia de decisão Certora vs Halmos vs Foundry (invariant/fuzz) vs Echidna, com trade-offs de quando usar cada uma.
• references/learning-resources.md — leia quando quiser se aprofundar ou integrar: links externos curados — tutoriais RareSkills/Certora, documentação oficial, palestras e repositórios públicos de especificações reais (Morpho, Aave, OpenZeppelin, Compound) que valem a pena ler como exemplos trabalhados.
• references/soundness-and-approximations.md — leia quando decidir o que assumir vs afirmar: sólido/pessimista vs insólido/otimista, aproximações de loop/hashing/havoc, a família de sinalizadores otimistas, o que uma regra aprovada garante e a lista de verificação de revisão de solidez.
• references/debugging-and-timeouts.md — leia quando uma regra estiver vazia, lenta ou suspeita: --rule_sanity, mitigação de tempo limite (sumários, divisão, restrições de intervalo), o relatório de dificuldade TAC, teste de mutação Gambit, o LSP do VSCode e a lista de verificação "devo confiar nesta aprovação?".
• cheatsheet.md — leia quando quiser uma referência rápida de uma página: as palavras-chave CVL mais usadas, esqueletos de regra/invariante, sinalizadores comuns certoraRun e as principais armadilhas à primeira vista.
• examples/ERC20.spec — leia quando quiser uma especificação completa: bloco methods, fantasma+soma-de-saldos, invariante de fornecimento, regras paramétricas/integridade/reversão/aditividade e controle de acesso de mint.
• examples/ERC20.conf — leia quando precisar de um modelo de conf JSON5 executável cobrindo todas as chaves comuns (files, verify, solc, packages, optimistic_loop, rule_sanity, ...).

Regras de ouro / armadilhas comuns

• require ≠ reverter. require assume um fato (poda o modelo); não verifica uma reversão de contrato. Para raciocinar sobre reversões use withrevert + lastReverted.
• Cuidado com vacuidade. Um require super-restrito pode fazer uma regra passar trivialmente porque nenhuma entrada sobrevive. Sempre execute --rule_sanity basic (prefira advanced).
• Sinalizadores otimistas são insólidos. --optimistic_loop, --optimistic_hashing, --optimistic_fallback, etc. assumem a ausência de casos. Use-os deliberadamente, documente o motivo e prefira eliminar a necessidade.
• Prefira preserved a filtered. Para invariantes, codifique suposições em blocos preserved (com requireInvariant) em vez de silenciosamente excluir métodos.
• Use mathint para acumuladores. Somas e contadores em uint256 podem transbordar e produzir CEXs fantasmas (ou esconder os reais); calcule em mathint sem limites, converta na fronteira.
• Uma regra aprovada é tão forte quanto suas suposições. Cada sumário, link, limite de loop e require é um buraco na prova. Teste com mutação para confirmar que a regra pode realmente falhar.

---

Arquivos mais usados: comece por references/spec-patterns-cookbook.md para a receita certa e examples/ERC20.spec para uma especificação completa e adaptável.