EVMBench Certora Agent Harness

Harness agent configurabile per la generazione/raffinamento iterativo di specifiche per smart contract utilizzando:

• Task in stile EVMBench (openai/frontier-evals -> project/evmbench)
• Certora Prover (Certora/CertoraProver)
• Backend LLM: OpenAI API, OpenRouter API, Ollama locale, o modalità mock

Cosa fa

L'harness esegue un ciclo su una challenge:

1. Legge i file di contratto/contesto.
2. Chiede a un LLM il testo della specifica Certora CVL (output JSON rigoroso).
3. Esegue Certora.
4. Reinserisce l'output del verificatore nell'LLM.
5. Ripete fino al successo o al numero massimo di iterazioni.

Gli artefatti di esecuzione vengono persistiti per ogni iterazione.

Struttura del progetto

• src/evmbench_certora_harness/ implementazione principale
• configs/harness.example.yaml configurazione di esempio
• scripts/fetch_evmbench.sh helper per scaricare i task di benchmark
• examples/sample_challenge/ scaffold locale minimale
• 00_..05_*.md note sperimentali (compatibili con Obsidian)

Prerequisiti

• Python 3.9+
• Certora Prover installato ed eseguibile (certoraRun o certoraRun.py)
• Dipendenze solver/toolchain richieste da Certora (Z3/CVC5/JDK/ecc.)
• Un backend LLM:
  • OpenAI: OPENAI_API_KEY
  • OpenRouter: OPENROUTER_API_KEY
  • Ollama: server locale su http://localhost:11434

Certora upstream:

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

EVMBench upstream:

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

Installazione

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

Configurazione

Copia e modifica la configurazione:

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

Esecuzione

Challenge singola:

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

Prima challenge dal glob nella configurazione:

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

Dry run (nessuna esecuzione di Certora):

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

Note

• La sintassi del comando Certora varia da progetto a progetto. Mantieni certora.command_template consapevole della challenge.
• L'harness memorizza i log completi sotto runs/ per analisi post-mortem.