EVMBench Certora Agent Harness

Настраиваемый агентный harness для итеративной генерации и уточнения спецификаций смарт-контрактов с использованием:

• Задач в стиле EVMBench (openai/frontier-evals -> project/evmbench)
• Certora Prover (Certora/CertoraProver)
• Бэкенда LLM: OpenAI API, OpenRouter API, локальный Ollama или mock-режим

Что это делает

Harness выполняет цикл по задаче:

1. Читает файлы контракта/контекста.
2. Запрашивает у LLM текст спецификации Certora CVL (строгий вывод JSON).
3. Запускает Certora.
4. Передаёт вывод верификатора обратно в LLM.
5. Повторяет до успеха или достижения максимального числа итераций.

Артефакты запуска сохраняются для каждой итерации.

Структура проекта

• src/evmbench_certora_harness/ — основная реализация
• configs/harness.example.yaml — пример конфигурации
• scripts/fetch_evmbench.sh — вспомогательный скрипт для загрузки задач бенчмарка
• examples/sample_challenge/ — минимальный локальный каркас
• 00_..05_*.md — заметки об экспериментах (совместимы с Obsidian)

Предварительные требования

• Python 3.9+
• Установленный и работоспособный Certora Prover (certoraRun или certoraRun.py)
• Зависимости решателя/тулчейна, необходимые для Certora (Z3/CVC5/JDK и т.д.)
• Один бэкенд LLM:
  • OpenAI: OPENAI_API_KEY
  • OpenRouter: OPENROUTER_API_KEY
  • Ollama: локальный сервер на http://localhost:11434

Оригинальный репозиторий Certora:

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

Оригинальный репозиторий EVMBench:

• https://github.com/openai/frontier-evals/tree/main/project/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 зависит от проекта. Держите certora.command_template с учётом особенностей задачи.
• Harness сохраняет полные логи в runs/ для последующего анализа.