Certora Prover (CVL / EVM)

Que fait EVM) ?

Le Certora Prover vérifie formellement les contrats intelligents : vous rédigez des spécifications en CVL (Certora Verification Language) décrivant des propriétés (règles et invariants), et le Prover prouve ces propriétés pour toutes les entrées et tous les états, ou renvoie un contre-exemple (CEX) concret.

Modèle mental essentiel — à lire en premier :

• Prouver, ne pas tester. Contrairement aux tests unitaires ou au fuzzing (qui échantillonnent quelques entrées), le Prover raisonne symboliquement sur chaque entrée, appelant, et état de stockage autorisé par votre modèle.
• Correct mais incomplet. Dans le modèle, il ne manquera pas une violation, mais il peut expirer, et il ne vérifie que ce que votre spécification affirme réellement. Une spécification vide/faible ne prouve rien d'utile.
• « Vérifié » = pas de contre-exemple dans le modèle, modulo vos hypothèses. Chaque require, résumé, déroulage de boucle, et indicateur optimiste réduit le modèle. Une coche verte n'est aussi forte que ces hypothèses — les obtenir correctement est tout l'enjeu.

Workflow : vérifier une application à partir de zéro

1. Installation + clé. pip install certora-cli ; définissez CERTORAKEY. (→ references/running-and-config.md)
2. Structure du projet. Placez les contrats dans src/, les spécifications dans certora/specs/, un .conf par cible. (→ references/running-and-config.md)
3. Écrivez une première règle de base/paramétrique. Commencez petit : une règle paramétrique (method f) affirmant qu'une propriété de base est vraie après n'importe quelle fonction, juste pour confirmer que le harnais compile et s'exécute. (→ references/rules-invariants.md, references/spec-patterns-cookbook.md)
4. Exécutez-la. certoraRun MyContract.conf (ou passez le .sol/.spec directement), puis ouvrez le lien du rapport. (→ references/running-and-config.md)
5. Lisez le rapport. Inspectez les traces d'appels CEX et le stockage ; corrigez la spécification ou confirmez un vrai bogue. (→ references/running-and-config.md, references/debugging-and-timeouts.md)
6. Ajoutez des invariants + fantômes. Énoncez les propriétés réelles : invariants inductifs, plus fantômes/hooks pour la comptabilité (par ex. sumOfBalances == totalSupply). (→ references/rules-invariants.md, references/hooks-and-ghosts.md)
7. Renforcez la correction et la vraisemblance. Exécutez toujours --rule_sanity basic ; révisez chaque résumé et hypothèse ; supprimez ou justifiez tout raccourci non fiable. (→ references/soundness-and-approximations.md, references/methods-and-summaries.md)
8. Testez par mutation. Utilisez Gambit pour confirmer que vos règles attrapent réellement les bogues injectés — une spécification qui survit aux mutants fait trop d'hypothèses. (→ references/debugging-and-timeouts.md)

DÉMARRAGE RAPIDE en 10 secondes

pip install certora-cli
export CERTORAKEY=<votre-clé>

// Counter.spec — prouve que increment() augmente strictement la valeur
methods {
    function get() external returns (uint256) envfree;
}

rule incrementIncreases(env e) {
    uint256 before = get();
    increment(e);
    assert get() > before, "increment doit augmenter le compteur";
}

certoraRun src/Counter.sol:Counter \
    --verify Counter:certora/specs/Counter.spec \
    --solc solc8.20 \
    --rule_sanity basic \
    --msg "incrémentation du compteur"

Comment utiliser cette compétence / carte de référence

Lisez le fichier correspondant à la tâche qui vous fait face :

