Agent skill

Vero Source Coq

Load BEFORE translating Coq source (.v files) to Lean 4. An agent skill from sunblaze-ucb/vero.

Apache-2.0Auto-check: notesWriting & Content

Install Vero Source Coq

skills CLI

$ npx skills add sunblaze-ucb/vero --skill vero-source-coq -a claude-code

Project install by default; add -g for ~/.claude/skills/.

GitHub CLI

$ gh skill install sunblaze-ucb/vero vero-source-coq --agent claude-code

Project scope by default; add --scope user for a personal install. Needs GitHub CLI 2.90.0 or later (public preview).

Manual copy

$ git clone --depth 1 https://github.com/sunblaze-ucb/vero.git skills-src && mkdir -p .claude/skills && cp -r skills-src/.claude/skills/vero-source-coq .claude/skills/vero-source-coq && rm -rf skills-src

Use ~/.claude/skills/ instead of .claude/skills for a personal install. The folder must contain SKILL.md.

Claude Code skills documentation · loads skills from .claude/skills/

Paste into Claude Code

Install the "vero-source-coq" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-source-coq into .claude/skills/vero-source-coq/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-source-coq", then confirm the skill loads.

Claude Code copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

$skill-installer

$skill-installer install https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-source-coq

Type this inside Codex. $skill-installer <name> installs a curated skill from openai/skills. The installer writes to $CODEX_HOME/skills (default ~/.codex/skills). Restart Codex if the skill does not show up.

skills CLI

$ npx skills add sunblaze-ucb/vero --skill vero-source-coq -a codex

Project install goes to .agents/skills/; add -g for ~/.codex/skills/.

GitHub CLI

$ gh skill install sunblaze-ucb/vero vero-source-coq --agent codex

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/sunblaze-ucb/vero.git skills-src && mkdir -p .agents/skills && cp -r skills-src/.claude/skills/vero-source-coq .agents/skills/vero-source-coq && rm -rf skills-src

Use ~/.agents/skills/ instead of .agents/skills for a personal install.

Codex skills documentation · loads skills from .agents/skills/

Paste into Codex

Install the "vero-source-coq" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-source-coq into .agents/skills/vero-source-coq/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-source-coq", then confirm the skill loads.

Codex copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

skills CLI

$ npx skills add sunblaze-ucb/vero --skill vero-source-coq -a cursor

Project install goes to .agents/skills/; add -g for ~/.cursor/skills/.

GitHub CLI

$ gh skill install sunblaze-ucb/vero vero-source-coq --agent cursor

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/sunblaze-ucb/vero.git skills-src && mkdir -p .cursor/skills && cp -r skills-src/.claude/skills/vero-source-coq .cursor/skills/vero-source-coq && rm -rf skills-src

Use ~/.cursor/skills/ instead of .cursor/skills for a personal install.

Cursor skills documentation · loads skills from .cursor/skills/, .agents/skills/, .claude/skills/, .codex/skills/

Paste into Cursor

Install the "vero-source-coq" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-source-coq into .cursor/skills/vero-source-coq/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-source-coq", then confirm the skill loads.

Cursor copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

gemini skills install

$ gemini skills install https://github.com/sunblaze-ucb/vero.git --path .claude/skills/vero-source-coq

--scope user (default) or --scope workspace; --path is the subfolder of the repo that holds the skill; --consent skips the security confirmation prompt.

skills CLI

$ npx skills add sunblaze-ucb/vero --skill vero-source-coq -a gemini-cli

Project install goes to .agents/skills/; add -g for ~/.gemini/skills/.

GitHub CLI

$ gh skill install sunblaze-ucb/vero vero-source-coq --agent gemini-cli

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/sunblaze-ucb/vero.git skills-src && mkdir -p .gemini/skills && cp -r skills-src/.claude/skills/vero-source-coq .gemini/skills/vero-source-coq && rm -rf skills-src

Use ~/.gemini/skills/ instead of .gemini/skills for a personal install, then run /skills reload.

Gemini CLI skills documentation · loads skills from .gemini/skills/, .agents/skills/

Paste into Gemini CLI

Install the "vero-source-coq" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-source-coq into .gemini/skills/vero-source-coq/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-source-coq", then confirm the skill loads.

