vero-validate

Official

Efficient semantic check synthesis during code generation

Authorsunblaze-ucb
Version1.0.0
Installs0

System Documentation

What problem does it solve?

This Skill performs the LLM review component during the code generation stage, ensuring semantic correctness, code idiom, and meaningful tests across Lean 4 repositories.

Core Features & Use Cases

  • Semantic Check Synthesis: Evaluates the alignment of code specifications with intended intent, idiomatic code, meaningful test cases, and more.
  • Benchmark Curation: Designed to review semantic checks against a translated Lean project and its specifications.
  • Use Case: For repositories using Lean 4, this Skill is used to validate and ensure the quality of code and specifications.

Quick Start

Validate the semantic checks of the Lean 4 project 'benchmark_path'.

Dependency Matrix

Required Modules

None required

Components

scriptsreferencesassets

💻 Claude Code Installation

Recommended: Let Claude install automatically. Simply copy and paste the text below to Claude Code.

Please help me install this Skill:
Name: vero-validate
Download link: https://github.com/sunblaze-ucb/vero/archive/main.zip#vero-validate

Please download this .zip file, extract it, and install it in the .claude/skills/ directory.
View Source Repository

Agent Skills Search Helper

Install a tiny helper to your Agent, search and equip skill from 620,000+ vetted skills library on demand.