EVMBench Certora एजेंट हार्नेस

इटरेटिव स्मार्ट-कॉन्ट्रैक्ट स्पेक जनरेशन/रिफाइनमेंट के लिए कॉन्फ़िगर करने योग्य एजेंट हार्नेस, जो निम्नलिखित का उपयोग करता है:

• 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 द्वारा आवश्यक Solver/टूलचेन निर्भरताएँ (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/ के अंतर्गत संग्रहीत करता है।