Vero Validate

VCG Validate: LLM Review

The validate stage of the curation pipeline has two halves:

1. Rule-based (Python, deterministic): eight checks implemented in src/vero/curation/validation/checks.py. These cover schema, markers, file roles, build, toolchain, #guard.
2. LLM review (this skill): semantic checks that need judgment — does the spec capture intent, is the code idiomatic, are tests meaningful, etc., and what repo-specific issue patterns should feed future validation memory.

Use this skill only for the LLM-review half. Rule-based checks never call the LLM.

Reference the canonical shape at reference/BankLedger/. Every check compares the candidate against that shape.

Input

The subagent is handed:

• benchmark_path — absolute path to the translated Lean project (contains manifest.json, lakefile.toml, <Project>.lean, <Project>/Impl/, <Project>/Spec/, etc.).
• check_name — which semantic review to run.
• reference_path — absolute path to reference/BankLedger/ (the canonical benchmark, for shape comparison).

Output contract

A JSON object matching CheckResult from src/vero/curation/validation/types.py:

{
  "name": "<check_name>",
  "status": "pass | warn | fail",
  "details": [
    {"severity": "info|warn|error", "message": "...", "location": "file:line | null"}
  ]
}

Emit the JSON as a fenced ```json code block at the end of the reply. Text before the block is allowed (and helpful for debugging).

Rule of thumb for severity:

• info — positive signal, no action needed.
• warn — minor issue; pipeline should continue but the curator should look.
• error — must be fixed before the benchmark is usable.

Overall status rolls up from severities: any error → fail, any warn → warn, else pass.

Prior Memory

If the request includes memory_excerpt, read it before judging. Treat it as reviewed lessons from prior audits, not as proof that the current repo has the same problem. Use it to look for recurring patterns and to avoid repeating known mistakes.

When producing repo_issue_taxonomy, prefer lessons that can later be promoted into deterministic validation rules or stable judge prompts.

The checks

spec_intent_alignment

Claim to verify: every def spec_* (impl : RepoImpl) : Prop := … in <Project>/Spec/*.lean correctly formalizes the English intent in its /-- … -/ docstring (or in the plan.json nl_description).

How to run:

1. Read plan.json if present (for authoritative NL descriptions); else fall back to each spec's /-- -/ docstring.
2. For each spec, compare the natural-language description to the Lean body. Ask: "If the Lean body is true, does the English claim hold? And vice versa?"
3. Flag:
   • error — body contradicts the NL description.
   • warn — body misses a case the NL description implies.
   • info — matches cleanly.

idiom

Claim to verify: the Impl / Harness / Bundle code is idiomatic Lean 4 and matches the paradigm shape.

How to run:

1. Compare the Impl file structure against reference/BankLedger/BankLedger/Impl/*.lean: types in the foundation file, sig abbrevs in namespace <API>, and def <API>.<fn> : <API>.<FnSig> := <reference impl> inside code markers. Remember that pre-agent generation replaces those bodies with sorry; the curated source should not contain sorry there.
2. Check <Project>/Bundle.lean: structure <Project>Bundle where with one field per API sig. Field names match the API's Lean name (camelCase).
3. Check <Project>/Harness.lean: structure RepoImpl where <pkg> : <Project>Bundle; canonical wires via { <pkg> := { … } }. joint_unsat macro present; no other macros.
4. Flag un-idiomatic patterns: mutable state hacks, #[verifier::external_body]-shaped things, heavy meta-programming where a plain def would do.

test_meaningfulness

Claim to verify: <Project>/Test.lean's #guard assertions probe real behavior (not trivially True), cover the API surface, and include boundary cases.

How to run:

1. List every #guard in Test.lean.
2. For each guard, determine what behavior it exercises. Trivial guards (e.g. #guard True, #guard 1 == 1, #guard []) are error.
3. Check API coverage: does every API in manifest.json.packages[0].modules[].apis[] have at least one guard touching it? Missing coverage is warn.
4. Check boundary cases: empty inputs, duplicate IDs, zero balances, missing-account paths. Absence of any boundary case is warn.

review_annotations

Claim to verify: !curation @review v1 annotations in Impl/* have sensible content (real concerns, not stale copy-paste).

How to run:

1. Grep !curation @review across <Project>/Impl/*.lean.
2. For each line, check the <name> field matches a surrounding definition (within ~5 lines).
3. Check the <notes> field is non-empty and specific. Generic templates ("TODO", "review this") are warn.
4. Check the checkbox status ([ ] vs [x]) — if every annotation is [ ] (never reviewed), flag info; if mixed or fully [x], pass.