Gemini CLI copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

GitHub CLI

$ gh skill install sunblaze-ucb/vero vero-source-coq

Installs for Copilot at project scope by default; add --scope user for a personal install. Preview a skill first with gh skill preview. Needs GitHub CLI 2.90.0 or later (public preview).

skills CLI

$ npx skills add sunblaze-ucb/vero --skill vero-source-coq -a github-copilot

Project install goes to .agents/skills/; add -g for ~/.copilot/skills/.

Manual copy

$ git clone --depth 1 https://github.com/sunblaze-ucb/vero.git skills-src && mkdir -p .github/skills && cp -r skills-src/.claude/skills/vero-source-coq .github/skills/vero-source-coq && rm -rf skills-src

Use ~/.copilot/skills/ instead of .github/skills for a personal install. Commit .github/skills so cloud agent and code review can use it.

GitHub Copilot skills documentation · loads skills from .github/skills/, .claude/skills/, .agents/skills/

Paste into GitHub Copilot

Install the "vero-source-coq" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-source-coq into .github/skills/vero-source-coq/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-source-coq", then confirm the skill loads.

GitHub Copilot copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

skills CLI

$ npx skills add sunblaze-ucb/vero --skill vero-source-coq -a opencode

OpenCode documents no install command of its own. Project install goes to .agents/skills/; add -g for ~/.config/opencode/skills/.

GitHub CLI

$ gh skill install sunblaze-ucb/vero vero-source-coq --agent opencode

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/sunblaze-ucb/vero.git skills-src && mkdir -p .opencode/skills && cp -r skills-src/.claude/skills/vero-source-coq .opencode/skills/vero-source-coq && rm -rf skills-src

Use ~/.config/opencode/skills/ instead of .opencode/skills for a personal install.

OpenCode skills documentation · loads skills from .opencode/skills/, .claude/skills/, .agents/skills/

Paste into OpenCode

Install the "vero-source-coq" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-source-coq into .opencode/skills/vero-source-coq/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-source-coq", then confirm the skill loads.

OpenCode copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

Facts

Skill name: vero-source-coq
GitHub stars: 107
Token cost: ~2k tokens
SKILL.md length: 715 words
Files: 1
Skills in repo: 16
Repo updated: Aug 17, 2026
First seen: Oct 7, 2026
Licence: Apache-2.0

At a glance

Load BEFORE translating Coq source (.v files) to Lean 4. An agent skill from sunblaze-ucb/vero.

Tasks that involve Translation
SKILL.md covers When to use, Output-shape recap…, Coq construct → Lean… and Type mapping, plus 6 more sections
Instructions only: no scripts, shell commands, URLs or credentials in SKILL.md

What it does

Vero Source Coq is an agent skill from sunblaze-ucb/vero. Load BEFORE translating Coq source (.v files) to Lean 4. Provides Coq-specific classification rules, type mappings, and patterns for mapping Coq constructs (Definition / Fixpoint / Inductive / Theorem / Module) into the ratified bundle paradigm (Impl/ + Spec/ + Bundle + Harness). Pair with vero-discover, vero-plan, vero-translate, and vero-coq-pitfalls.

Its SKILL.md is about 2k tokens, which your agent loads only when the skill is triggered. It is a single SKILL.md file with no bundled scripts.

It sits in Writing & Content, covering Translation. The licence is Apache-2.0.

When your agent uses it

Tasks that involve Translation

Example prompts

“/vero-source-coq”

Requirements

Pre-approved tools (allowed-tools): Read, Write, Edit, Bash, Grep, Glob

What it can do on your machine

Read from SKILL.md and the folder at commit 0a7325d. It shows what the files ask for, not the result of running them.

Tool permissions
Pre-approves these tools, so the agent can use them without asking each time:
- Read
- Write
- Edit
- Bash
- Grep
- Glob
From allowed-tools in the SKILL.md frontmatter.
Runs code
No scripts in the folder and no shell commands in SKILL.md (its code samples are coq, lean and json).
From the folder's file list and the shell code blocks in SKILL.md.
Network
No URLs in SKILL.md.
From URLs in SKILL.md, links to its own repository left out.
Credentials
Names no API keys, tokens, secrets or passwords.
From names ending in _API_KEY, _TOKEN, _SECRET, _KEY or _PASSWORD in SKILL.md.

