v0.0.5 — Stronger Problems

Strengthens problem descriptions and postconditions to improve benchmark quality.

Changed

Explicit De Bruijn slot ordering in descriptions (issue #13):

• VB-T4-002 (GCD): description states @Nat.0=b (rightmost), @Nat.1=a
• VB-T4-004 (power): description states @Nat.0=exp (rightmost), @Nat.1=base
• VB-T5-003 (safe_div): description states slot mapping for both functions

Stronger postconditions that catch logic bugs (issue #14):

Problem	New postcondition	Z3 tier
multiply(a,b)	result == a * b	Tier 1
div_natural(a,b)	result * b <= a AND (result+1) * b > a	Tier 1
sum_to_n(n)	result == n * (n+1) / 2	Tier 1
gcd(a,b)	result <= a || b > 0	Tier 1
counter()	result == 3	Tier 3
state_double(x)	result == x * 2	Tier 3
state_max(n)	result == n	Tier 3

Tier 4 postconditions are Z3-proved. Tier 5 fall to runtime due to effect handlers.

Impact

A slot-swapped GCD or multiply that previously passed vera verify (because ensures(@Nat.result >= 0) is trivially true) will now fail verification. This makes the verify@1 metric more meaningful.

v0.0.4 — TypeScript Support

Adds TypeScript support for both baselines and LLM-generated code evaluation.

Added

• TypeScript baseline runner (vera-bench baselines --language typescript)
• TypeScript LLM generation (vera-bench run --model MODEL --language typescript)
• TypeScript prompt builder with automatic snake_case → camelCase conversion
• TypeScript code evaluation via npx tsx (Node.js 22+)
• Node.js 22 added to CI test job

Changed

• --language flag now accepts vera, python, or typescript
• Baselines command supports --language typescript
• Version bumped to 0.0.4

Usage

# TypeScript baselines
vera-bench baselines --language typescript

# LLM-generated TypeScript
vera-bench run --model claude-sonnet-4-20250514 --language typescript

# Full cross-language report
vera-bench report results/

v0.0.3 — Cross-Language Python Generation

Adds cross-language LLM comparison: ask the same model to write Python for the same problems.

Added

• --language python flag on vera-bench run for cross-language comparison
• Python prompt builder — minimal prompt (no SKILL.md, no contracts) for fair comparison
• Python code evaluation via subprocess with test wrapper
• Vera-specific metrics (verify@1, fix@1) hidden for Python runs
• CHANGELOG.md, CODE_OF_CONDUCT.md, CONTRIBUTING.md, SECURITY.md
• CI and Codecov badges in README

Security hardening

• Python subprocess runs with cwd=work_dir and API keys stripped from env
• SyntaxError/ImportError/NameError in generated Python sets check_pass=False

Usage

# Vera
vera-bench run --model claude-sonnet-4-20250514

# Python (same problems, same model)
vera-bench run --model claude-sonnet-4-20250514 --language python

# Three-way comparison
vera-bench report results/

v0.0.2 — Baseline Comparison

Adds Python baseline comparison and reporting fixes.

Added

• vera-bench baselines — runs canonical Python solutions against test cases
• Cross-language comparison in vera-bench report (Vera results alongside Python baselines)
• baseline_runner.py — subprocess-based execution with generated test wrappers

Fixed

• run_correct shows - instead of 0% when no test cases exist (Tier 2/3)
• Bool string normalisation ("true"/"false" from vera run mapped to Python True/False)
• check_rate type annotation (float | None)

Comparison (Claude Sonnet 4)

Model	check@1	verify@1	run_correct	Problems
Sonnet 4 (Vera)	96%	96%	83%	50
Python baseline	100%	-	100%	24

v0.0.1 — LLM Runner

First functional release of VeraBench.

What's included

• 50 benchmark problems across 5 difficulty tiers (10 per tier)
• Canonical solutions in Vera, Python, and TypeScript
• vera-bench run --model MODEL — end-to-end LLM evaluation pipeline
• vera-bench validate — problem and solution validation
• vera-bench report results/ — markdown report generation
• Full-spec and spec-from-NL prompt modes
• Retry-with-error-feedback (fix@1 metric)
• Incremental JSONL results output
• CI with lint, security, coverage, and dependency audit

First benchmark results (Claude Sonnet 4)

Metric	Overall	T1	T2	T3	T4	T5
check@1	96%	100%	100%	100%	90%	90%
verify@1	96%	100%	100%	100%	90%	89%
run_correct	83%	100%	-	-	75%	60%