gmh5225/evmbench-certora-agent-harnessИтеративный агентный каркас, использующий LLM и Certora Prover для генерации и уточнения CVL-спецификаций смарт-контрактов, передавая вывод верификатора обратно до достижения успеха или максимального числа итераций.
Настраиваемый агентный harness для итеративной генерации и уточнения спецификаций смарт-контрактов с использованием:
openai/frontier-evals -> project/evmbench)Certora/CertoraProver)Harness выполняет цикл по задаче:
Артефакты запуска сохраняются для каждой итерации.
src/evmbench_certora_harness/ — основная реализацияconfigs/harness.example.yaml — пример конфигурацииscripts/fetch_evmbench.sh — вспомогательный скрипт для загрузки задач бенчмаркаexamples/sample_challenge/ — минимальный локальный каркас00_..05_*.md — заметки об экспериментах (совместимы с Obsidian)certoraRun или certoraRun.py)OPENAI_API_KEYOPENROUTER_API_KEYhttp://localhost:11434Оригинальный репозиторий Certora:
Оригинальный репозиторий EVMBench:
python -m venv .venv
source .venv/bin/activate
pip install -e .
Скопируйте и отредактируйте конфигурацию:
cp configs/harness.example.yaml configs/harness.yaml
Одна задача:
python -m evmbench_certora_harness.cli run \
--config configs/harness.yaml \
--challenge datasets/evmbench/audits/2023-07-pooltogether \
--max-iterations 4
Первая задача из glob в конфигурации:
python -m evmbench_certora_harness.cli run --config configs/harness.yaml --limit 1
Пробный запуск (без выполнения Certora):
python -m evmbench_certora_harness.cli run --config configs/harness.yaml --dry-run
certora.command_template с учётом особенностей задачи.runs/ для последующего анализа.