zakrad/certora-prover-skill

Certora Prover (CVL / EVM)

El Certora Prover verifica formalmente contratos inteligentes: escribes especificaciones en CVL (Certora Verification Language) describiendo propiedades (reglas e invariantes), y el Prover las prueba para todos los estados y entradas, o devuelve un contraejemplo (CEX) concreto.

Modelo mental clave — léelo primero:

• Demuestra, no pruebes. A diferencia de las pruebas unitarias o el fuzzing (que muestrean pocas entradas), el Prover razona simbólicamente sobre cada entrada, llamante y estado de almacenamiento permitido por tu modelo.
• Sólido pero incompleto. Dentro del modelo no omitirá una violación, pero puede agotar el tiempo de ejecución, y solo verifica lo que tu especificación realmente afirma. Una especificación vacía/débil no prueba nada útil.
• "Verificado" = ningún contraejemplo dentro del modelo, según tus suposiciones. Cada require, resumen, desenrollado de bucle y marcador optimista reduce el modelo. Una marca verde es tan fuerte como esas suposiciones — lograrlas correctamente es todo el juego.

Flujo de trabajo: verificar una aplicación desde cero

1. Instalación + clave. pip install certora-cli; establece CERTORAKEY. (→ references/running-and-config.md)
2. Estructura del proyecto. Coloca los contratos en src/, las especificaciones en certora/specs/, un archivo .conf por objetivo. (→ references/running-and-config.md)
3. Escribe una primera regla de cordura/paramétrica. Empieza pequeño: una regla paramétrica (method f) que afirme alguna propiedad básica que se cumple después de cualquier función, solo para confirmar que el arnés compila y funciona. (→ references/rules-invariants.md, references/spec-patterns-cookbook.md)
4. Ejecútala. certoraRun MiContrato.conf (o pasa el .sol/.spec directamente), luego abre el enlace del informe. (→ references/running-and-config.md)
5. Lee el informe. Inspecciona las trazas de llamadas CEX y el almacenamiento; corrige la especificación o confirma un error real. (→ references/running-and-config.md, references/debugging-and-timeouts.md)
6. Añade invariantes + fantasmas. Declara las propiedades reales: invariantes inductivas, más fantasmas/hooks para contabilidad (ej. sumaDeBalances == suministroTotal). (→ references/rules-invariants.md, references/hooks-and-ghosts.md)
7. Endurece solidez + cordura. Siempre ejecuta --rule_sanity basic; revisa cada resumen y suposición; elimina o justifica cualquier atajo inseguro. (→ references/soundness-and-approximations.md, references/methods-and-summaries.md)
8. Prueba con mutaciones. Usa Gambit para confirmar que tus reglas realmente detectan errores inyectados — una especificación que sobrevive a mutantes está asumiendo demasiado. (→ references/debugging-and-timeouts.md)

INICIO RÁPIDO en 10 segundos

pip install certora-cli
export CERTORAKEY=<tu-clave>

// Counter.spec — demostrar que increment() aumenta estrictamente el valor
methods {
    function get() external returns (uint256) envfree;
}

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

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

Cómo usar esta habilidad / mapa de referencia

Lee el archivo que coincida con la tarea que tienes delante:

• references/cvl-language.md — léelo cuando necesites sintaxis CVL: estructura de archivos, tipos (mathint/env/method/calldataarg/storage), casts y su solidez, operadores/cuantificadores, require vs assert vs satisfy vs havoc, funciones vs definiciones, y cómo llamar métodos del contrato (env, envfree, withrevert, lastReverted).
• references/rules-invariants.md — léelo cuando escribas reglas, reglas paramétricas (method f), testigos satisfy, o invariantes inductivas con bloques preserved y requireInvariant.
• references/methods-and-summaries.md — léelo cuando configures el bloque methods: tipos de entrada, envfree/optional, el catálogo completo de resúmenes + tabla de solidez, resúmenes de expresión/fantasma, y configuraciones multi-contrato (using, links, DISPATCHER).
• references/hooks-and-ghosts.md — léelo cuando necesites reflejar almacenamiento o demostrar contabilidad: hooks de almacenamiento/opcódigo/transitorios, variables/funciones fantasma, sumas fantasma y fantasmas persistent.
• references/running-and-config.md — léelo cuando instales, ejecutes certoraRun, escribas archivos .conf, elijas banderas, diseñes un proyecto o interpretes el informe web.
• references/spec-patterns-cookbook.md — léelo cuando quieras una receta lista: control de acceso, "qué puede cambiar", suma-de-balances, monotonicidad, condiciones de marco, máquinas de estado, viajes de ida y vuelta, conmutatividad, condiciones de reversión y reglas estilo prueba unitaria.
• references/advanced-defi-patterns.md — léelo cuando verifiques un protocolo real y el libro de recetas básico no sea suficiente: monotonicidad del tipo de cambio de bóvedas ERC4626 (multiplicación cruzada, sin almuerzo gratis, límites de vista previa), invariante k de AMM y sin extracción de valor, solvencia/salud/"sin deuda incobrable" de préstamos & liquidez anti-bloqueo, contabilidad de deriva de recompensas, reentrancia como CEI y control de acceso basado en roles a escala — cada idioma atribuido al repositorio de producción (Morpho/OZ/Aave/Certora) del que proviene.
• references/tooling-and-ecosystem.md — léelo cuando integres Certora en CI (GitHub Actions, caché, compuerta de PRs) o decidas qué herramienta se ajusta a una propiedad: una guía de decisión Certora vs Halmos vs Foundry (invariante/fuzz) vs Echidna, con compensaciones de cuándo usar cada una.
• references/learning-resources.md — léelo cuando quieras profundizar o incorporarte: enlaces externos seleccionados — tutoriales RareSkills/Certora, documentación oficial, charlas y repositorios de especificaciones públicas del mundo real (Morpho, Aave, OpenZeppelin, Compound) que vale la pena leer como ejemplos trabajados.
• references/soundness-and-approximations.md — léelo cuando decidas qué asumir vs afirmar: sólido/pesimista vs inseguro/optimista, aproximaciones de bucle/hashing/havoc, la familia de marcadores optimistas, qué garantiza una regla que pasa y la lista de verificación de revisión de solidez.
• references/debugging-and-timeouts.md — léelo cuando una regla sea vacua, lenta o sospechosa: --rule_sanity, mitigación de tiempos de espera (resúmenes, división, restricciones de rango), el informe de dificultad TAC, pruebas de mutación con Gambit, el LSP de VSCode y la lista de verificación "¿debería confiar en esta aprobación?".
• cheatsheet.md — léelo cuando quieras una referencia rápida de una página: las palabras clave CVL más usadas, esqueletos de reglas/invariantes, banderas comunes de certoraRun y los errores más frecuentes de un vistazo.
• examples/ERC20.spec — léelo cuando quieras una especificación trabajada completa: bloque methods, ghost+hook de suma-de-balances, invariante de suministro, reglas paramétricas/integridad/reversión/aditividad y control de acceso de minteo.
• examples/ERC20.conf — léelo cuando necesites una plantilla JSON5 ejecutable que cubra todas las claves comunes (files, verify, solc, packages, optimistic_loop, rule_sanity, ...).

Reglas de oro / errores comunes

• require ≠ reversión. require asume un hecho (poda el modelo); no verifica una reversión del contrato. Para razonar sobre reversiones usa withrevert + lastReverted.
• Cuidado con la vacuidad. Un require sobre-restringido puede hacer que una regla pase trivialmente porque ninguna entrada sobrevive. Siempre ejecuta --rule_sanity basic (prefiere advanced).
• Los marcadores optimistas son inseguros. --optimistic_loop, --optimistic_hashing, --optimistic_fallback, etc. asumen que ciertos casos no ocurren. Úsalos deliberadamente, documenta por qué y prefiere eliminar la necesidad.
• Prefiere preserved sobre filtered. Para invariantes, codifica las suposiciones en bloques preserved (con requireInvariant) en lugar de excluir métodos silenciosamente.
• Usa mathint para acumuladores. Las sumas y contadores en uint256 pueden desbordarse y producir CEXs fantasma (u ocultar reales); calcula en mathint sin límites, convierte en el límite.
• Una regla que pasa es tan buena como sus suposiciones. Cada resumen, enlace, límite de bucle y require es un agujero en la prueba. Prueba con mutaciones para confirmar que la regla realmente puede fallar.

---

Archivos más usados: empieza desde references/spec-patterns-cookbook.md para la receta adecuada y examples/ERC20.spec para una especificación completa y funcional que puedas adaptar.