Context cost

Vero Source Coq loads about 2k tokens when it runs. Until then it costs about 93 tokens; SKILL.md has 715 words of instructions outside code blocks.

Always · name and description, kept in context so the agent knows when to use it: ~93
When it runs · the whole SKILL.md, loaded when a task matches: ~2k

Estimates: characters ÷ 4, the usual rule of thumb; real counts depend on the model's tokenizer. Scripts and assets cost tokens only if the agent reads them.

Safety

Auto-check: notes

The automated check noted patterns worth knowing about, such as sudo or a known installer.

NotePre-approves every shell command (allowed-tools: Bash)SKILL.md
```
allowed-tools: Read, Write, Edit, Bash, Grep, Glob
```

Automated static check — not a guarantee. Review scripts before installing. It scans the text of SKILL.md for risky patterns (piping downloads into a shell, reading credential files, hidden Unicode, destructive commands); files beside SKILL.md are not scanned.

SKILL.md

The full file from sunblaze-ucb/vero at commit 0a7325d, republished under its Apache-2.0 licence (© sunblaze-ucb). 715 words, ~2,028 tokens.

Download SKILL.mdSave it as .claude/skills/vero-source-coq/SKILL.md (or your agent's skills folder).

name: vero-source-coq
description: Load BEFORE translating Coq source (.v files) to Lean 4. Provides Coq-specific classification rules, type mappings, and patterns for mapping Coq constructs (Definition / Fixpoint / Inductive / Theorem / Module) into the ratified bundle paradigm (Impl/ + Spec/ + Bundle + Harness). Pair with vero-discover, vero-plan, vero-translate, and vero-coq-pitfalls.
allowed-tools: Read, Write, Edit, Bash, Grep, Glob

VCG Source: Coq → Lean 4

Coq-specific classification and translation patterns for the ratified curation paradigm. The shape of the emitted Lean is pinned by reference/BankLedger/ + .claude/skills/vero-translate/SKILL.md — this skill teaches the language mapping.

Lean 4's core calculus (CIC-like + inductive families) is close to Coq's. The main work is Module/Section → Lean namespace, tactic divergence, and the Prop vs Bool decidability split.

When to use

Classifying items in a Coq source (.v) with vero-discover.
Writing the translation plan with vero-plan.
Emitting Lean from Coq with vero-translate.

Output-shape recap (non-negotiable)

Per source-side Coq module (a Section, Module, or one .v file), translate emits:

<Project>/Impl/<Module>.lean — types + sig abbrevs + translated reference implementations in code slots.
<Project>/Spec/<Module>.lean — def spec_<…> (impl : RepoImpl) : Prop := …. Frozen, no markers.
Bundle.lean + Harness.lean + Test.lean shared across modules.

See .claude/skills/vero-translate/SKILL.md for file templates.

Coq construct → Lean classification

Coq	Lean artifact	Markers?
`Definition` (computable, API)	`def Bank.<fn> : Bank.<FnSig> := <translated reference impl>`	Yes — `code` / `code_aux`
`Definition` (vocabulary)	`def <name> : <type> := …` full body	No
`Fixpoint` (API)	Same as API `Definition`, with the translated recursive reference implementation	Yes
`Fixpoint` (vocabulary)	`def <name>` with full body; `termination_by` if needed	No
`Inductive`	`inductive <name> where \| <ctor> : <type>`	No
`Record`	`structure <name> where <field> : <type>`	No
`Class` (type class)	`class <name> where <field> : <type>`	No
`Theorem` / `Lemma` (property worth tracking)	`spec_<name>` in plan.json	No (Spec frozen)
`Theorem` / `Lemma` (proof helper only)	Drop from plan — becomes `proof_aux` downstream	—
`Axiom`	`axiom <name> : <type>` in Impl	No
`Parameter`	`axiom <name>` or `opaque` if a caller provides the impl	No
`Hypothesis` (inside Section)	Becomes arguments to post-`End` definitions	—
`Notation`	Usually elide; translate expands where used	—
`Scheme` (induction principles)	Skip — Lean generates them automatically	—

Classify by role. A Fixpoint implementing fold (vocabulary used by other defs) → full-body helper, no markers. A Fixpoint for push (an API the user calls) → translated reference implementation in a code slot.

Type mapping

Coq	Lean 4
`nat`	`Nat`
`Z`	`Int`
`N`	`Nat`
`bool`	`Bool`
`Prop`	`Prop`
`string`	`String`
`list A`	`List A`
`option A`	`Option A`
`sum A B`	`A ⊕ B`
`prod A B`	`A × B`
`{x : A	P x}`
`A -> B`	`A → B`
`forall x, P x`	`∀ x, P x`
`exists x, P x`	`∃ x, P x`
`unit`	`Unit`
`True` / `False` (in Prop)	`True` / `False`

Prop vs Bool: Coq often uses bool for decidable checks; Lean 4 has Bool + Decidable instances. Keep Bool returns as Bool; specs can use = true / = false.

Namespace translation

Coq's Section and Module both become Lean namespaces when needed, but the project's public API lives under one umbrella namespace (e.g. Bank). Individual Coq modules become file names under Impl/, not separate Lean namespaces.

coq

Module Account.
  Definition create_account (id : nat) (l : ledger) : ledger := …
End Account.

→ emitted in Impl/Account.lean:

lean

namespace Bank
abbrev CreateAccountSig := AccountId → Ledger → Ledger
end Bank

def Bank.createAccount : Bank.CreateAccountSig := <translated reference impl>

The Coq module name Account determines the file name; the Lean namespace is Bank (the API umbrella).

Show full SKILL.md (262 more words)Show less

API translation pattern

Coq:

coq

Definition create_account (id : nat) (l : ledger) : ledger := …

plan.json:

json

{
  "upstream_name": "create_account",
  "lean_name": "createAccount",
  "sig_abbrev": "CreateAccountSig",
  "lean_type": "AccountId → Ledger → Ledger",
  "opaque": false,
  "nl_description": "Add a new account with the given id to the ledger."
}

Emitted Impl:

lean

namespace Bank
abbrev CreateAccountSig := AccountId → Ledger → Ledger
end Bank

-- !benchmark @start code_aux def=createAccount
-- !benchmark @end code_aux def=createAccount

-- !curation @review v1 [ ] createAccount — Impl/Account, code, reference impl
def Bank.createAccount : Bank.CreateAccountSig :=
-- !benchmark @start code def=createAccount
  -- translated Coq body, not `sorry`
  ...
-- !benchmark @end code def=createAccount

Partial functions

Coq functions are total by construction. When the source uses a subset type ({x : A | P x}), translate as Subtype, or relax to A + a hypothesis argument, or switch to Option A — match the project's overall convention.

Spec translation pattern

`Theorem` / `Lemma` → spec entry

Coq:

coq

Theorem deposit_preserves_sum :
  forall (id : nat) (amt : nat) (l : ledger),
    sum (deposit id amt l) = sum l + amt.
Proof. … Qed.

plan.json:

json

{
  "name": "spec_deposit_preserves_sum",
  "nl_description": "Depositing `amt` adds exactly `amt` to the total.",
  "lean_form": "∀ (id : AccountId) (amt : Balance) (l : Ledger), impl.bankLedger.totalAssets (impl.bankLedger.deposit id amt l) = impl.bankLedger.totalAssets l + amt",
  "apis_referenced": ["deposit", "totalAssets"],
  "curator_intended_truth": "prove"
}

Emitted Spec:

lean

/-- Depositing `amt` adds exactly `amt` to the total. -/
def spec_deposit_preserves_sum (impl : RepoImpl) : Prop :=
  ∀ (id : AccountId) (amt : Balance) (l : Ledger),
    impl.bankLedger.totalAssets (impl.bankLedger.deposit id amt l) =
      impl.bankLedger.totalAssets l + amt

The Coq proof body is discarded — the Lean proof is materialized per-mode downstream.

The theorem statement is not optional. If you cannot translate the Coq proposition into a concrete Lean Prop, do not emit a scored spec_<name> for it. Keep the item review-only/untranslated with source provenance and a reason. Do not use a generated predicate such as sourceSpec, source-token wrappers, True, or any other placeholder to stand in for the theorem body.

`Lemma` as a proof helper

Used only by other proofs (no standalone property) → drop from plan.json. The LLM produces analogous helpers in proof_aux slots downstream.

Sections and `Implicit Type`

coq

Section LedgerOps.
  Variable L : ledger.
  Hypothesis (HL : valid L).
  Definition deposit_safe (id amt : nat) : ledger := …
End LedgerOps.

After End, deposit_safe takes L and HL as explicit arguments. Translate the exported (post-End) signature. Don't carry the Section block into Lean.

Common pitfalls (see `vero-coq-pitfalls`)

Prop vs bool vs Bool — pick one for API returns; be consistent.
Program Fixpoint / Function / Equations — translate to plain def with explicit termination_by if needed.
Coercions — Coq's implicit coercions often don't survive; make conversions explicit in the Lean form.
classical / choice axioms — flag as !curation @review; Lean's stdlib may need Classical.choice.

Load vero-coq-pitfalls before translating any non-trivial item.

Pair with

vero-plan — consumes Coq classifications.
vero-translate — emits Lean per the templates.
vero-coq-pitfalls — Coq→Lean corner cases.
vero-lean-pitfalls — universal Lean traps.

Files

Just SKILL.md in .claude/skills/vero-source-coq of sunblaze-ucb/vero.

Open the folder on GitHubat commit 0a7325d

Compare with similar skills

Vero Source Coq next to the 5 skills that share the most tags, products or categories with it. Stars are the repository's; “used in” counts other GitHub owners with a copy.

Vero Source Coq compared with similar skills
Skill	Stars	Used in	Tokens	Auto-check	Licence	Repo updated
Vero Source Coq this skillsunblaze-ucb/vero	107	—	~2k	Automated safety check: Notes	Apache-2.0	1 mo ago
Translation Diff ExportDevolutions/UniGetUI	26k	—	~1.1k	Automated safety check: Pass	MIT	today
Sync Translationssymfony/symfony	31k	—	~1.9k	Automated safety check: Pass	MIT	yesterday
Translation Diff ImportDevolutions/UniGetUI	26k	—	~750	Automated safety check: Pass	MIT	today
Translation Diff TranslateDevolutions/UniGetUI	26k	—	~934	Automated safety check: Pass	MIT	today
Generate Translationspayloadcms/payload	45k	—	~1.1k	Automated safety check: Pass	MIT	today

Similar skills

Translation Diff Export
Devolutions/UniGetUI
Compares UniGetUI JSON locale files against English, identifies untranslated or source-changed keys, and generates patch, reference, and handoff files for a target language.
26k GitHub stars~1.1k tokensUpdated today
Writing & ContentAuto-check passed
Sync Translations
symfony/symfony
Synchronize translation catalogs across maintained Symfony branches: find messages that newer branches added to the English catalogs but that are still missing from the oldest maintained branch…
31k GitHub stars~1.9k tokensUpdated yesterday
Writing & ContentAuto-check passed
Translation Diff Import
Devolutions/UniGetUI
Merges translated key-value pairs from a UniGetUI JSON localization patch back into the full language file and validates the merged result.
26k GitHub stars~750 tokensUpdated today
Writing & ContentAuto-check passed
Translation Diff Translate
Devolutions/UniGetUI
Translates a sparse UniGetUI JSON language patch, writes completed entries into the working copy, preserves placeholders and terminology, and prepares the patch for merge-back.
26k GitHub stars~934 tokensUpdated today
Writing & ContentAuto-check passed
Generate Translations
payloadcms/payload
A skill your agent uses when new translation keys are added to packages to generate new translations strings
45k GitHub stars~1.1k tokensUpdated today
Writing & ContentAuto-check passed
InkOS Creative Harness
Narcooo/inkos
Drives long-form fiction, scripts, storyboards, interactive films and long-document translation through InkOS, with every change made by a typed action.
10k GitHub starsUsed in 1 repo~1.1k tokens
Writing & ContentAuto-check passed

Questions about Vero Source Coq

What does Vero Source Coq do?

Load BEFORE translating Coq source (.v files) to Lean 4. An agent skill from sunblaze-ucb/vero. Vero Source Coq is an agent skill from sunblaze-ucb/vero.v files) to Lean 4.

