gmh5225/evmbench-certora-agent-harnessArnés de agente iterativo que utiliza LLMs y Certora Prover para generar y refinar especificaciones CVL de contratos inteligentes, realimentando la salida del verificador hasta alcanzar el éxito o el máximo de iteraciones.
Harness de agente configurable para la generación/refinamiento iterativo de especificaciones de contratos inteligentes usando:
openai/frontier-evals -> project/evmbench)Certora/CertoraProver)El harness itera sobre un desafío:
Los artefactos de ejecución se conservan para cada iteración.
src/evmbench_certora_harness/ implementación principalconfigs/harness.example.yaml configuración de ejemploscripts/fetch_evmbench.sh script auxiliar para obtener tareas de benchmarkexamples/sample_challenge/ andamiaje local mínimo00_..05_*.md notas de experimentos (compatibles 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 .
Copiar y editar la configuración:
cp configs/harness.example.yaml configs/harness.yaml
Desafío único:
python -m evmbench_certora_harness.cli run \
--config configs/harness.yaml \
--challenge datasets/evmbench/audits/2023-07-pooltogether \
--max-iterations 4
Primer desafío desde el glob en la configuración:
python -m evmbench_certora_harness.cli run --config configs/harness.yaml --limit 1
Ejecución en seco (sin ejecución de Certora):
python -m evmbench_certora_harness.cli run --config configs/harness.yaml --dry-run
certora.command_template adaptado al desafío.runs/ para análisis post-mortem.