EVMBench Certora Agent Harness

Harness de agente configurable para la generación/refinamiento iterativo de especificaciones de contratos inteligentes usando:

• Tareas estilo EVMBench (openai/frontier-evals -> project/evmbench)
• Certora Prover (Certora/CertoraProver)
• Backend LLM: OpenAI API, OpenRouter API, Ollama local o modo mock

Qué hace esto

El harness itera sobre un desafío:

1. Lee archivos de contrato/contexto.
2. Solicita al LLM texto de especificación Certora CVL (salida JSON estricta).
3. Ejecuta Certora.
4. Retroalimenta la salida del verificador al LLM.
5. Repite hasta el éxito o el máximo de iteraciones.

Los artefactos de ejecución se conservan para cada iteración.

Estructura del proyecto

• src/evmbench_certora_harness/ implementación principal
• configs/harness.example.yaml configuración de ejemplo
• scripts/fetch_evmbench.sh script auxiliar para obtener tareas de benchmark
• examples/sample_challenge/ andamiaje local mínimo
• 00_..05_*.md notas de experimentos (compatibles con Obsidian)

Requisitos previos

• Python 3.9+
• Certora Prover instalado y ejecutable (certoraRun o certoraRun.py)
• Dependencias de solver/toolchain requeridas por Certora (Z3/CVC5/JDK/etc.)
• Un backend LLM:
  • OpenAI: OPENAI_API_KEY
  • OpenRouter: OPENROUTER_API_KEY
  • Ollama: servidor local en http://localhost:11434

Certora upstream:

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

EVMBench upstream:

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

Instalación

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

Configuración

Copiar y editar la configuración:

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

Ejecución

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

Notas

• La sintaxis del comando de Certora varía según el proyecto. Mantén certora.command_template adaptado al desafío.
• El harness almacena los registros completos en runs/ para análisis post-mortem.