Automated scheduled benchmark runs with structured storage

[aallan]

Context

Currently benchmarks are run manually from a developer's machine. For longitudinal tracking across vera compiler versions and model releases, we need automated scheduled runs that store results in a structured, queryable format — not flat JSONL files.

What this looks like

A GitHub Actions scheduled workflow that:

1. Triggers weekly (or on vera release tags)
2. Installs the latest vera from main (or a pinned release)
3. Runs the full 50-problem benchmark against a matrix of models:
   • Claude Sonnet 4, Claude Opus 4
   • GPT-4o
   • (Others as API access permits)
4. Runs both Vera full-spec and spec-from-NL modes
5. Stores results in a structured format (not flat files)
6. Publishes updated results to the dashboard (Results dashboard (GitHub Pages or veralang.dev) #30)

Storage: beyond flat JSONL

Flat JSONL files in results/ don't scale for longitudinal tracking. Each run produces ~100-200 result records (50 problems × 2-4 modes × 1-2 attempts), and we'll accumulate hundreds of runs over time. Options:

Option A: SQLite database in the repo

• Single results/verabench.db file
• Schema: runs table (run_id, timestamp, vera_version, skill_md_hash) + results table (run_id, problem_id, model, language, mode, check_pass, verify_pass, run_correct, ...)
• Queryable with standard SQL
• Git-tracked (SQLite is a single file, diffs are binary but size is manageable)
• vera-bench report reads from DB instead of globbing JSONL

Option B: Cloud database (Supabase, PlanetScale, etc.)

• Better for public dashboards and API access
• More infrastructure to maintain
• Overkill for current scale

Option C: Structured JSONL with metadata headers

• Keep JSONL but add a metadata record at the top of each file: {"_meta": {"run_id": "...", "vera_version": "0.0.105", "skill_md_hash": "abc123", "timestamp": "..."}}
• Naming convention: results/{date}-{vera_version}-{model}.jsonl
• Simpler than SQLite but harder to query across runs

Recommendation: Start with SQLite (Option A). It's zero-infrastructure, queryable, and the vera-bench report command can read from it directly. Migrate to a cloud DB later if the dashboard needs an API.

Cost considerations

Each full run (50 problems × 1 model × 2 modes) costs approximately:

• ~100 API calls
• ~500K input tokens (mostly SKILL.md context, ~65K per call)
• ~15K output tokens
• Estimated cost: ~$2-5 per model per run (varies by model pricing)

Weekly runs across 3 models ≈ $30-60/month. Acceptable for a research project.

Secrets management

The scheduled workflow needs API keys as GitHub Actions secrets:

• ANTHROPIC_API_KEY — for Claude models
• OPENAI_API_KEY — for GPT models

These are already used in the manual workflow pattern.

Relates to

• Include vera compiler version in output JSONL filename #20 — vera version in filenames/metadata
• Run benchmark against multiple models (Opus, GPT-4o, DeepSeek, Gemini) #24 — multi-model runs
• Results dashboard (GitHub Pages or veralang.dev) #30 — results dashboard (consumes the stored data)

[aallan]

Simplification: start with flat JSONL files in results/ committed by the GitHub Actions workflow, using the naming convention from #20 ({date}-{vera_version}-{model}-{mode}.jsonl). The workflow commits results back to the repo after each run.

Migrate to SQLite or a DB only if querying across hundreds of runs becomes painful. Keep it simple for now.

[aallan]

Dependency: VB-T4-007 (count_digits) takes ~78s due to Z3 solver time. aallan/vera#391 (per-contract Z3 timeout) would help prevent CI hangs in automated runs.

[aallan]

Note from v0.0.7 benchmark runs: The script-level subprocess timeout (currently 60 min per target) is a blunt instrument. For automated scheduled runs, the runner should support per-problem timeouts — if one problem hangs or a model is slow on a specific prompt, it shouldn't kill the entire 50-problem run. This would also enable better error reporting: mark individual problems as timeout in the JSONL rather than losing the whole run. Relevant context: kimi-k2.5 hit the 30-minute timeout during a full benchmark run, losing all progress.

[aallan]

Two pieces of the prerequisite tooling for this landed in PR #93, worth noting before someone builds the workflow.

scripts/preflight.sh is the gate step a scheduled run needs. It verifies every configured model id against each provider's /v1/models, that auth works, that the request parameters each model accepts are the ones we send, and that all four toolchains resolve — at one problem per check, roughly $1–2 against a sweep that is hours. Critically for automation, it now exits non-zero when the gate fails, so it composes:

- run: bash scripts/preflight.sh
- run: python scripts/run_full_benchmark.py --model ... --skip-baselines

Until #93 it always exited 0 — it could print *** pro may be SILENTLY IGNORED ***, the single finding that invalidates the reasoning slide, and a chained && would sail straight past.

The model list is read from run_full_benchmark.py rather than duplicated, so a model added to the sweep is gated automatically instead of silently skipped.

Error accounting now exists, which unattended runs need more than attended ones. BenchmarkMetrics gained run_eligible and errored (#95): run_correct is measured over problems that compiled, so API-error rows used to leave the denominator silently — 40 API failures plus 20 successes reported run_correct = 100%. For a scheduled run, where nobody is watching the console, that is the difference between a visibly broken night and a plausible datapoint quietly entering the longitudinal series this issue exists to build.

Suggest the workflow asserts on errored before storing anything, rather than only on exit codes.

Two caveats for the design here:

• There is no resume. vera-bench run unlinks the output file for that model × language × mode at startup, and filenames carry no timestamp. A job killed at the 6-hour runner limit loses that target entirely, so the matrix needs to be sharded across jobs rather than run as one long step.
• The problem count is 60, not 50 as this issue states, and there are ten targets per model (six LLM + four baselines) rather than the two listed. Worth recosting the runtime estimate before committing to a schedule.

[aallan]

PR #100 built most of the substrate a scheduled run needs:

• scripts/run_sweep.sh — an idempotent full-matrix sweep: it skips any target already on disk and clean and re-runs the rest. A sharded scheduled run can lean on that skip-clean idempotence for the "no resume" problem noted above — shard the matrix across jobs, and a job that dies just re-runs its shard.
• scripts/sweep_status.py — reads the JSONL rows and separates transient (re-run) from real results (keep); a workflow can assert "zero transient rows" before storing.
• scripts/rerun_failed.py — surgical per-problem repair.
• vera_bench/matrix.py — the model matrix as a single source, so a job enumerates from it.

The remaining robustness gap for unattended automation is #101: the sweep currently re-runs whole targets on any transient, which is wasteful and can fail to converge under provider flakiness with no human watching. Structured storage (SQLite, your Option A) is still the open design piece.