When should I use Vero Source Coq?

Vero Source Coq fits situations like: tasks that involve Translation.

How do I install Vero Source Coq in Claude Code?

Run `npx skills add sunblaze-ucb/vero --skill vero-source-coq -a claude-code`. Or copy the skill folder (.claude/skills/vero-source-coq in sunblaze-ucb/vero) into .claude/skills/vero-source-coq in your project. Claude Code loads it when a task matches its description.

How do I install Vero Source Coq in Codex?

Run `npx skills add sunblaze-ucb/vero --skill vero-source-coq -a codex`. Or copy the skill folder (.claude/skills/vero-source-coq in sunblaze-ucb/vero) into .agents/skills/vero-source-coq in your project. Codex loads it when a task matches its description.

Can I use Vero Source Coq in Cursor, Gemini CLI or GitHub Copilot?

Cursor, Gemini CLI, GitHub Copilot and OpenCode also load SKILL.md folders. With the skills CLI, run `npx skills add sunblaze-ucb/vero --skill vero-source-coq -a cursor` (or -a gemini-cli, github-copilot or opencode for the others). To copy it by hand, put the folder in .cursor/skills/vero-source-coq, .gemini/skills/vero-source-coq, .github/skills/vero-source-coq and .opencode/skills/vero-source-coq in your project.