• references/cvl-language.md — à lire quand vous avez besoin de la syntaxe CVL : structure du fichier, types (mathint/env/method/calldataarg/storage), casts et leur fiabilité, opérateurs/quantificateurs, require vs assert vs satisfy vs havoc, fonctions vs définitions, et comment appeler des méthodes de contrat (env, envfree, withrevert, lastReverted).
• references/rules-invariants.md — à lire quand vous écrivez des règles, des règles paramétriques (method f), des témoins satisfy, ou des invariants inductifs avec des blocs preserved et requireInvariant.
• references/methods-and-summaries.md — à lire quand vous configurez le bloc methods : types d'entrée, envfree/optional, le catalogue complet des résumés + tableau de fiabilité, les résumés d'expression/fantômes, et les configurations multi-contrats (using, links, DISPATCHER).
• references/hooks-and-ghosts.md — à lire quand vous avez besoin de refléter le stockage ou de prouver une comptabilité : hooks de stockage/opcode/transitoires, variables/fonctions fantômes, sommes fantômes, et fantômes persistent.
• references/running-and-config.md — à lire quand vous installez, exécutez certoraRun, écrivez des fichiers .conf, choisissez des indicateurs, structurez un projet, ou interprétez le rapport web.
• references/spec-patterns-cookbook.md — à lire quand vous voulez une recette prête : contrôle d'accès, « ce qui peut changer », somme des soldes, monotonie, conditions de cadre, machines d'état, allers-retours, commutativité, conditions de revert, et règles de style test unitaire.
• references/advanced-defi-patterns.md — à lire quand vous vérifiez un protocole réel et que le livre de recettes de base ne suffit pas : monotonie du taux de change du coffre ERC4626 (multiplication croisée, pas de repas gratuit, bornes de preview), invariant k de l'AMM et absence d'extraction de valeur, solvabilité de prêt/santé/« pas de créances irrécouvrables » & vivacité anti-blocage, comptabilité de dérive de récompense, réentrance comme CEI, et contrôle d'accès basé sur les rôles à grande échelle — chaque idiome attribué au dépôt de production (Morpho/OZ/Aave/Certora) dont il provient.
• references/tooling-and-ecosystem.md — à lire quand vous intégrez Certora dans une CI (GitHub Actions, mise en cache, contrôle des PRs) ou décidez quel outil correspond à une propriété : un guide de décision Certora vs Halmos vs Foundry (invariant/fuzz) vs Echidna, avec des compromis sur quand utiliser chacun.
• references/learning-resources.md — à lire quand vous voulez approfondir ou vous former : liens externes organisés — tutoriels RareSkills/Certora, documentation officielle, présentations, et dépôts de spécifications publiques réels (Morpho, Aave, OpenZeppelin, Compound) utiles comme exemples travaillés.
• references/soundness-and-approximations.md — à lire quand vous décidez quoi supposer vs affirmer : fiable/pessimiste vs non fiable/optimiste, approximations de boucle/hachage/havoc, la famille d'indicateurs optimistes, ce qu'une règle réussie garantit, et la liste de vérification de révision de fiabilité.
• references/debugging-and-timeouts.md — à lire quand une règle est vide, lente ou suspecte : --rule_sanity, atténuation des timeouts (résumés, fractionnement, contraintes de plage), le rapport de difficulté TAC, le test de mutation Gambit, le LSP VSCode, et la liste de vérification « dois-je faire confiance à cette réussite ? ».
• cheatsheet.md — à lire quand vous voulez une référence rapide d'une page : les mots-clés CVL les plus utilisés, squelettes de règles/invariants, indicateurs certoraRun courants, et les principaux pièges en un coup d'œil.
• examples/ERC20.spec — à lire quand vous voulez une spécification travaillée complète : bloc methods, fantôme de somme des soldes+hook, invariant de supply, règles paramétriques/d'intégrité/de revert/d'additivité, et contrôle d'accès mint.
• examples/ERC20.conf — à lire quand vous avez besoin d'un modèle de configuration JSON5 exécutable couvrant chaque clé courante (files, verify, solc, packages, optimistic_loop, rule_sanity, ...).

Règles d'or / pièges courants

• require ≠ revert. require suppose un fait (élague le modèle) ; il ne vérifie pas un revert du contrat. Pour raisonner sur les reverts, utilisez withrevert + lastReverted.
• Attention à la vacuité. Un require trop contraint peut faire réussir une règle trivialement car aucune entrée ne survit. Exécutez toujours --rule_sanity basic (préférez advanced).
• Les indicateurs optimistes sont non fiables. --optimistic_loop, --optimistic_hashing, --optimistic_fallback, etc. supposent des cas écartés. Utilisez-les délibérément, documentez pourquoi, et préférez éliminer le besoin.
• Préférez preserved à filtered. Pour les invariants, encodez les hypothèses dans des blocs preserved (avec requireInvariant) plutôt que d'exclure silencieusement des méthodes.
• Utilisez mathint pour les accumulateurs. Les sommes et compteurs en uint256 peuvent déborder et produire des CEX fantômes (ou cacher de vrais) ; calculez en mathint non borné, castez à la frontière.
• Une règle réussie n'est aussi bonne que ses hypothèses. Chaque résumé, lien, borne de boucle, et require est un trou dans la preuve. Testez par mutation pour confirmer que la règle peut réellement échouer.

---

Fichiers les plus utilisés : commencez par references/spec-patterns-cookbook.md pour la bonne recette et examples/ERC20.spec pour une spécification complète fonctionnelle à adapter.