EVMBench Certora Agent Harness

反復的なスマートコントラクト仕様の生成/改良のための設定可能なエージェントハーネス。以下を使用:

• EVMBench スタイルのタスク (openai/frontier-evals -> project/evmbench)
• Certora Prover (Certora/CertoraProver)
• LLM バックエンド: OpenAI API、OpenRouter API、ローカル Ollama、またはモックモード

これが行うこと

ハーネスはチャレンジをループ処理します:

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 はチャレンジを考慮したものにしてください。
• ハーネスは事後分析のために完全なログを runs/ 以下に保存します。