EVMBench Certora Agent Harness

Harness de agente configurável para geração/refinamento iterativo de especificações de contratos inteligentes usando:

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

O que isto faz

O harness itera sobre um desafio:

1. Lê ficheiros de contrato/contexto.
2. Pede a um LLM texto de especificação Certora CVL (saída JSON estrita).
3. Executa o Certora.
4. Devolve a saída do verificador ao LLM.
5. Repete até sucesso ou máximo de iterações.

Os artefactos de execução são persistidos para cada iteração.

Estrutura do projeto

• src/evmbench_certora_harness/ implementação principal
• configs/harness.example.yaml configuração de exemplo
• scripts/fetch_evmbench.sh auxiliar para obter tarefas de benchmark
• examples/sample_challenge/ scaffold local mínimo
• 00_..05_*.md notas de experiência (compatíveis com Obsidian)

Pré-requisitos

• Python 3.9+
• Certora Prover instalado e executável (certoraRun ou certoraRun.py)
• Dependências de solver/toolchain exigidas pelo Certora (Z3/CVC5/JDK/etc.)
• Um backend LLM:
  • OpenAI: OPENAI_API_KEY
  • OpenRouter: OPENROUTER_API_KEY
  • Ollama: servidor local em http://localhost:11434

Certora upstream:

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

EVMBench upstream:

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

Instalação

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

Configuração

Copie e edite a configuração:

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

Execução

Desafio único:

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

Primeiro desafio a partir de glob na configuração:

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

Dry run (sem execução do Certora):

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

Notas

• A sintaxe do comando Certora varia por projeto. Mantenha certora.command_template ciente do desafio.
• O harness armazena logs completos em runs/ para análise post-mortem.