EVMBench Certora Agent Harness

可配置的 agent 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/ 下，以便事后分析。