What does Vero Source Coq need to run?

SKILL.md names no scripts, command-line tools or credentials: Vero Source Coq is instructions for the agent only. Its frontmatter pre-approves these tools: Read, Write, Edit, Bash, Grep, Glob.

Does Vero Source Coq access the network?

SKILL.md contains no URLs. Any network use would come from the scripts or tools the agent runs. This is read from the text; nothing was executed.

Is Vero Source Coq safe to install?

Our automated static check of SKILL.md found notes only (pre-approves every shell command (allowed-tools: bash)), nothing it rates as a warning. It is not a guarantee. Review the folder before installing.

What licence does Vero Source Coq use?

Vero Source Coq is published under the Apache-2.0 licence (the repository's licence). It allows redistribution, so the full SKILL.md is shown on this page.

How many tokens does Vero Source Coq use?

About 2k tokens (SKILL.md is roughly 8.1k characters). Agents keep only the skill's name and description in context until a task matches; then they load SKILL.md in full.

What are the alternatives to Vero Source Coq?

Skills that share tags, products or a category with Vero Source Coq: Translation Diff Export (Devolutions/UniGetUI, 26k stars), Sync Translations (symfony/symfony, 31k stars), Translation Diff Import (Devolutions/UniGetUI, 26k stars) and Translation Diff Translate (Devolutions/UniGetUI, 26k stars). The comparison table on this page puts their stars, adoption, token cost, safety result and licence side by side.

Who maintains Vero Source Coq?

sunblaze-ucb (a GitHub organization) maintains it in sunblaze-ucb/vero, which has 107 GitHub stars. The repository holds 16 skills in this directory. The repository was last updated on August 17, 2026.

Source: sunblaze-ucb/vero on GitHub. Facts on this page come from the repository at the commit we read; the author's words are quoted as theirs.

Install Vero Source Coq

Facts

At a glance

What it does

When your agent uses it

Example prompts

Requirements

What it can do on your machine

Tool permissions

Runs code

Network

Credentials

Context cost

Safety

SKILL.md

VCG Source: Coq → Lean 4

When to use

Output-shape recap (non-negotiable)

Coq construct → Lean classification

Type mapping

Namespace translation

API translation pattern

Partial functions

Spec translation pattern

Theorem / Lemma → spec entry

Lemma as a proof helper

Sections and Implicit Type

Common pitfalls (see vero-coq-pitfalls)

Pair with

Files

Compare with similar skills

Similar skills

More from sunblaze-ucb/vero

Related

Questions about Vero Source Coq

`Theorem` / `Lemma` → spec entry

`Lemma` as a proof helper

Sections and `Implicit Type`

Common pitfalls (see `vero-coq-pitfalls`)