EVMBench Certora 에이전트 하네스

다음을 사용하여 반복적인 스마트 컨트랙트 명세 생성/개선을 위한 구성 가능한 에이전트 하네스:

• EVMBench 스타일 작업 (openai/frontier-evals -> project/evmbench)
• Certora Prover (Certora/CertoraProver)
• LLM 백엔드: OpenAI API, OpenRouter API, 로컬 Ollama 또는 mock 모드

기능

하네스는 챌린지에 대해 반복 실행합니다:

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/ 아래에 저장합니다.