gmh5225/evmbench-certora-agent-harnessHarness de agente iterativo que usa LLMs e o Certora Prover para gerar e refinar especificações CVL de contratos inteligentes, realimentando a saída do verificador até obter sucesso ou atingir o número máximo de iterações.
Harness de agente configurável para geração/refinamento iterativo de especificações de contratos inteligentes usando:
openai/frontier-evals -> project/evmbench)Certora/CertoraProver)O harness itera sobre um desafio:
Os artefactos de execução são persistidos para cada iteração.
src/evmbench_certora_harness/ implementação principalconfigs/harness.example.yaml configuração de exemploscripts/fetch_evmbench.sh auxiliar para obter tarefas de benchmarkexamples/sample_challenge/ scaffold local mínimo00_..05_*.md notas de experiência (compatíveis com Obsidian)certoraRun ou certoraRun.py)OPENAI_API_KEYOPENROUTER_API_KEYhttp://localhost:11434Certora upstream:
EVMBench upstream:
python -m venv .venv
source .venv/bin/activate
pip install -e .
Copie e edite a configuração:
cp configs/harness.example.yaml configs/harness.yaml
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
certora.command_template ciente do desafio.runs/ para análise post-mortem.