zakrad/certora-prover-skill

Certora Prover (CVL / EVM)

Der Certora Prover verifiziert Smart Contracts formal: Sie schreiben Spezifikationen in CVL (Certora Verification Language), die Eigenschaften (Rules und Invariants) beschreiben, und der Prover beweist sie für alle Eingaben und Zustände oder gibt ein konkretes Gegenbeispiel (CEX) zurück.

Zentrales mentales Modell – zuerst lesen:

• Beweisen, nicht testen. Anders als Unit-Tests oder Fuzzing (die nur wenige Eingaben abtasten), argumentiert der Prover symbolisch über jede Eingabe, jeden Aufrufer und jeden Speicherzustand, der von Ihrem Modell erlaubt wird.
• Korrekt, aber unvollständig. Innerhalb des Modells wird er keinen Verstoß übersehen, kann aber ein Timeout verursachen, und er prüft nur, was Ihre Spezifikation tatsächlich behauptet. Eine leere/schwache Spezifikation beweist nichts Nützliches.
• „Verifiziert“ = kein Gegenbeispiel innerhalb des Modells, abhängig von Ihren Annahmen. Jedes require, jede Zusammenfassung (Summary), Schleifenentrollung und optimistische Flag schränkt das Modell ein. Ein grüner Haken ist nur so stark wie diese Annahmen – diese richtig zu setzen, ist die ganze Herausforderung.

Workflow: Eine App von Grund auf verifizieren

1. Installation + Schlüssel. pip install certora-cli; setzen Sie CERTORAKEY. (→ references/running-and-config.md)
2. Projektstruktur. Legen Sie die Verträge unter src/ ab, Spezifikationen unter certora/specs/, eine .conf pro Ziel. (→ references/running-and-config.md)
3. Erste grundlegende/parametrische Regel schreiben. Fangen Sie klein an: Eine parametrische Regel (method f), die eine grundlegende Eigenschaft nach jeder Funktion behauptet, nur um zu bestätigen, dass das Grundgerüst kompiliert und läuft. (→ references/rules-invariants.md, references/spec-patterns-cookbook.md)
4. Ausführen. certoraRun MyContract.conf (oder übergeben Sie die .sol/.spec direkt), dann öffnen Sie den Berichtslink. (→ references/running-and-config.md)
5. Bericht lesen. Untersuchen Sie CEX-Aufrufspuren und Speicher; korrigieren Sie die Spezifikation oder bestätigen Sie einen echten Fehler. (→ references/running-and-config.md, references/debugging-and-timeouts.md)
6. Invarianten + Ghosts hinzufügen. Formulieren Sie die tatsächlichen Eigenschaften: induktive Invarianten, plus Ghosts/Hooks für Buchhaltung (z.B. sumOfBalances == totalSupply). (→ references/rules-invariants.md, references/hooks-and-ghosts.md)
7. Soundness + Sanity härten. Führen Sie immer --rule_sanity basic aus; überprüfen Sie jede Summary und Annahme; entfernen oder rechtfertigen Sie jede unsounde Abkürzung. (→ references/soundness-and-approximations.md, references/methods-and-summaries.md)
8. Mutationstests. Verwenden Sie Gambit, um zu bestätigen, dass Ihre Regeln tatsächlich injizierte Fehler erkennen – eine Spezifikation, die Mutationen überlebt, nimmt zu viel an. (→ references/debugging-and-timeouts.md)

10-Sekunden-QUICKSTART

pip install certora-cli
export CERTORAKEY=<ihr-schlüssel>

// Counter.spec – beweisen, dass increment() den Wert strikt erhöht
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"

Verwendung dieses Skills / Referenzkarte

Lesen Sie die Datei, die zur aktuellen Aufgabe passt:

• references/cvl-language.md – lesen, wenn Sie CVL-Syntax benötigen: Dateistruktur, Typen (mathint/env/method/calldataarg/storage), Casts und deren Soundness, Operatoren/Quantoren, require vs assert vs satisfy vs havoc, Funktionen vs Definitionen und wie man Vertragsmethoden aufruft (env, envfree, withrevert, lastReverted).
• references/rules-invariants.md – lesen, wenn Sie Regeln, parametrische Regeln (method f), satisfy-Zeugen oder induktive Invarianten mit preserved-Blöcken und requireInvariant schreiben.
• references/methods-and-summaries.md – lesen, wenn Sie den methods-Block einrichten: Eintragsarten, envfree/optional, den vollständigen Summary-Katalog + Soundness-Tabelle, Ausdrucks-/Ghost-Summaries und Multi-Vertrags-Setups (using, links, DISPATCHER).
• references/hooks-and-ghosts.md – lesen, wenn Sie Speicher spiegeln oder Buchhaltung beweisen müssen: Speicher-/Opcode-/Transient-Hooks, Ghost-Variablen/-Funktionen, Summen-Ghosts und persistent-Ghosts.
• references/running-and-config.md – lesen, wenn Sie installieren, certoraRun ausführen, .conf-Dateien schreiben, Flags wählen, ein Projekt anlegen oder den Webreport interpretieren.
• references/spec-patterns-cookbook.md – lesen, wenn Sie ein fertiges Rezept wollen: Zugriffskontrolle, „was kann sich ändern“, Summe-der-Kontostände, Monotonie, Rahmenbedingungen, Zustandsautomaten, Round-Trips, Kommutativität, Revert-Bedingungen und Unit-Test-ähnliche Regeln.
• references/advanced-defi-patterns.md – lesen, wenn Sie ein echtes Protokoll verifizieren und das grundlegende Kochbuch nicht ausreicht: ERC4626-Vault-Wechselkurs-Monotonie (Kreuzmultiplikation, No-Free-Lunch, Preview-Grenzen), AMM-k-Invariante & No-Value-Extraction, Kredit-Solvenz/Gesundheit/„No Bad Debt“ & Anti-Lockup-Liveness, Reward-Drift-Buchhaltung, Reentrancy-as-CEI und rollenbasierte Zugriffskontrolle in großem Maßstab – jedes Idiom wird dem Produktions-Repository (Morpho/OZ/Aave/Certora) zugeordnet, aus dem es stammt.
• references/tooling-and-ecosystem.md – lesen, wenn Sie Certora in CI einbinden (GitHub Actions, Caching, PR-Gating) oder entscheiden, welches Tool zu einer Eigenschaft passt: eine Entscheidungshilfe zwischen Certora vs Halmos vs Foundry (Invariant/Fuzz) vs Echidna, mit Abwägungen, wann man zu welchem greift.
• references/learning-resources.md – lesen, wenn Sie tiefer einsteigen oder einarbeiten wollen: kuratierte externe Links – RareSkills/Certora-Tutorials, offizielle Dokumentation, Vorträge und reale öffentliche Spezifikations-Repositories (Morpho, Aave, OpenZeppelin, Compound), die sich als ausgearbeitete Beispiele lohnen.
• references/soundness-and-approximations.md – lesen, wenn Sie entscheiden, was Sie annehmen vs. behaupten sollen: sound/pessimistisch vs unsound/optimistisch, Schleifen-/Hashing-/Havoc-Näherungen, die Familie der optimistischen Flags, was eine bestandene Regel garantiert und die Soundness-Überprüfungs-Checkliste.
• references/debugging-and-timeouts.md – lesen, wenn eine Regel leer, langsam oder verdächtig ist: --rule_sanity, Timeout-Minderung (Summaries, Aufteilung, Bereichsbeschränkungen), der TAC-Schwierigkeitsbericht, Gambit-Mutationstests, das VSCode-LSP und die Checkliste „Sollte ich diesem Bestehen vertrauen?“.
• cheatsheet.md – lesen, wenn Sie eine einseitige Kurzreferenz wollen: die am häufigsten verwendeten CVL-Schlüsselwörter, Regel-/Invarianten-Gerüste, übliche certoraRun-Flags und die wichtigsten Fallstricke auf einen Blick.
• examples/ERC20.spec – lesen, wenn Sie eine vollständige ausgearbeitete Spezifikation wollen: Methods-Block, Summe-der-Kontostände-Ghost+Hook, Supply-Invariante, parametrische/Integritäts-/Revert-/Additivitätsregeln und Zugriffskontrolle für Mint.
• examples/ERC20.conf – lesen, wenn Sie eine ausführbare JSON5-Konfigurationsvorlage benötigen, die alle gängigen Schlüssel abdeckt (files, verify, solc, packages, optimistic_loop, rule_sanity, ...).

Goldene Regeln / Häufige Fallstricke

• require ≠ Revert. require nimmt eine Tatsache an (schränkt das Modell ein); es prüft keinen Vertrags-Revert. Um Reverts zu modellieren, verwenden Sie withrevert + lastReverted.
• Achten Sie auf Leere. Ein zu stark eingeschränktes require kann eine Regel trivial bestehen lassen, weil keine Eingabe übrig bleibt. Führen Sie immer --rule_sanity basic aus (bevorzugen Sie advanced).
• Optimistische Flags sind unsound. --optimistic_loop, --optimistic_hashing, --optimistic_fallback, usw. nehmen Fälle weg. Verwenden Sie sie bewusst, dokumentieren Sie warum, und ziehen Sie es vor, die Notwendigkeit zu beseitigen.
• Bevorzugen Sie preserved gegenüber filtered. Für Invarianten kodieren Sie Annahmen in preserved-Blöcken (mit requireInvariant), anstatt Methoden stillschweigend auszuschließen.
• Verwenden Sie mathint für Akkumulatoren. Summen und Zähler in uint256 können überlaufen und phantomhafte CEXs erzeugen (oder echte verstecken); rechnen Sie in unbeschränktem mathint und casten Sie an der Grenze.
• Eine bestandene Regel ist nur so gut wie ihre Annahmen. Jede Summary, jeder Link, jede Schleifengrenze und jedes require ist ein Loch im Beweis. Testen Sie durch Mutationen, ob die Regel tatsächlich fehlschlagen kann.

---

Meistgenutzte Dateien: Starten Sie mit references/spec-patterns-cookbook.md für das richtige Rezept und examples/ERC20.spec für eine vollständige, funktionierende Spezifikation zur Anpassung.