gmh5225/evmbench-certora-agent-harnessHarnais d'agent itératif qui utilise des LLM et Certora Prover pour générer et affiner des spécifications CVL de contrats intelligents, en réinjectant la sortie du vérificateur jusqu'à la réussite ou le nombre maximal d'itérations.
Harnais d'agent configurable pour la génération/raffinement itératif de spécifications de contrats intelligents à l'aide de :
openai/frontier-evals -> project/evmbench)Certora/CertoraProver)Le harnais boucle sur un défi :
Les artefacts d'exécution sont conservés pour chaque itération.
src/evmbench_certora_harness/ implémentation principaleconfigs/harness.example.yaml configuration d'exemplescripts/fetch_evmbench.sh utilitaire pour récupérer les tâches de benchmarkexamples/sample_challenge/ échafaudage local minimal00_..05_*.md notes d'expérience (compatibles 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 .
Copiez et modifiez la configuration :
cp configs/harness.example.yaml configs/harness.yaml
Défi unique :
python -m evmbench_certora_harness.cli run \
--config configs/harness.yaml \
--challenge datasets/evmbench/audits/2023-07-pooltogether \
--max-iterations 4
Premier défi à partir du glob dans la configuration :
python -m evmbench_certora_harness.cli run --config configs/harness.yaml --limit 1
Exécution à blanc (sans exécution de Certora) :
python -m evmbench_certora_harness.cli run --config configs/harness.yaml --dry-run
certora.command_template adapté au défi.runs/ pour une analyse post-mortem.