gmh5225/evmbench-certora-agent-harnessHarness agent iterativo che utilizza LLM e Certora Prover per generare e perfezionare specifiche CVL di smart contract, reinviando l'output del verificatore fino al successo o al numero massimo di iterazioni.
Harness agent configurabile per la generazione/raffinamento iterativo di specifiche per smart contract utilizzando:
openai/frontier-evals -> project/evmbench)Certora/CertoraProver)L'harness esegue un ciclo su una challenge:
Gli artefatti di esecuzione vengono persistiti per ogni iterazione.
src/evmbench_certora_harness/ implementazione principaleconfigs/harness.example.yaml configurazione di esempioscripts/fetch_evmbench.sh helper per scaricare i task di benchmarkexamples/sample_challenge/ scaffold locale minimale00_..05_*.md note sperimentali (compatibili con Obsidian)certoraRun o certoraRun.py)OPENAI_API_KEYOPENROUTER_API_KEYhttp://localhost:11434Certora upstream:
EVMBench upstream:
python -m venv .venv
source .venv/bin/activate
pip install -e .
Copia e modifica la configurazione:
cp configs/harness.example.yaml configs/harness.yaml
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
certora.command_template consapevole della challenge.runs/ per analisi post-mortem.