EVMBench Certora Agent Harness

Konfigurierbares Agent-Harness für die iterative Generierung/Verfeinerung von Smart-Contract-Spezifikationen mit:

• EVMBench-artigen Aufgaben (openai/frontier-evals -> project/evmbench)
• Certora Prover (Certora/CertoraProver)
• LLM-Backend: OpenAI API, OpenRouter API, lokales Ollama oder Mock-Modus

Was dies tut

Das Harness durchläuft eine Challenge in einer Schleife:

1. Liest Contract-/Kontextdateien.
2. Fragt ein LLM nach Certora-CVL-Spezifikationstext (strikte JSON-Ausgabe).
3. Führt Certora aus.
4. Speist die Verifier-Ausgabe zurück in das LLM.
5. Wiederholt dies bis zum Erfolg oder zur maximalen Iterationszahl.

Run-Artefakte werden für jede Iteration persistiert.

Projektstruktur

• src/evmbench_certora_harness/ Kernimplementierung
• configs/harness.example.yaml Beispielkonfiguration
• scripts/fetch_evmbench.sh Hilfsskript zum Abrufen von Benchmark-Aufgaben
• examples/sample_challenge/ minimales lokales Gerüst
• 00_..05_*.md Experimentnotizen (Obsidian-freundlich)

Voraussetzungen

• Python 3.9+
• Certora Prover installiert und ausführbar (certoraRun oder certoraRun.py)
• Von Certora benötigte Solver-/Toolchain-Abhängigkeiten (Z3/CVC5/JDK/etc.)
• Ein LLM-Backend:
  • OpenAI: OPENAI_API_KEY
  • OpenRouter: OPENROUTER_API_KEY
  • Ollama: lokaler Server unter http://localhost:11434

Certora-Upstream:

• https://github.com/Certora/CertoraProver

EVMBench-Upstream:

• https://github.com/openai/frontier-evals/tree/main/project/evmbench

Installation

python -m venv .venv
source .venv/bin/activate
pip install -e .

Konfiguration

Konfiguration kopieren und bearbeiten:

cp configs/harness.example.yaml configs/harness.yaml

Ausführung

Einzelne Challenge:

python -m evmbench_certora_harness.cli run \
  --config configs/harness.yaml \
  --challenge datasets/evmbench/audits/2023-07-pooltogether \
  --max-iterations 4

Erste Challenge aus dem Glob in der Konfiguration:

python -m evmbench_certora_harness.cli run --config configs/harness.yaml --limit 1

Dry Run (keine Certora-Ausführung):

python -m evmbench_certora_harness.cli run --config configs/harness.yaml --dry-run

Hinweise

• Die Certora-Befehlssyntax variiert je nach Projekt. Halte certora.command_template challenge-spezifisch.
• Das Harness speichert vollständige Logs unter runs/ für die Post-Mortem-Analyse.