gmh5225/evmbench-certora-agent-harnessIterativer Agent-Harness, der LLMs und den Certora Prover nutzt, um CVL-Spezifikationen für Smart Contracts zu generieren und zu verfeinern, wobei die Ausgabe des Verifiers zurückgespeist wird, bis ein Erfolg eintritt oder die maximale Anzahl an Iterationen erreicht ist.
Konfigurierbares Agent-Harness für die iterative Generierung/Verfeinerung von Smart-Contract-Spezifikationen mit:
openai/frontier-evals -> project/evmbench)Certora/CertoraProver)Das Harness durchläuft eine Challenge in einer Schleife:
Run-Artefakte werden für jede Iteration persistiert.
src/evmbench_certora_harness/ Kernimplementierungconfigs/harness.example.yaml Beispielkonfigurationscripts/fetch_evmbench.sh Hilfsskript zum Abrufen von Benchmark-Aufgabenexamples/sample_challenge/ minimales lokales Gerüst00_..05_*.md Experimentnotizen (Obsidian-freundlich)certoraRun oder certoraRun.py)OPENAI_API_KEYOPENROUTER_API_KEYhttp://localhost:11434Certora-Upstream:
EVMBench-Upstream:
python -m venv .venv
source .venv/bin/activate
pip install -e .
Konfiguration kopieren und bearbeiten:
cp configs/harness.example.yaml configs/harness.yaml
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
certora.command_template challenge-spezifisch.runs/ für die Post-Mortem-Analyse.